ilang  0.9.0
ILAng: A Modeling and Verification Platform for SoCs
Classes | Typedefs | Enumerations | Functions
ilang Namespace Reference

Classes

class  AbsKnob
 
class  Ast
 The class for the Abstract Syntax Tree. An Ast object can be an expression or function definition (interpreted or uninterpreted). More...
 
class  BoolVal
 The container for representing Boolean values. More...
 
class  BvVal
 The container for representing Bitvector values. More...
 
class  CommDiag
 Generator for commutating diagram-based equivalence checking. More...
 
class  CompRefRel
 Compositional refinement relation defines a unit (element for the composition) of refinement relation, which specifies. More...
 
class  Cosa_problem
 a class to store (and generate) the problem for cosa More...
 
class  DebugLog
 The wrapper for enabling and disabling debug tags. More...
 
class  Expr
 The class for expression, which is the basic type for variables, constraints, state update expressions, etc. More...
 
class  ExprConst
 Expression for constant values (bool, bv, or memory). Constant should be terminating nodes in the AST. More...
 
class  ExprHash
 The function object for hashing Expr. The hash value is the id of the symbol, which is supposed to be unique. More...
 
class  ExprMngr
 Simplifier for AST trees by sharing nodes based on the hash value. More...
 
class  ExprOp
 Expression for operations, e.g. AND, OR, ADD, etc. Operations are non-terminating nodes in the AST. More...
 
class  ExprOpAdd
 The wrapper for unsigned addition. More...
 
class  ExprOpAnd
 The wrapper for binary logical AND operation "&". More...
 
class  ExprOpAppFunc
 The class wrapper for apply uninterpreted function. More...
 
class  ExprOpAshr
 The wrapper for arithmetic right shifting a bit-vector. More...
 
class  ExprOpCompl
 The wrapper for unary bit-wise complement "~". (bv only) More...
 
class  ExprOpConcat
 The class wrapper for bitvector concatenation. More...
 
class  ExprOpEq
 The class wrapper for binary comparison EQ "==". More...
 
class  ExprOpExtract
 The class wrapper for bitvector extraction. More...
 
class  ExprOpGt
 The class wrapper for binary comparison signed greater than ">". More...
 
class  ExprOpImply
 The class wrapper for logical imply. More...
 
class  ExprOpIte
 The class wrapper for if-then-else. More...
 
class  ExprOpLoad
 The class wrapper for memory load. More...
 
class  ExprOpLshr
 The wrapper for logical right shifting a bit-vector. More...
 
class  ExprOpLt
 The class wrapper for binary comparison signed less than "<". More...
 
class  ExprOpNeg
 The wrapper for unary negate operation "-". More...
 
class  ExprOpNot
 The wrapper for unary not operation "!". (bool only) More...
 
class  ExprOpOr
 The wrapper for binary logical OR operation "|". More...
 
class  ExprOpSExt
 The calss wrapper for sign-extend. More...
 
class  ExprOpShl
 The wrapper for left shifting a bit-vector. More...
 
class  ExprOpStore
 The class wrapper for memory store. More...
 
class  ExprOpSub
 The wrapper for unsigned subtraction. More...
 
class  ExprOpUgt
 The class wrapper for binary comparison unsigned greater than. More...
 
class  ExprOpUlt
 The class wrapper for binary comparison unsigned less than. More...
 
class  ExprOpXor
 The wrapper for binary logical XOR operation "^". More...
 
class  ExprOpZExt
 The class wrapper for zero-extend. More...
 
class  ExprRef
 The wrapper of Expr (e.g. state var, var relation, constant, etc). More...
 
class  ExprVar
 Expression for variables (bool, bv, or mem). Variable should be the terminating nodes in the AST. More...
 
class  Func
 The class for uninterpreted function. More...
 
