ilang  1.0.2
ILAng: A Modeling and Verification Platform for SoCs
Public Types | Public Member Functions | Static Public Attributes | Protected Attributes | List of all members
ilang::Tso Class Reference

Class of TSO. More...

#include <tso_manual.h>

Inheritance diagram for ilang::Tso:

Public Types

typedef std::shared_ptr< TsoTraceStepTsoTraceStepPtr
 Type of trace step pointer.
typedef std::set< TsoTraceStepPtrTsoTraceStepPtrSet
 Type of trace steps, we need to collect the set of trace steps (WRITE)
- Public Types inherited from ilang::MemoryModel
using ZExpr = TraceStep::ZExpr
 Type alias for z3::expr.
using ZExprVec = TraceStep::ZExprVec
 Type for containing a vector of z3::expr.
using TraceStepPtr = TraceStep::TraceStepPtr
 Type of trace step shared pointers.
using TraceStepPtrSet = TraceStep::TraceStepPtrSet
 Type of trace steps, we need to collect the set of trace steps (WRITE)
using TraceStepType = TraceStep::TraceStepType
 Type of trace step type, INIT/INST/FACET.
using StateNameSet = TraceStep::StateNameSet
 Type of set of state names.
using AddrDataVec = TraceStep::AddrDataVec
 Type of vector of (addr,data) pair.
typedef std::vector< InstrPtrInstrVec
 Type of an instruction vector to represent a sequence.
typedef std::vector< InstrVecProgramTemplate
typedef std::vector< std::vector< TraceStepPtr > > PerILATraceStepPtrSet
typedef std::map< std::string, StateNameSetILANameStateNameSetMap
 Type of map ila-name to state-set.

Public Member Functions

virtual void RegisterSteps (size_t regIdx, const InstrVec &_inst_seq) override
virtual void FinishRegisterSteps () override
virtual void ApplyAxioms () override
 To apply the axioms, the complete program should be given.
virtual void SetFinalProperty (const ExprPtr &property) override
 Set the final property, this is implementation-specific.
 Tso (z3::context &ctx, ZExprVec &_cstrlist, const StateNameSet &shared_states, const ILANameStateNameSetMap &private_states, const InstrLvlAbsPtr &global_ila_ptr)
- Public Member Functions inherited from ilang::MemoryModel
ZExpr ConvertZ3 (const ExprPtr &ast, const std::string &suffix) const
 Return the z3 converter used by this memory model.
virtual void InitSize (const ProgramTemplate &_tmpl)
 To initialize the inner storage space.
virtual void SetLocalState (const std::vector< bool > &ordered)
virtual void AddSingleTraceStepProperty (const ExprPtr &property, std::function< bool(const TraceStep &)> filter)
 Assert a property that some trace step (decided by filter) should follow.
virtual void GetSingleTraceStepProperty (const ExprPtr &property, std::function< bool(const TraceStep &)> filter, std::function< void(const z3::expr &)> collector)
 Get the z3 expression of a property on a trace step.
virtual void AddDoubleTraceStepProperty (std::function< z3::expr(const TraceStep &, const TraceStep &)>, std::function< bool(const TraceStep &, const TraceStep &)>)
 MemoryModel (z3::context &ctx, ZExprVec &_cstrlist, const StateNameSet &shared_states, const ILANameStateNameSetMap &private_states, const InstrLvlAbsPtr &global_ila_ptr)
const TraceStepPtrSetGetAllTraceSteps () const
 Determine if an instruction access a shared state.

Static Public Attributes

static InterIlaUnroller::MemoryModelCreator TsoModel
 Declaration of memory model creator that chooses Tso.

Protected Attributes

TraceStepPtrSet WRITE_list
TraceStepPtrSet READ_list
TraceStepPtrSet FENCE_list
TraceStepPtrSet RMW_list
TraceStepPtrSet PureWrite_list
- Protected Attributes inherited from ilang::MemoryModel
TraceStepPtr _init_trace_step
 The pointer to the initial trace step.
TraceStepPtr _final_trace_step
 The pointer to the final trace step.
TraceStepPtrSet _all_trace_steps
 The set of all trace steps.
TraceStepPtrSet _all_inst_trace_steps
 The set of all instruction trace steps.
PerILATraceStepPtrSet _ila_trace_steps
const StateNameSetm_shared_state_names
 The set of names of shared states.
const ILANameStateNameSetMapm_ila_private_state_names
 The internal storage of all private states of all ilas.
InstrLvlAbsPtr m_p_global_ila
 The pointer to the (dummy) global ILA.
z3::context & _ctx_
 A reference to the constraint list.
Z3ExprAdapter _expr2z3_
NestedMemAddrDataAvoider nested_finder_
 An AST traversor, make sure there are no nested asts.

Additional Inherited Members

- Protected Types inherited from ilang::MemoryModel
enum  AxiomFuncHint { HINT_NONE = 0, HINT_READ = 1, HINT_WRITE }
- Protected Member Functions inherited from ilang::MemoryModel
z3::context & ctx () const
 Return the context (for variable creation)
TraceStepPtr CreateGlobalInitStep ()
 A function for dervied classes to create init trace step.
TraceStepPtr CreateGlobalFinalStep (const ExprPtr &property)
 A function for dervied classes to create final trace step.
z3::expr HB (const TraceStep &l, const TraceStep &r) const
z3::expr Sync (const TraceStep &l, const TraceStep &r) const
z3::expr PO (const TraceStep &l, const TraceStep &r) const
z3::expr SameAddress (const TraceStep &l, const TraceStep &r, const std::string &sname, AxiomFuncHint lhint=HINT_NONE, AxiomFuncHint rhint=HINT_NONE) const
z3::expr Decode (const TraceStep &l) const
z3::expr SameData (const TraceStep &l, const TraceStep &r, const std::string &sname, AxiomFuncHint lhint=HINT_NONE, AxiomFuncHint rhint=HINT_NONE) const
bool SameCore (const TraceStep &l, const TraceStep &r) const
StaticResult SameAddressStatic (const TraceStep &l, const TraceStep &r) const
StaticResult DecodeStatic (const TraceStep &l) const
StaticResult SameCoreStatic (const TraceStep &l, const TraceStep &r) const
z3::expr Z3ForallList (const ZExprVec &l) const
 This is to deal with forall (if does not exist, it should be true also)
z3::expr Z3ExistsList (const ZExprVec &l) const
 This is to apply to exists, (if does not exist, it should be false)

Detailed Description

Class of TSO.

Member Function Documentation

◆ FinishRegisterSteps()

virtual void ilang::Tso::FinishRegisterSteps ( )

To do some extra bookkeeping work when it is known that no more instruction steps are needed.

Implements ilang::MemoryModel.

◆ RegisterSteps()

virtual void ilang::Tso::RegisterSteps ( size_t  regIdx,
const InstrVec _inst_seq 

To create more view operations associated with an instruction, and also to add them to the set

Implements ilang::MemoryModel.

The documentation for this class was generated from the following file: