Classes
class	Ast
	The class for the Abstract Syntax Tree. An Ast object can be an expression or function definition (interpreted or uninterpreted). More...

class	Expr
	The class for expression, which is the basic type for variables, constraints, state update expressions, etc. 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	ExprConst
	Expression for constant values (bool, bv, or memory). Constant should be terminating nodes in the AST. More...

class	ExprOp
	Expression for operations, e.g. AND, OR, ADD, etc. Operations are non-terminating nodes in the AST. More...

class	ExprOpNeg
	The wrapper for unary negate operation "-". More...

class	ExprOpNot
	The wrapper for unary not operation "!". (bool only) More...

class	ExprOpCompl
	The wrapper for unary bit-wise complement "~". (bv only) More...

class	ExprOpAnd
	The wrapper for binary logical AND operation "&". More...

class	ExprOpOr
	The wrapper for binary logical OR operation "\|". More...

class	ExprOpXor
	The wrapper for binary logical XOR operation "^". More...

class	ExprOpShl
	The wrapper for left shifting a bit-vector. More...

class	ExprOpAshr
	The wrapper for arithmetic right shifting a bit-vector. More...

class	ExprOpLshr
	The wrapper for logical right shifting a bit-vector. More...

class	ExprOpAdd
	The wrapper for unsigned addition. More...

class	ExprOpSub
	The wrapper for unsigned subtraction. More...

class	ExprOpDiv
	The wrapper for unsigned division. More...

class	ExprOpSRem
	The wrapper for signed remainder. More...

class	ExprOpURem
	The wrapper for unsigned remainder. More...

class	ExprOpSMod
	The wrapper for signed remainder. More...

class	ExprOpMul
	The wrapper for unsigned multiplication. More...

class	ExprOpEq
	The class wrapper for binary comparison EQ "==". More...

class	ExprOpLt
	The class wrapper for binary comparison signed less than "<". More...

class	ExprOpGt
	The class wrapper for binary comparison signed greater than ">". More...

class	ExprOpUlt
	The class wrapper for binary comparison unsigned less than. More...

class	ExprOpUgt
	The class wrapper for binary comparison unsigned greater than. More...

class	ExprOpLoad
	The class wrapper for memory load. More...

class	ExprOpStore
	The class wrapper for memory store. More...

class	ExprOpConcat
	The class wrapper for bitvector concatenation. More...

class	ExprOpExtract
	The class wrapper for bitvector extraction. More...

class	ExprOpZExt
	The class wrapper for zero-extend. More...

class	ExprOpSExt
	The class wrapper for sign-extend. More...

class	ExprOpLRotate
	The class wrapper for left-rotate. More...

class	ExprOpRRotate
	The class wrapper for right-rotate. More...

class	ExprOpAppFunc
	The class wrapper for apply uninterpreted function. More...

class	ExprOpImply
	The class wrapper for logical imply. More...

class	ExprOpIte
	The class wrapper for if-then-else. 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	FuncHash
	The function object for hashing Func. The hash value is the id of the symbol, which is supposed to be unique. 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	Value
	The base type for constant value. More...

class	BoolVal
	The container for representing Boolean values. More...

class	BvVal
	The container for representing Bitvector values. More...

class	MemVal
	The container for representing memory (array) values. More...

class	ExprMngr
	Simplifier for AST trees by sharing nodes based on the hash value. 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	Object
	The basest type in the ILA structure. It can be either Ast, Instr, or InstrLvlAbs. More...

class	Symbol
	The symbol is the name and ID of an object. Every object has an unique symbol. More...

class	InstrTranEdge
	Instruction transition edge, includeing: More...

class	InstrTranNode
	Node for instruction-transition node, each node represent an instruction. More...

class	InstrSeq
	Instruction Sequencing does: More...

class	FuncObjRewrExpr
	Function object for rewriting Expr. More...

class	FuncObjRewrIla
	Function object for rewriting ILA tree. More...

class	FuncObjFlatIla
	Function object for flatten ILA tree. More...

class	Unroller
	Base class for unrolling ILA execution in different settings. More...

class	PathUnroll
	Application class for unrolling a path of instruction sequence. More...

class	MonoUnroll
	Application class for unrolling the ILA as a monolithic transition system. More...

class	UnrollerSmt
	Base class for unrolling ILA execution in different settings. More...

class	PathUnroller
	Application class for unrolling a sequence of instructions. More...