class  FuncObjFlatIla
 Function object for flatten ILA tree. There is currently a problem: this func obj calls duplInst which in turn uses rewriteExpr and rewriteExpr does not change the host of of state variables, so the flatten expression still has the host pointed to their original ILA. This is fine for Verilog Gen, which only depends on variable names to generate variables but may not be good enough for other purpose. More...
 
class  FuncObjRewrExpr
 Function object for rewriting Expr. More...
 
class  FuncObjRewrIla
 Function object for rewriting ILA tree. More...
 
class  FuncRef
 The wrapper of Func (uninterpreted function). More...
 
class  HostRemoveRestore
 Class to remove and restore the host info This is useful as we want the ast with the same name generates the same z3 expr. This framework is based on an assumption that if we call z3 to create the variable of the same name multiple times they refer to the same one internally. FIXME: Need to check this assumption if we want to support other SMT solvers! More...
 
class  Ila
 The wrapper of InstrLvlAbs (ILA). More...
 
class  IlaZ3Unroller
 The wrapper of generating z3::expr for verification. More...
 
class  Instr
 The class for the Instruction. An Instr object contains: More...
 
class  InstrLvlAbs
 The class of Instruction-Level Abstraction (ILA). An ILA contains: More...
 
class  InstrRef
 The wrapper of Instr (instruction). More...
 
class  InstrSeq
 Instruction Sequencing does: More...
 
class  InstrTranEdge
 Instruction transition edge, includeing: More...
 
class  InstrTranNode
 Node for instruction-transition node, each node represent an instruction. More...
 
class  IntefaceDirectiveRecorder
 Used in Verilog Verification Target Generation for dealing with interface directives. More...
 
class  InterIlaUnroller
 Base class for unrolling multiple ILAs. There are two ways of unrolling: ordered and unordered. Ordered unrolling assumes an ordered program template, despite that some may not exist in the final outcome. By default the state with the same name among ILAs is considered as the same shared state. More...
 
class  KeyVec
 The container that support key search and index access. More...
 
class  KeyVecIt
 A pseudo-iterator for the key-search vector. More...
 
class  LegacyBmc
 Simplified bounded model checking engine for ILAs. More...
 
class  LogInitter
 A one-time class for initializing GLog. More...
 
class  MapSet
 A map for sets. More...
 
class  MemoryModel
 The base class for memory models. More...
 
class  MemVal
 The container for representing memory (array) values. More...
 
class  MonoUnroll
 Application class for unrolling the ILA as a monolithic transition system. More...
 
class  NestedMemAddrDataAvoider
 Class of traversing to avoid nested memory access in address. More...
 
class  Object
 The basest type in the ILA structure. It can be either Ast, Instr, or InstrLvlAbs. More...
 
class  PathUnroll
 Application class for unrolling a path of instruction sequence. More...
 
class  PortableMngr
 The class for exporting and importing ILA portable in JSON format. More...
 
class  RefinementMap
 Refinement mapping defines how to map micro-architectural states to architectural states for comparison. More...
 
class  RelationMap
 Relation mapping defines how arch states of two models are mapped, i.e., state mapping. More...
 
class  Sc
 Class of TSO. More...
 
class  ScTraceStep
 Class of TSO trace step. More...
 
class  SignalInfoBase
 Class to hold signal info. More...
 
class  SignalInfoPort
 Class to convert port to signal info. More...
 
class  SignalInfoReg
 Class to convert reg to signal info. More...
 
class  SignalInfoWire
 Class to convert wire to signal info. More...
 
class  Sort
 The class for sort (type for expr, and the range/domain of functions). More...
 
class  SortBool
 The class of Boolean Sort. More...
 
class  SortBv
 The class of bit-vector Sort. More...
 
class  SortMem
 The class of memory (array) Sort. More...
 
class  SortRef
 The wrapper of Sort (type for different AST nodes). More...
 
class  StateMappingDirectiveRecorder
 a class to handle state mapping directives in the refinement relations More...
 
class  Symbol
 The symbol is the name and ID of an object. Every object has an unique symbol. More...
 
class  SynthAbsConverter
 The class for converting an abstraction from the synthesis engine to an ILA model. More...
 
