Class Hierarchy

This inheritance list is sorted roughly, but not completely, alphabetically:

[detail level 1234]

ilang::VlgVerifTgtGenBase::_adv_parameters
ilang::VlgVerifTgtGenBase::_vtg_config	Verilog Target Generation Configuration
ilang::smt::arg_t	Argument used in a function def
ilang::CexExtractor	Class to extract counterexample from a vcd file
ilang::CommDiag	Generator for commutating diagram-based equivalence checking
ilang::CompRefRel	Compositional refinement relation defines a unit (element for the composition) of refinement relation, which specifies
ilang::Cosa_problem	Class to store (and generate) the problem for cosa
ilang::DebugLog	The wrapper for enabling and disabling debug tags
ilang::DesignStatistics	Design statistics information
enable_shared_from_this
ilang::Expr	The class for expression, which is the basic type for variables, constraints, state update expressions, etc
ilang::ExprConst	Expression for constant values (bool, bv, or memory). Constant should be terminating nodes in the AST
ilang::ExprOp	Expression for operations, e.g. AND, OR, ADD, etc. Operations are non-terminating nodes in the AST
ilang::ExprOpAdd	The wrapper for unsigned addition
ilang::ExprOpAnd	The wrapper for binary logical AND operation "&"
ilang::ExprOpAppFunc	The class wrapper for apply uninterpreted function
ilang::ExprOpAshr	The wrapper for arithmetic right shifting a bit-vector
ilang::ExprOpCompl	The wrapper for unary bit-wise complement "~". (bv only)
ilang::ExprOpConcat	The class wrapper for bitvector concatenation
ilang::ExprOpDiv	The wrapper for unsigned division
ilang::ExprOpEq	The class wrapper for binary comparison EQ "=="
ilang::ExprOpExtract	The class wrapper for bitvector extraction
ilang::ExprOpGt	The class wrapper for binary comparison signed greater than ">"
ilang::ExprOpImply	The class wrapper for logical imply
ilang::ExprOpIte	The class wrapper for if-then-else
ilang::ExprOpLoad	The class wrapper for memory load
ilang::ExprOpLRotate	The class wrapper for left-rotate
ilang::ExprOpLshr	The wrapper for logical right shifting a bit-vector
ilang::ExprOpLt	The class wrapper for binary comparison signed less than "<"
ilang::ExprOpMul	The wrapper for unsigned multiplication
ilang::ExprOpNeg	The wrapper for unary negate operation "-"
ilang::ExprOpNot	The wrapper for unary not operation "!". (bool only)
ilang::ExprOpOr	The wrapper for binary logical OR operation "|"
ilang::ExprOpRRotate	The class wrapper for right-rotate
ilang::ExprOpSExt	The class wrapper for sign-extend
ilang::ExprOpShl	The wrapper for left shifting a bit-vector
ilang::ExprOpSMod	The wrapper for signed remainder
ilang::ExprOpSRem	The wrapper for signed remainder
ilang::ExprOpStore	The class wrapper for memory store
ilang::ExprOpSub	The wrapper for unsigned subtraction
ilang::ExprOpUgt	The class wrapper for binary comparison unsigned greater than
ilang::ExprOpUlt	The class wrapper for binary comparison unsigned less than
ilang::ExprOpURem	The wrapper for unsigned remainder
ilang::ExprOpXor	The wrapper for binary logical XOR operation "^"
ilang::ExprOpZExt	The class wrapper for zero-extend
ilang::ExprVar	Expression for variables (bool, bv, or mem). Variable should be the terminating nodes in the AST
ilang::InstrLvlAbs	The class of Instruction-Level Abstraction (ILA). An ILA contains:
ilang::VlgVerifTgtGenBase::ex_info_t
ilang::execute_result	Result from executing
ilang::ExprHash	The function object for hashing Expr. The hash value is the id of the symbol, which is supposed to be unique
ilang::ExprMngr	Simplifier for AST trees by sharing nodes based on the hash value
ilang::ExprRef	The wrapper of Expr (e.g. state var, var relation, constant, etc)
ilang::FuncHash	The function object for hashing Func. The hash value is the id of the symbol, which is supposed to be unique
ilang::FuncObjFlatIla	Function object for flatten ILA tree
ilang::FuncObjRewrExpr	Function object for rewriting Expr
ilang::FuncObjRewrIla	Function object for rewriting ILA tree
ilang::FuncRef	The wrapper of Func (uninterpreted function)
ilang::VerilogGeneratorBase::function_app_t	Type of app func
ilang::FunctionApplicationFinder	Class of traversing to find the application of functions in an AST
ilang::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!
ilang::I2JSer	The class for serializing an ILA model to JSON format
ilang::Ila	The wrapper of InstrLvlAbs (ILA)
ilang::IlaSerDesMngr	Class wrapper for the ILA portable Ser/Des interface
ilang::IlaSim	A class to generate SystemC simulator model from ILA model Example Use:
ilang::Ilator	The ILAtor class - for CMake-based SystemC simulator generation
ilang::IlaZ3Unroller	The wrapper of generating z3::expr for verification
ilang::InstrRef	The wrapper of Instr (instruction)
ilang::InstrSeq	Instruction Sequencing does:
ilang::InstrTranEdge	Instruction transition edge, includeing:
ilang::InstrTranNode	Node for instruction-transition node, each node represent an instruction
ilang::IntefaceDirectiveRecorder	Used in Verilog Verification Target Generation for dealing with interface directives
ilang::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
ilang::InvariantObject	Invariant object, it needs smt-info to parse
ilang::J2IDes	The class for deserializing an ILA model from JSON format
ilang::KeyVec< Key, T >	The container that support key search and index access
ilang::KeyVec< Symbol, ExprPtr >
ilang::KeyVec< Symbol, InstrLvlAbsPtr >
ilang::KeyVec< Symbol, InstrPtr >
ilang::KeyVecIt< Key, T >	A pseudo-iterator for the key-search vector
ilang::IlaSim::ld_info	TODO
ilang::LegacyBmc	Simplified bounded model checking engine for ILAs
ilang::LogInitter	A one-time class for initializing GLog
ilang::MapSet< Key, T >	A map for sets
ilang::VerilogGeneratorBase::mem_write_entry_t	This is type of an individual write
ilang::VerilogGeneratorBase::mem_write_t	This is the write and its associated condition
ilang::MemoryModel	The base class for memory models
ilang::Sc	Class of TSO
ilang::Tso	Class of TSO
ilang::NestedMemAddrDataAvoider	Class of traversing to avoid nested memory access in address
ilang::Object	The basest type in the ILA structure. It can be either Ast, Instr, or InstrLvlAbs
ilang::Ast	The class for the Abstract Syntax Tree. An Ast object can be an expression or function definition (interpreted or uninterpreted)
ilang::Expr	The class for expression, which is the basic type for variables, constraints, state update expressions, etc
ilang::Func	The class for uninterpreted function
ilang::Sort	The class for sort (type for expr, and the range/domain of functions)
ilang::SortBool	The class of Boolean Sort
ilang::SortBv	The class of bit-vector Sort
ilang::SortMem	The class of memory (array) Sort
ilang::Instr	The class for the Instruction. An Instr object contains:
ilang::InstrLvlAbs	The class of Instruction-Level Abstraction (ILA). An ILA contains:
ilang::RefinementMap	Refinement mapping defines how to map micro-architectural states to architectural states for comparison
ilang::RelationMap	Relation mapping defines how arch states of two models are mapped, i.e., state mapping
ilang::Relchc_problem	Class to store (and generate) the problem for Relchc (Z3)
ilang::VlgTgtSupplementaryInfo::reset_config_t
ilang::VerilogGeneratorBase::rport_t	Type of read port
ilang::SignalInfoBase	Class to hold signal info
ilang::SignalInfoPort	Class to convert port to signal info
ilang::SignalInfoReg	Class to convert reg to signal info
ilang::SignalInfoWire	Class to convert wire to signal info
ilang::smt::smt_file	Class that holds the whole file
ilang::smt::smt_item
ilang::smt::func_def_t	Function
ilang::smt::line_comment
ilang::smt::smtlib2_abstract_parser_wrapper	Wrapper of the abstract parser so it is okay to do crazy stuff
ilang::smt::SmtlibInvariantParserBase	This a base class, should not be instantiated
ilang::smt::SmtlibInvariantParser	Class for parsing invariant
ilang::smt::SmtlibInvariantParserInstance	This a base class, should not be instantiated
ilang::SmtShim< Generator >	A templated class for wrapping z3 and smt-switch to provide a unified interface for different application, e.g., unroller
ilang::smt::SmtTermInfo< T >	Type of term info that needs to be carried
ilang::SortRef	The wrapper of Sort (type for different AST nodes)
ilang::IlaSim::st_info	TODO
ilang::VerilogGeneratorBase::state_update_unknown	Type of ite update unknown
ilang::smt::state_var_t	And item in declare-datatype
ilang::StateMappingDirectiveRecorder	Class to handle state-mapping directives in the refinement relations
ilang::smt::str_iterator	String iterator
ilang::Symbol	The symbol is the name and ID of an object. Every object has an unique symbol
ilang::SynthAbsConverter	The class for converting an abstraction from the synthesis engine to an ILA model
ilang::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
ilang::ScTraceStep	Class of TSO trace step
ilang::TsoTraceStep	Class of TSO trace step
ilang::Unroller	Base class for unrolling ILA execution in different settings
ilang::MonoUnroll	Application class for unrolling the ILA as a monolithic transition system
ilang::PathUnroll	Application class for unrolling a path of instruction sequence
ilang::UnrollerSmt< Generator >	Base class for unrolling ILA execution in different settings
ilang::PathUnroller< Generator >	Application class for unrolling a sequence of instructions
ilang::Value	The base type for constant value
ilang::BoolVal	The container for representing Boolean values
ilang::BvVal	The container for representing Bitvector values
ilang::MemVal	The container for representing memory (array) values
ilang::smt::var_type	Type Bool or (_ BitVec)
ilang::VarExtractor
ilang::VarUseFinder< T >	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
ilang::VerilogAnalyzerBase	VerilogAnalyzerBase should never be instantiated, only used as a pointer type in class VerilogInfo
ilang::VerilogAnalyzer	Class for Verilog analysis
ilang::VerilogConstantExprEval	The class to convert a constant expr to an integer number
ilang::VerilogGeneratorBase	Base class of VerilogGenerator
ilang::VerilogGenerator	Class of Verilog Generator
ilang::VerilogInfo	The class that invoke the analyzer
ilang::VerilogModifier	Class for modification to verilog
ilang::VerilogVerificationTargetGenerator
ilang::VlgAbsMem	Struct to store abstract memory
ilang::VerilogGeneratorBase::VlgGenConfig	Structure to configure the verilog generator
ilang::VlgSglTgtGen	Generating a target (just the invairant or for an instruction)
ilang::VlgSglTgtGen_Cosa	Class to interface w. COSA
ilang::VlgSglTgtGen_Jasper	Verilog Verification Target Generator – for JasperGold Unlike for cosa, we don't need a separate file although we do have some ..
ilang::VlgSglTgtGen_Relchc	Class to interface w. Relchc Z3
ilang::VlgSglTgtGen_Yosys	Class to interface w. Yosys
ilang::VlgTgtSupplementaryInfo	Class to hold supplementary information
ilang::VlgVerifTgtGenBase	VlgVerifTgtGenBase: do nothing, should not instantiate
ilang::VlgVerifTgtGen
ilang::VerilogGeneratorBase::wport_t	Type of write port
ilang::Yosys_problem	Class to store (and generate) the problem for Yosys
ilang::smt::YosysSmtParser	To parse an smt file this will only work on the yosys's generated smt and not on the assembled CHC
ilang::Z3ExprAdapter	The class for generating z3 expression from an ILA