class	LegacyBmc
	Simplified bounded model checking engine for ILAs. 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	CompRefRel
	Compositional refinement relation defines a unit (element for the composition) of refinement relation, which specifies. More...

class	CommDiag
	Generator for commutating diagram-based equivalence checking. More...

class	SortRef
	The wrapper of Sort (type for different AST nodes). More...

class	ExprRef
	The wrapper of Expr (e.g. state var, var relation, constant, etc). More...

class	FuncRef
	The wrapper of Func (uninterpreted function). More...

class	InstrRef
	The wrapper of Instr (instruction). More...

class	Ila
	The wrapper of InstrLvlAbs (ILA). More...

class	IlaZ3Unroller
	The wrapper of generating z3::expr for verification. More...

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	NestedMemAddrDataAvoider
	Class of traversing to avoid nested memory access in address. More...

class	FunctionApplicationFinder
	Class of traversing to find the application of functions in an AST. 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	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	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	MemoryModel
	The base class for memory models. More...

class	ScTraceStep
	Class of TSO trace step. More...

class	Sc
	Class of TSO. More...

class	TsoTraceStep
	Class of TSO trace step. More...

class	Tso
	Class of TSO. More...

class	SynthAbsConverter
	The class for converting an abstraction from the synthesis engine to an ILA model. More...

class	I2JSer
	The class for serializing an ILA model to JSON format. More...

class	IlaSerDesMngr
	Class wrapper for the ILA portable Ser/Des interface. More...

class	J2IDes
	The class for deserializing an ILA model from JSON format. More...

class	IlaSim
	A class to generate SystemC simulator model from ILA model Example Use: More...

class	Ilator
	The ILAtor class - for CMake-based SystemC simulator generation. More...

class	SmtShim
	A templated class for wrapping z3 and smt-switch to provide a unified interface for different application, e.g., unroller. More...

class	Z3ExprAdapter
	The class for generating z3 expression from an ILA. More...

class	KeyVecIt
	A pseudo-iterator for the key-search vector. More...

class	KeyVec
	The container that support key search and index access. More...

class	MapSet
	A map for sets. More...

struct	execute_result
	the result from executing More...

class	LogInitter
	A one-time class for initializing GLog. More...

class	DebugLog
	The wrapper for enabling and disabling debug tags. 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	VerilogAnalyzer
	Class for Verilog analysis. More...

class	VerilogAnalyzerBase
	VerilogAnalyzerBase should never be instantiated, only used as a pointer type in class VerilogInfo. More...

class	SignalInfoBase
	Class to hold signal info. More...

class	VerilogInfo
	The class that invoke the analyzer. More...

class	VerilogConstantExprEval
	The class to convert a constant expr to an integer number. More...

class	VerilogGeneratorBase
	Base class of VerilogGenerator. More...

class	VerilogGenerator
	Class of Verilog Generator. More...

struct	VlgAbsMem
	a struct to store abstract memory More...

struct	DesignStatistics
	design statistics information More...

class	IntefaceDirectiveRecorder
	Used in Verilog Verification Target Generation for dealing with interface directives. More...

class	StateMappingDirectiveRecorder
	a class to handle state-mapping directives in the refinement relations More...

class	CexExtractor
	the class to extract counterexample from a vcd file More...

class	InvariantObject
	the invariant object, it needs smt-info to parse More...

struct	VlgTgtSupplementaryInfo
	the class to hold supplementary information More...

class	VarExtractor

class	VerilogModifier
	the class for modification to verilog More...

class	VlgVerifTgtGenBase
	VlgVerifTgtGenBase: do nothing, should not instantiate. More...

class	VerilogVerificationTargetGenerator

class	Cosa_problem
	a class to store (and generate) the problem for cosa More...

class	VlgSglTgtGen_Cosa
	a class to interface w. COSA More...

class	VlgSglTgtGen
	Generating a target (just the invairant or for an instruction) More...

class	VlgVerifTgtGen

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	Relchc_problem
	a class to store (and generate) the problem for Relchc (Z3) More...

class	VlgSglTgtGen_Relchc
	a class to interface w. Relchc Z3 More...

class	Yosys_problem
	a class to store (and generate) the problem for Yosys More...

class	VlgSglTgtGen_Yosys
	a class to interface w. Yosys 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, ExprHash >	ExprMap
	Type for mapping between Expr.