class  TraceStep
 The class for trace step (an instance of instruction) As in the unrolling, there may be multiple instances of the same instructions, so we have the trace steps. More...
 
class  Tso
 Class of TSO. More...
 
class  TsoTraceStep
 Class of TSO trace step. More...
 
class  Unroller
 Base class for unrolling ILA execution in different settings. More...
 
class  Value
 The base type for constant value. More...
 
class  VarExtractor
 
class  VarUseFinder
 Class of finding variable uses. So that we don't need to create pi variables for unused state variables. FIXME: currently there is no need to make a class for it, but in the future it is possible to use a hash table to avoid traverse the same sub-tree twice. More...
 
class  VerilogAnalyzer
 Class for Verilog analysis. More...
 
class  VerilogAnalyzerBase
 VerilogAnalyzerBase should never be instantiated, only used as a pointer type in class VerilogInfo. More...
 
class  VerilogGenerator
 Class of Verilog Generator. More...
 
class  VerilogGeneratorBase
 Base class of VerilogGenerator. More...
 
class  VerilogInfo
 The class that invoke the analyzer. More...
 
class  VerilogModifier
 the class for modification to verilog More...
 
class  VerilogVerificationTargetGenerator
 
struct  VlgAbsMem
 a struct to store abstract memory More...
 
class  VlgSglTgtGen
 Generating a target (just the invairant or for an instruction) More...
 
class  VlgSglTgtGen_Cosa
 a class to interface w. COSA More...
 
class  VlgSglTgtGen_Jasper
 Verilog Verification Target Generator – for JasperGold Unlike for cosa, we don't need a separate file although we do have some ... More...
 
class  VlgVerifTgtGen
 
class  VlgVerifTgtGenBase
 VlgVerifTgtGenBase: do nothing, should not instantiate. More...
 
class  Z3ExprAdapter
 The class for generating z3 expression from an ILA. More...
 

Typedefs

typedef Expr::ExprPtr ExprPtr
 Pointer type for normal use of Expr.
 
typedef Expr::ExprPtrVec ExprPtrVec
 Type for storing a set of Expr.
 
typedef std::unordered_map< const ExprPtr, const ExprPtr, ExprHashExprMap
 Type for mapping between Expr.
 
typedef std::unordered_set< ExprPtr, ExprHashExprSet
 Type for storing a set of Expr.
 
typedef Func::FuncPtr FuncPtr
 Pointer type for normal use of Func.
 
typedef Sort::SortPtr SortPtr
 Pointer type for storing/passing Sort.
 
typedef Value::ValPtr ValPtr
 Pointer type for all use of Value.
 
typedef BoolVal::BoolValPtr BoolValPtr
 Pointer type for all use of BoolVal.
 
typedef BvVal::BvValType BvValType
 Data type for storing BvVal.
 
typedef BvVal::BvValPtr BvValPtr
 Pointer type for all use of BvVal.
 
typedef MemVal::MemValPtr MemValPtr
 Pointer type for all use of MemVal.
 
typedef MemVal::MemValMap MemValMap
 Type for storing the address/data mapping.
 
typedef RefinementMap::RefPtr RefPtr
 Pointer type for passing around the refinement mapping.
 
typedef RelationMap::RelPtr RelPtr
 Pointer type for passing around the relation mapping.
 
typedef CompRefRel::CrrPtr CrrPtr
 Pointer type for passing around the compositional relation mapping.
 
typedef std::vector< z3::expr > Z3ExprVec
 Vector type for z3 expression.
 
typedef std::shared_ptr< Z3ExprVecZ3ExprVecPtr
 Pointer for the z3 expression vector.
 
typedef KeyVec< Symbol, z3::expr > Z3ExprMap
 Map type for z3 expression.
 
typedef std::shared_ptr< Z3ExprMapZ3ExprMapPtr
 Pointer for the z3 expression map.
 
