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

Class of TSO. More...

#include <sc_manual.h>

Inheritance diagram for ilang::Sc:
ilang::MemoryModel

Public Types

typedef std::shared_ptr< ScTraceStepScTraceStepPtr
 Type of trace step pointer.
 
typedef std::set< ScTraceStepPtrScTraceStepPtrSet
 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.
 
 Sc (z3::context &ctx, ZExprVec &_cstrlist, const StateNameSet &shared_states, const ILANameStateNameSetMap &private_states, const InstrLvlAbsPtr &global_ila_ptr)
 Constructor.
 
- 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 ScModel
 Declaration of memory model creator that chooses Sc.
 

Protected Attributes

TraceStepPtrSet WRITE_list
 
TraceStepPtrSet READ_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_
 
ZExprVec_constr
 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  StaticResult { STATIC_TRUE = 1, STATIC_FALSE, STATIC_UNKNOWN }
 
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::Sc::FinishRegisterSteps ( )
overridevirtual

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

Implements ilang::MemoryModel.

◆ RegisterSteps()

virtual void ilang::Sc::RegisterSteps ( size_t  regIdx,
const InstrVec _inst_seq 
)
overridevirtual

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: