|
ilang
1.1.4
ILAng: A Modeling and Verification Platform for SoCs
|
|
ilang
1.1.4
ILAng: A Modeling and Verification Platform for SoCs
|
Class of TSO trace step. More...
#include <tso_manual.h>
Public Types | |
|
typedef std::shared_ptr < TraceStep > | TraceStepPtr |
| Type of trace step pointer. | |
 Public Types inherited from ilang::TraceStep | |
| enum | TraceStepType { INST_EVT, FACET_EVT, INIT_EVT, FINAL_EVT } |
| The type of trace step type. | |
| typedef z3::expr | ZExpr |
| Type alias for z3::expr. | |
| typedef std::vector< ZExpr > | ZExprVec |
| Type for containing a set of z3::expr. | |
|
typedef std::shared_ptr < TraceStep > | TraceStepPtr |
| Type of trace step pointer. | |
| typedef std::set< TraceStepPtr > | TraceStepPtrSet |
| Type of set of trace steps. | |
| typedef std::set< std::string > | StateNameSet |
| Type of state name set. | |
|
typedef std::vector< std::pair < ExprPtr, ExprPtr > > | AddrDataVec |
| Type of (addr,data) pair vector. | |
|
typedef std::unordered_map < std::string, AddrDataVec > | MRFVal |
| Map from state name to memory read pair. | |
Public Member Functions | |
| TsoTraceStep (const InstrPtr &inst, ZExprVec &cstr, z3::context &ctx, size_t pos) | |
| To create a trace step (for inst, we don't need it for facet/init) | |
| Public Member Functions inherited from ilang::TraceStep | |
| InstrLvlAbsPtr | host () const |
| Return the host ILA. | |
| std::string | name () const |
| Return the name. | |
| const StateNameSet & | get_inst_read_set () const |
| Return the set of states read by inst/parent-inst. | |
| const StateNameSet & | get_inst_write_set () const |
| Return the set of states written by inst/parent-inst. | |
| const TraceStepType & | type () const |
| Return the type of the trace step. | |
| bool | is_init_tracestep () const |
| Decide if the trace step is the initial trace step (a short-cut) | |
| bool | is_facet_tracestep () const |
| Decide if the trace step is the facet trace step (a short-cut) | |
| bool | is_final_tracestep () const |
| Decide if the trace step is the facet trace step (a short-cut) | |
| InstrPtr | inst () const |
| Return the associated instruction for facet / instruction event. | |
| size_t | pos_suffix () const |
| Z3ExprAdapter & | z3adapter () const |
| Return the adapter. | |
| z3::context & | ctx () |
| Return the context (for variable creation) | |
| ExprPtr | final_property () |
| Return final property. | |
| TraceStep (const InstrPtr &inst, ZExprVec &cstr, z3::context &ctx, size_t pos) | |
| TraceStep (const InstrPtr &inst, ZExprVec &cstr, z3::context &ctx, ZExpr _ts_overwrite, size_t pos) | |
| TraceStep (const InstrPtr &ref_inst, ZExprVec &cstr, z3::context &ctx, const std::string &fevt_name, size_t pos) | |
| To create a facet event: FACET_EVT. | |
| TraceStep (const ExprPtr &property, ZExprVec &cstr, z3::context &ctx, const InstrLvlAbsPtr &host) | |
| To create a final event: FINAL_EVT. | |
| virtual | ~TraceStep () |
| Destructor, make it virtual. | |
| void | AddStateAccess (const std::string &name, AccessType acc_type) |
| To update the set for FACET_EVT. | |
| void | AddStateAccess (const StateNameSet &s, AccessType acc_type) |
| To update the set for FACET_EVT. | |
| ZExpr | ConvertZ3OnThisStep (const ExprPtr &ast) const |
| bool | Access (AccessType acc_type, const std::string &name) const |
| To determine if the instruction READ/WRITE a certain state. | |
| bool | Access (AccessType acc_type, const StateNameSet &stateset) const |
| To determine if the instruction READ/WRITE a certain set. | |
| std::string | Print (z3::model &m) const |
| Print out a trace step for debug purpose. | |
Public Attributes | |
| TraceStepPtr | wfe_global |
Additional Inherited Members | |
| Protected Attributes inherited from ilang::TraceStep | |
| TraceStepType | _type |
| the type of this trace step (event) | |
| InstrPtr | _inst |
| The pointer to the instruction executed in this step. | |
| InstrPtr | _parent_inst |
| The pointer to the referred instruction. | |
| StateNameSet | _read_state_set |
| StateNameSet | _write_state_set |
| StateNameSet | _inst_read_set |
| Set of states (that are read by inst or parent-inst) | |
| StateNameSet | _inst_write_set |
| Set of states (that are written by inst or parent-inst) | |
| ZExprVec & | _cstr |
| std::string | _name |
| The name of trace step. | |
| z3::expr | timestamp |
| The time stamp. | |
| size_t | _pos_suffix |
| The relative position. | |
| Z3ExprAdapter | _expr2z3_ |
| Keep an adapter that trace steps (won't shared w. others) | |
| z3::context & | _ctx_ |
| Keep a context to allocate z3 vars. | |
| InstrLvlAbsPtr | _host_final_ |
| Host for Final Event. | |
| ExprPtr | _final_property |
| The cache for the property to witness on the final step. | |
Class of TSO trace step.
1.8.5