typedef ExprMngr::ExprMngrPtr ExprMngrPtr
 Pointer type for passing shared ast simplifier.
 
typedef Instr::InstrPtr InstrPtr
 Pointer type for normal use of Instr.
 
typedef std::shared_ptr< const InstrInstrCnstPtr
 Pointer type for read-only use of Instr.
 
typedef std::vector< InstrPtrInstrVec
 Type for storing a set of Instr.
 
typedef InstrLvlAbs::InstrLvlAbsPtr InstrLvlAbsPtr
 Pointer type for normal use of InstrLvlAbs.
 
typedef InstrLvlAbs::InstrLvlAbsCnstPtr InstrLvlAbsCnstPtr
 Pointer type for read-only usage of InstrLvlAbs.
 
typedef std::map< InstrLvlAbsCnstPtr, InstrLvlAbsPtrCnstIlaMap
 Type for storing a mapping from constant ILA ptr to ILA ptr.
 
typedef Object::ObjPtr ObjPtr
 Pointer type for normal use of Object.
 
typedef InstrSeq::InstrSeqPtr InstrSeqPtr
 Pointer type for passing around InstrSeq.
 
typedef ExprHash Z3AdapterHash
 The function object for hashing Expr in generating z3 expression.
 
typedef PortableMngr::PortableMngrPtr PortableMngrPtr
 Pointer type for normal use of PortableMngr.
 
typedef SynthAbsConverter::SynthAbsConverterPtr SynthAbsConverterPtr
 Pointer type for normal use of SynthAbsConverter.
 
typedef ExprHash VerilogGenHash
 

Enumerations

enum  AccessType { READ, WRITE, EITHER }
 Type of state read or write.
 
enum  KeyVecItVal { END, FOUND }
 KeyVecItVal.
 

Functions

void LogLevel (const int &lvl)
 Set the minimun log level. Log messages at or above this level will be logged. (Default: 0) More...
 
void LogPath (const std::string &path)
 Set the path for log file. If specified, logfiles are written into this directory instead of the default logging directory (/tmp).
 
void LogToErr (bool to_err)
 Pipe log to stderr. Log messages to stderr instead of logfiles, if set to 1.
 
void EnableDebug (const std::string &tag)
 Add a debug tag.
 
void DisableDebug (const std::string &tag)
 Remove a debug tag.
 
ExprRef operator- (const ExprRef &a)
 Arithmetic negate for bit-vectors.
 
ExprRef operator! (const ExprRef &a)
 Logical not for Booleans.
 
ExprRef operator~ (const ExprRef &a)
 Bit-wise complement for bit-vectors.
 
ExprRef operator & (const ExprRef &a, const ExprRef &b)
 Logical AND (bit-wise for bit-vectors).
 
ExprRef operator| (const ExprRef &a, const ExprRef &b)
 Logical OR (bit-wise for bit-vectors).
 
ExprRef operator^ (const ExprRef &a, const ExprRef &b)
 Logical XOR (bit-wise for bit-vectors).
 
ExprRef operator<< (const ExprRef &a, const ExprRef &b)
 Left shift for bit-vectors.
 
ExprRef operator>> (const ExprRef &a, const ExprRef &b)
 Arithmetic right shift for bit-vectors.
 
ExprRef Lshr (const ExprRef &a, const ExprRef &b)
 Logical right shift for bit-vectors.
 
ExprRef operator+ (const ExprRef &a, const ExprRef &b)
 Unsigned addition for bit-vectors.
 
ExprRef operator- (const ExprRef &a, const ExprRef &b)
 Unsigned subtraction for bit-vectors.
 
ExprRef operator & (const ExprRef &a, const bool &b)
 Logical AND with Boolean constant.
 
ExprRef operator| (const ExprRef &a, const bool &b)
 Logical OR with Boolean constant.
 
ExprRef operator^ (const ExprRef &a, const bool &b)
 Logical XOR with Boolean constant.
 
ExprRef operator<< (const ExprRef &a, const int &b)
 Left shift with int constant.
 