typedef std::unordered_set < ExprPtr, ExprHash >	ExprSet
	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 std::vector< z3::expr >	Z3ExprVec
	Vector type for z3 expression.

typedef std::shared_ptr < Z3ExprVec >	Z3ExprVecPtr
	Pointer for the z3 expression vector.

typedef KeyVec< Symbol, z3::expr >	Z3ExprMap
	Map type for z3 expression.

typedef std::shared_ptr < Z3ExprMap >	Z3ExprMapPtr
	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 Instr::InstrCnstPtr	InstrCnstPtr
	Pointer type for read-only use of Instr.

typedef std::vector< InstrPtr >	InstrVec
	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, InstrLvlAbsPtr >	CnstIlaMap
	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 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 uint64_t	NumericType
	Data type for numerics. NOTE: SHOULD BE SYNCED WITH BvValType!!

typedef SynthAbsConverter::SynthAbsConverterPtr	SynthAbsConverterPtr
	Pointer type for normal use of SynthAbsConverter.

typedef I2JSer::I2JSerPtr	I2JSerPtr
	Pointer type for normal use of I2JSer.

using	json = nlohmann::json

typedef J2IDes::J2IDesPtr	J2IDesPtr
	Pointer type for normal use of J2IDes.

typedef ExprHash	Z3AdapterHash
	The function object for hashing Expr in generating z3 expression.

typedef ExprHash	VerilogGenHash

Enumerations
enum	AstUidExprOp { kInvalid = 0, kNegate, kNot, kComplement, kAnd, kOr, kXor, kShiftLeft, kArithShiftRight, kLogicShiftRight, kAdd, kSubtract, kMultiply, kEqual, kLessThan, kGreaterThan, kUnsignedLessThan, kUnsignedGreaterThan, kLoad, kStore, kConcatenate, kExtract, kZeroExtend, kSignedExtend, kApplyFunc, kImply, kIfThenElse, kDivide, kRotateLeft, kRotateRight, kSignedRemainder, kUnsignedRemainder, kSignedModular }
	Unified ID for ExprOp.

enum	AstUidSort { kBool = 1, kBv, kMem }
	Unified ID for Sort.

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

enum	ExprTypeId { kVar = 1, kConst, kOp }
	ILA ser/des specific ID for Expr type.

enum	KeyVecItVal { END, FOUND }
	KeyVecItVal.

enum	redirect_t { NONE = 0, STDOUT = 1, STDERR = 2, BOTH = 3 }
	the type of redirect

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 ExprRef &b)
	Unsigned multiply for bit-vectors.

ExprRef	operator/ (const ExprRef &a, const ExprRef &b)
	Unsigned division 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 NumericType &b)
	Unsigned addition with constant.

ExprRef	operator- (const ExprRef &a, const NumericType &b)
	Unsigned subtraction with constant.

ExprRef	operator* (const ExprRef &a, const NumericType &b)
	Unsigned multiply with constant.

ExprRef	SRem (const ExprRef &a, const ExprRef &b)
	Arithmetic signed remainder.

ExprRef	URem (const ExprRef &a, const ExprRef &b)
	Arithmetic unsigned remainder.

ExprRef	SMod (const ExprRef &a, const ExprRef &b)
	Arithmetic signed modular.

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 NumericType &b)
	Equal to constant.

ExprRef	operator!= (const ExprRef &a, const NumericType &b)
	Not equal to constant.

ExprRef	operator< (const ExprRef &a, const NumericType &b)
	Signed/Unsigned less than constant (bit-vectors only).

ExprRef	operator> (const ExprRef &a, const NumericType &b)
	Signed/Unsigned greater than constant (bit-vectors only).

ExprRef	operator<= (const ExprRef &a, const NumericType &b)
	Signed/Unsigned less than or equal to constant (bit-vectors only).

ExprRef	operator>= (const ExprRef &a, const NumericType &b)
	Signed/Unsigned greater than or equal to constant (bit-vectors only).

ExprRef	Ult (const ExprRef &a, const NumericType &b)
	Unsigned less than constant (bit-vectors only).

ExprRef	Ugt (const ExprRef &a, const NumericType &b)
	Unsigned greater than constant (bit-vectors only).

ExprRef	Ule (const ExprRef &a, const NumericType &b)
	Unsigned less than or equal to constant (bit-vectors only).

ExprRef	Uge (const ExprRef &a, const NumericType &b)
	Unsigned greater than or equal to constant (bit-vectors only).

