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