ExprRef operator>> (const ExprRef &a, const int &b)
 Arithmetic right shift with int constant.
 
ExprRef Lshr (const ExprRef &a, const int &b)
 Logical right shift with int constant.
 
ExprRef operator+ (const ExprRef &a, const int &b)
 Unsigned addition with int constant.
 
ExprRef operator- (const ExprRef &a, const int &b)
 Unsigned subtraction with int constant.
 
void SetUnsignedComparison (bool sign)
 
ExprRef operator== (const ExprRef &a, const ExprRef &b)
 Equal.
 
ExprRef operator!= (const ExprRef &a, const ExprRef &b)
 Not equal.
 
ExprRef operator< (const ExprRef &a, const ExprRef &b)
 Signed/Unsigned less than (bit-vectors only).
 
ExprRef operator> (const ExprRef &a, const ExprRef &b)
 Signed/Unsigned greater than (bit-vectors only).
 
ExprRef operator<= (const ExprRef &a, const ExprRef &b)
 Signed/Unsigned less than or equal to (bit-vectors only).
 
ExprRef operator>= (const ExprRef &a, const ExprRef &b)
 Signed/Unsigned greater than or equal to (bit-vectors only).
 
ExprRef Ult (const ExprRef &a, const ExprRef &b)
 Unsigned less than (bit-vectors only).
 
ExprRef Ugt (const ExprRef &a, const ExprRef &b)
 Unsigned greater than (bit-vectors only).
 
ExprRef Ule (const ExprRef &a, const ExprRef &b)
 Unsigned less than or equal to (bit-vectors only).
 
ExprRef Uge (const ExprRef &a, const ExprRef &b)
 Unsigned greater than or equal to (bit-vectors only).
 
ExprRef Slt (const ExprRef &a, const ExprRef &b)
 Signed less than (bit-vectors only).
 
ExprRef Sgt (const ExprRef &a, const ExprRef &b)
 Signed greater than (bit-vectors only).
 
ExprRef Sle (const ExprRef &a, const ExprRef &b)
 Signed less than or equal to (bit-vectors only).
 
ExprRef Sge (const ExprRef &a, const ExprRef &b)
 Signed greater than or equal to (bit-vectors only).
 
ExprRef operator== (const ExprRef &a, const bool &b)
 Equal to Boolean constant.
 
ExprRef operator== (const ExprRef &a, const int &b)
 Equal to int constant.
 
ExprRef operator!= (const ExprRef &a, const int &b)
 Not equal to int constant.
 
ExprRef operator< (const ExprRef &a, const int &b)
 Signed/Unsigned less than int constant (bit-vectors only).
 
ExprRef operator> (const ExprRef &a, const int &b)
 Signed/Unsigned greater than int constant (bit-vectors only).
 
ExprRef operator<= (const ExprRef &a, const int &b)
 Signed/Unsigned less than or equal to int constant (bit-vectors only).
 
ExprRef operator>= (const ExprRef &a, const int &b)
 Signed/Unsigned greater than or equal to int constant (bit-vectors only).
 
ExprRef Ult (const ExprRef &a, const int &b)
 Unsigned less than int constant (bit-vectors only).
 
ExprRef Ugt (const ExprRef &a, const int &b)
 Unsigned greater than int constant (bit-vectors only).
 
ExprRef Ule (const ExprRef &a, const int &b)
 Unsigned less than or equal to int constant (bit-vectors only).
 
ExprRef Uge (const ExprRef &a, const int &b)
 Unsigned greater than or equal to int constant (bit-vectors only).
 
ExprRef Slt (const ExprRef &a, const int &b)
 Signed less than int constant (bit-vectors only).
 
ExprRef Sgt (const ExprRef &a, const int &b)
 Signed greater than int constant (bit-vectors only).
 
ExprRef Sle (const ExprRef &a, const int &b)
 Signed less than or equal to int constant (bit-vectors only).
 