ExprRef	Slt (const ExprRef &a, const NumericType &b)
	Signed less than constant (bit-vectors only).

ExprRef	Sgt (const ExprRef &a, const NumericType &b)
	Signed greater than constant (bit-vectors only).

ExprRef	Sle (const ExprRef &a, const NumericType &b)
	Signed less than or equal to constant (bit-vectors only).

ExprRef	Sge (const ExprRef &a, const NumericType &b)
	Signed greater than or equal to 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 NumericType &addr)
	Load from memory with constant address.

ExprRef	Store (const ExprRef &mem, const NumericType &addr, const NumericType &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	LRotate (const ExprRef &bv, const int &immediate)
	Left-rotate the bit-vector with immediate number of times. More...

ExprRef	RRotate (const ExprRef &bv, const int &immediate)
	Right-rotate the bit-vector with immediate number of times. 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 NumericType &bv_val, const int &bit_width)
	Return a bit-vector constant. More...

ExprRef	MemConst (const NumericType &def_val, const std::map< NumericType, NumericType > &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.

bool	ExportIlaPortable (const Ila &ila, const std::string &file_name)
	Export the ILA portable to file. More...

Ila	ImportIlaPortable (const std::string &file_name)
	Import the ILA portable from file. More...

void	ExportSysCSim (const Ila &ila, const std::string &dir_path, bool optimize=false)
	Generate the SystemC simulator. More...

bool	getIteUnknownCondVal (const ExprPtr &e, ExprPtr &c, ExprPtr &v)
	Function to deal with Ite(c, v, apply(unknown) );.

z3::expr	Z3And (const z3::expr &a, const z3::expr &b)
	This is just a shortcut to be used for generated axiom.

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_exist (const std::string &path)
	Check if path exist.

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.

bool	os_portable_move_file_to_dir (const std::string &src, const std::string &dst)
	Move one file to the destination dir.

bool	os_portable_remove_file (const std::string &file)
	Remove one file.

bool	os_portable_remove_directory (const std::string &dir)
	Remove one directory.

std::string	os_portable_append_dir (const std::string &dir1, const std::string &dir2)
	Append two paths.

std::string	os_portable_append_dir (const std::string &dir1, const std::vector< std::string > &dirs)
	Append paths to another.

std::string	os_portable_join_dir (const std::vector< std::string > &dirs)
	Join paths.

std::string	os_portable_remove_file_name_extension (const std::string &fname)
	C:\a.txt -> C:\a or /a/b/c.txt -> a/b/c.

execute_result	os_portable_execute_shell (const std::vector< std::string > &cmdargs, const std::string &redirect_output_file="", redirect_t rdt=redirect_t::BOTH, unsigned timeout=0, const std::string &pid_file_name="")

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

std::string	os_portable_path_from_path (const std::string &path)

std::string	os_portable_read_last_line (const std::string &filename)
	read the last meaningful line from a file

bool	os_portable_chdir (const std::string &dirname)
	Change current directory: true if success.

std::string	os_portable_getcwd ()
	Get the current directory.

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	IntToStrCustomBase (uint64_t value, unsigned base, bool uppercase)
	Transform int to string with different bases.

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".

long long	StrToLong (const std::string &str, int base=10)
	Return the value represented in the string in long type, e.g. "10".

unsigned long long	StrToULongLong (const std::string &str, int base=10)
	Return the value represented in the string in unsigned long long, e.g. "10".

void	StrLeftTrim (std::string &s)
	Trim a string from start (in place)

void	StrRightTrim (std::string &s)
	Trim a string from end (in place)

void	StrTrim (std::string &s)
	Trim a string from both ends (in place)

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	RemoveWhiteSpace (const std::string &in)
	Remove whitespace " \n\t\r\f\v" from the input string.

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 ()

bool	StrEndsWith (const std::string &str, const std::string &suffix)
	Finds out if str ends with suffix.

bool	StrStartsWith (const std::string &str, const std::string &prefix)
	Finds out if str starts with prefix.

BvValType	Z3BvVal (const BvValType &bv_val)
	Interface z3 bit-vector constant numeric.

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	Z3SRem (z3::context &ctx, const z3::expr &a, const z3::expr &b)
	Interface z3 shl ast node construction.

z3::expr	Z3URem (z3::context &ctx, const z3::expr &a, const z3::expr &b)
	Interface z3 shl ast node construction.

z3::expr	Z3SMod (z3::context &ctx, const z3::expr &a, const z3::expr &b)
	Interface z3 shl 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.

z3::expr	Z3LRotate (z3::context &ctx, z3::expr &e, unsigned &w)
	Interface z3 left rotate ast node construction.

z3::expr	Z3RRotate (z3::context &ctx, z3::expr &e, unsigned &w)
	Interface z3 right rotate 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

int	TestParseVerilogFrom (const std::string &fn)

std::string	_ast_identifier_tostring (ast_identifier id)
	A wrapper of the ast_identifier_tostring method with basic string type.

Detailed Description

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

Function Documentation

ExprRef ilang::BoolConst ( bool bool_val )

Return a Boolean constant.

Parameters

[in] bool_val value of the Boolean constant.

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

Return a bit-vector constant.

Parameters

[in]	bv_val	value of the bit-vector constant.
[in]	bit_width	data bit-width.

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

Concatenate two bit-vectors.

Parameters

[in]	msbv	bit-vector on the more-significant side.
[in]	lsbv	bit-vector on the less-significant side.

bool ilang::ExportIlaPortable	(	const Ila &	ila,
		const std::string &	file_name
	)

Export the ILA portable to file.

Parameters

[in]	ila	the source ILA model to export.
[in]	file_name	the name of the exported ILA portable (JSON) file.

void ilang::ExportSysCSim	(	const Ila &	ila,
		const std::string &	dir_path,
		bool	optimize = `false`
	)

Generate the SystemC simulator.

Parameters

[in]	ila	the top-level ILA to generate.
[in]	dir_path	directory path of the generated simulator.
[in]	optimize	set true to enable optimization.

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

Extract bit-field in the bit-vector.

Parameters

[in]	bv	source bit-vector.
[in]	hi	the index of the most-significant bit.
[in]	lo	the index of the least-significant bit.

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

Logical imply for Booleans.

Parameters

[in]	ante	antecedent for the operator.
[in]	cons	consequent for the operator.

Ila ilang::ImportIlaPortable ( const std::string & file_name )

Import the ILA portable from file.

Parameters

[in] file_name the name of the ILA portable (JSON) file to import.

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_name	file name of the abstraction from the synthesis engine.
[in]	ila_name	name of the created ILA model.

Returns: the generated ILA model.

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_name	file name of the abstraction from the synthesis engine.
[in]	parent	pointer to the parent ILA.
[in]	ila_name	name of the created ILA model.

Returns: the generated ILA model.

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

If-then-else on the Boolean condition.

Parameters

[in]	cond	Boolean type condition.
[in]	t	Expression to take when the condition is true.
[in]	f	Expression to take when the condition is false.

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

ExprRef ilang::LRotate	(	const ExprRef &	bv,
		const int &	immediate
	)

Left-rotate the bit-vector with immediate number of times.

Parameters

[in]	bv	source bit-vector
[in]	immediate	number of times to rotate the bv

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

Return a memory constant.

Parameters

[in]	def_val	default value.
[in]	vals	non-default address-data mapping.
[in]	addr_width	address bit-width.
[in]	data_width	data bit-width.

execute_result ilang::os_portable_execute_shell	(	const std::vector< std::string > &	cmdargs,
		const std::string &	redirect_output_file = `""`,
		redirect_t	rdt = `redirect_t::BOTH`,
		unsigned	timeout = `0`,
		const std::string &	pid_file_name = `""`
	)

execute some executables that are shell scripts, timeout (if 0 will wait forever)

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

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

Extract path from path C: .txt -> "C:\a\b\ something " C: -> C: d/e/ghi -> "d/e/"

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

ExprRef ilang::RRotate	(	const ExprRef &	bv,
		const int &	immediate
	)

Right-rotate the bit-vector with immediate number of times.

Parameters

[in]	bv	source bit-vector
[in]	immediate	number of times to rotate the bv

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

Extract single bit in the bit-vector.

Parameters

[in]	bv	source bit-vector.
[in]	idx	the index of the selected bit.

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

void ilang::SetUnsignedComparison ( bool sign )

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

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

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

Parameters

[in]	bv	source bit-vector.
[in]	length	bit-width of the extended (result) bit-vector.

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

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

Parameters

[in]	bv	source bit-vector.
[in]	length	bit-width of the extended (result) bit-vector.

Classes

Typedefs

Enumerations

Functions

Detailed Description

Function Documentation