ExprRef Sge (const ExprRef &a, const int &b)
 Signed greater than or equal to int constant (bit-vectors only).
 
ExprRef Load (const ExprRef &mem, const ExprRef &addr)
 Load from memory.
 
ExprRef Store (const ExprRef &mem, const ExprRef &addr, const ExprRef &data)
 Store to memory.
 
ExprRef Load (const ExprRef &mem, const int &addr)
 Load from memory with constant address.
 
ExprRef Store (const ExprRef &mem, const int &addr, const int &data)
 Store to memory at constant address and data.
 
ExprRef Concat (const ExprRef &msbv, const ExprRef &lsbv)
 Concatenate two bit-vectors. More...
 
ExprRef Extract (const ExprRef &bv, const int &hi, const int &lo)
 Extract bit-field in the bit-vector. More...
 
ExprRef SelectBit (const ExprRef &bv, const int &idx)
 Extract single bit in the bit-vector. More...
 
ExprRef ZExt (const ExprRef &bv, const int &length)
 Zero-extend the bit-vector to the specified length. More...
 
ExprRef SExt (const ExprRef &bv, const int &length)
 Sign-extend the bit-vector to the specified length. More...
 
ExprRef Imply (const ExprRef &ante, const ExprRef &cons)
 Logical imply for Booleans. More...
 
ExprRef Ite (const ExprRef &cond, const ExprRef &t, const ExprRef &f)
 If-then-else on the Boolean condition. More...
 
ExprRef BoolConst (bool bool_val)
 Return a Boolean constant. More...
 
ExprRef BvConst (const int &bv_val, const int &bit_width)
 Return a bit-vector constant. More...
 
ExprRef MemConst (const int &def_val, const std::map< int, int > &vals, const int &addr_width, const int &data_width)
 Return a memory constant. More...
 
bool TopEqual (const ExprRef &a, const ExprRef &b)
 Topologically equivalent.
 
std::ostream & operator<< (std::ostream &out, const ExprRef &expr)
 Print out the ExprRef.
 
std::ostream & operator<< (std::ostream &out, const InstrRef &instr)
 Print out the Instruction.
 
std::ostream & operator<< (std::ostream &out, const Ila &ila)
 Print out the ILA.
 
z3::expr Z3And (const z3::expr &a, const z3::expr &b)
 This is just a shortcut to be used for generated axiom.
 
bool ExportPortableToFile (const InstrLvlAbsPtr &ila, const std::string &file)
 Export the ILA portable to a file. More...
 
InstrLvlAbsPtr ImportPortableFromFile (const std::string &file)
 Import the ILA model from the file. More...
 
InstrLvlAbsPtr ImportSynthAbsFromFile (const std::string &file_name, const std::string &ila_name="")
 Import from file the abstraction from the synthesis engine and convert it into an ILA model. More...
 
InstrLvlAbsPtr ImportSynthAbsFromFileHier (const std::string &file_name, const InstrLvlAbsPtr parent, const std::string &ila_name="")
 Import from file the abstraction from the synthesis engine and convert it into a child-ILA of the specified parent ILA. More...
 
bool os_portable_mkdir (const std::string &dir)
 Create a dir, true -> suceeded , ow false.
 
bool os_portable_copy_dir (const std::string &src, const std::string &dst)
 Copy all file from a source dir to the destination dir.
 
bool os_portable_copy_file_to_dir (const std::string &src, const std::string &dst)
 Copy one file to the destination dir.
 
std::string os_portable_append_dir (const std::string &dir1, const std::string &dir2)
 Append two path (you have to decide whether it is / or )
 
std::string os_portable_file_name_from_path (const std::string &path)
 
void SetLogLevel (const int &lvl)
 Set the minimun log level. Log messages at or above this level will be logged. (Default: 0) More...
 
void SetLogPath (const std::string &path)
 Set the path for log file. If specified, logfiles are written into this directory instead of the default logging directory (/tmp).
 
void SetToStdErr (const int &to_err)
 Pipe log to stderr. Log messages to stderr instead of logfiles, if set to 1.
 
std::string StrToUpper (const std::string &str)
 Transform basic string to upper case.
 
std::string StrToLower (const std::string &str)
 Transform basic string to lower case.
 
bool StrToBool (const std::string &str)
 Return true if string is "true" or "True".
 
int StrToInt (const std::string &str, int base=10)
 Return the value represented in the string, e.g. "10".
 
std::vector< std::string > Split (const std::string &str, const std::string &delim)
 Python-style split , return a vector of splitted strings.
 
std::vector< std::string > SplitSpaceTabEnter (const std::string &str)
 Python-style split behavior, delim: space tab enter and their combiniations.
 
std::string Join (const std::vector< std::string > &in, const std::string &delim)
 Python-style join, return a string that joins the list by the delim.
 
std::string ReplaceAll (const std::string &str, const std::string &a, const std::string &b)
 Replace all occurrance of substring a by substring b.
 
std::vector< std::string > ReFindList (const std::string &s, const std::string &re)
 Filter out a list of substring by the regular expression.
 
std::vector< std::string > ReFindAndDo (const std::string &s, const std::string &re, std::function< std::string(std::string)> f)
 
bool IsRExprUsable ()
 
z3::expr Z3Implies (z3::context &ctx, const z3::expr &a, const z3::expr &b)
 Interface z3 implies ast node construction.
 
z3::expr Z3Shl (z3::context &ctx, const z3::expr &a, const z3::expr &b)
 Interface z3 shl ast node construction.
 
z3::expr Z3Ashr (z3::context &ctx, const z3::expr &a, const z3::expr &b)
 Interface z3 ashr ast node construction.
 
z3::expr Z3Lshr (z3::context &ctx, const z3::expr &a, const z3::expr &b)
 Interface z3 lshr ast node construction.
 
z3::expr Z3ZExt (z3::context &ctx, const z3::expr &e, const unsigned &w)
 Interface z3 zext ast node construction.
 
z3::expr Z3SExt (z3::context &ctx, const z3::expr &e, const unsigned &w)
 Interface z3 sext ast node construction.
 
std::string Z3Expr2String (z3::context &ctx, const z3::expr &e)
 Return the output string of the given z3::expr.
 
std::ostream & operator<< (std::ostream &os, const VerilogAnalyzerBase::vlg_loc_t &obj)
 overload the operator << for printing location
 
void TestParseVerilog ()
 
int TestParseVerilogFrom (std::FILE *fp)
 

Detailed Description

Defines the core data structure and APIs for constructing and storing ILA.

Function Documentation

◆ BoolConst()

ExprRef ilang::BoolConst ( bool  bool_val)

Return a Boolean constant.

Parameters
[in]bool_valvalue of the Boolean constant.

◆ BvConst()

ExprRef ilang::BvConst ( const int &  bv_val,
const int &  bit_width 
)

Return a bit-vector constant.

Parameters
[in]bv_valvalue of the bit-vector constant.
[in]bit_widthdata bit-width.

◆ Concat()

ExprRef ilang::Concat ( const ExprRef msbv,
const ExprRef lsbv 
)

Concatenate two bit-vectors.

Parameters
[in]msbvbit-vector on the more-significant side.
[in]lsbvbit-vector on the less-significant side.

◆ ExportPortableToFile()

bool ilang::ExportPortableToFile ( const InstrLvlAbsPtr ila,
const std::string &  file 
)

Export the ILA portable to a file.

Parameters
[in]ilapointer to the ila model to be exported.
[in]fileoutput file name.
Returns
export status.

◆ Extract()

ExprRef ilang::Extract ( const ExprRef bv,
const int &  hi,
const int &  lo 
)

Extract bit-field in the bit-vector.

Parameters
[in]bvsource bit-vector.
[in]hithe index of the most-significant bit.
[in]lothe index of the least-significant bit.

◆ Imply()

ExprRef ilang::Imply ( const ExprRef ante,
const ExprRef cons 
)

Logical imply for Booleans.

Parameters
[in]anteantecedent for the operator.
[in]consconsequent for the operator.

◆ ImportPortableFromFile()

InstrLvlAbsPtr ilang::ImportPortableFromFile ( const std::string &  file)

Import the ILA model from the file.

Parameters
[in]fileinput file name.
Returns
the generated ILA model.

◆ ImportSynthAbsFromFile()

InstrLvlAbsPtr ilang::ImportSynthAbsFromFile ( const std::string &  file_name,
const std::string &  ila_name = "" 
)

Import from file the abstraction from the synthesis engine and convert it into an ILA model.

Parameters
[in]file_namefile name of the abstraction from the synthesis engine.
[in]ila_namename of the created ILA model.
Returns
the generated ILA model.

◆ ImportSynthAbsFromFileHier()

InstrLvlAbsPtr ilang::ImportSynthAbsFromFileHier ( const std::string &  file_name,
const InstrLvlAbsPtr  parent,
const std::string &  ila_name = "" 
)

Import from file the abstraction from the synthesis engine and convert it into a child-ILA of the specified parent ILA.

Parameters
[in]file_namefile name of the abstraction from the synthesis engine.
[in]parentpointer to the parent ILA.
[in]ila_namename of the created ILA model.
Returns
the generated ILA model.

◆ Ite()

ExprRef ilang::Ite ( const ExprRef cond,
const ExprRef t,
const ExprRef f 
)

If-then-else on the Boolean condition.

Parameters
[in]condBoolean type condition.
[in]tExpression to take when the condition is true.
[in]fExpression to take when the condition is false.

◆ LogLevel()

void ilang::LogLevel ( const int &  lvl)

Set the minimun log level. Log messages at or above this level will be logged. (Default: 0)

  • INFO: level 0
  • WARNING: level 1
  • ERROR: level 2
  • FATAL: level 3

◆ MemConst()

ExprRef ilang::MemConst ( const int &  def_val,
const std::map< int, int > &  vals,
const int &  addr_width,
const int &  data_width 
)

Return a memory constant.

Parameters
[in]def_valdefault value.
[in]valsnon-default address-data mapping.
[in]addr_widthaddress bit-width.
[in]data_widthdata bit-width.

◆ os_portable_file_name_from_path()

std::string ilang::os_portable_file_name_from_path ( const std::string &  path)

Extract filename from path C: .txt -> c.txt d/e/ghi -> ghi

◆ ReFindAndDo()

std::vector<std::string> ilang::ReFindAndDo ( const std::string &  s,
const std::string &  re,
std::function< std::string(std::string)>  f 
)

Filter out a list of substring by the regular expression, call f each time and use its return value in the list, f can also do something else in itself

◆ SelectBit()

ExprRef ilang::SelectBit ( const ExprRef bv,
const int &  idx 
)

Extract single bit in the bit-vector.

Parameters
[in]bvsource bit-vector.
[in]idxthe index of the selected bit.

◆ SetLogLevel()

void ilang::SetLogLevel ( const int &  lvl)

Set the minimun log level. Log messages at or above this level will be logged. (Default: 0)

  • INFO: level 0
  • WARNING: level 1
  • ERROR: level 2
  • FATAL: level 3

◆ SetUnsignedComparison()

void ilang::SetUnsignedComparison ( bool  sign)

Set the default behavior of operator <, <=, > and >=, by default, signed compare

◆ SExt()

ExprRef ilang::SExt ( const ExprRef bv,
const int &  length 
)

Sign-extend the bit-vector to the specified length.

Parameters
[in]bvsource bit-vector.
[in]lengthbit-width of the extended (result) bit-vector.

◆ ZExt()

ExprRef ilang::ZExt ( const ExprRef bv,
const int &  length 
)

Zero-extend the bit-vector to the specified length.

Parameters
[in]bvsource bit-vector.
[in]lengthbit-width of the extended (result) bit-vector.