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

Application class for unrolling a path of instruction sequence. More...

#include <unroller.h>

Inheritance diagram for ilang::PathUnroll:
ilang::Unroller

Public Types

typedef std::vector< InstrPtrInstrVec
 Type of a list of instruction sequence.
 
- Public Types inherited from ilang::Unroller
typedef z3::expr ZExpr
 Type alias for z3::expr.
 
typedef z3::expr_vector ZExprVec
 Type for containing a set of z3::expr.
 
typedef ExprPtrVec IExprVec
 Type alias for a set of ExprPtr.
 

Public Member Functions

 PathUnroll (z3::context &ctx, const std::string &suff="")
 Default constructor.
 
 ~PathUnroll ()
 Default destructor.
 
ZExpr PathSubs (const std::vector< InstrPtr > &seq, const int &pos=0)
 Unroll a sequence of instructions with internal states substituted. More...
 
ZExpr PathAssn (const std::vector< InstrPtr > &seq, const int &pos=0)
 Unroll a sequence of instructions while asserting states are equal between each step. More...
 
ZExpr PathNone (const std::vector< InstrPtr > &seq, const int &pos=0)
 Unroll a sequence of instructions without asserting states relations between steps. "N(var_i) == var_i.nxt_suff". More...
 
- Public Member Functions inherited from ilang::Unroller
 Unroller (z3::context &ctx, const std::string &suffix)
 Default constructor.
 
virtual ~Unroller ()
 Default virtual destructor.
 
void AddGlobPred (const ExprPtr p)
 Add a predicate that should be asserted globally.
 
void AddInitPred (const ExprPtr p)
 Add a predicate that should be asserted in the initial condition.
 
void AddStepPred (const ExprPtr p, const int &k)
 Add a predicate that should be asserted at the k-th step.
 
void ClearGlobPred ()
 Clear the global predicates.
 
void ClearInitPred ()
 Clear the initial predicates.
 
void ClearStepPred ()
 Clear the step-specific predicates.
 
void ClearPred ()
 Clear all predicates.
 
ZExpr CurrState (const ExprPtr v, const int &t)
 Return the z3::expr representing the current state at the time.
 
ZExpr NextState (const ExprPtr v, const int &t)
 Return the z3::expr representing the next state at the time.
 
ZExpr GetZ3Expr (const ExprPtr e, const int &t)
 Return the z3::expr representing the current-based Expr at the time.
 
ZExpr GetZ3Expr (const ExprPtr e)
 Return the z3::expr representing a unique Expr (regardless of time).
 
ZExpr Equal (const ExprPtr va, const int &ta, const ExprPtr vb, const int &tb)
 Return the z3::expr representing a and b are equal at their time.
 

Protected Member Functions

void DefineDepVar ()
 [Application-specific] Define dependant state variables. More...
 
void Transition (const int &idx)
 [Application-specific] Define next state update functions. More...
 
- Protected Member Functions inherited from ilang::Unroller
ZExpr UnrollSubs (const size_t &len, const int &pos)
 Unroll while substituting internal expression.
 
ZExpr UnrollAssn (const size_t &len, const int &pos, bool cache=false)
 Unroll without substituting internal expression.
 
ZExpr UnrollNone (const size_t &len, const int &pos)
 Unroll without asserting state equality between each step.
 

Additional Inherited Members

- Static Protected Member Functions inherited from ilang::Unroller
static ExprPtr StateUpdCmpl (const InstrPtr instr, const ExprPtr var)
 Return the state update function (unchanged if not defined).
 
static ExprPtr DecodeCmpl (const InstrPtr instr)
 Return the decode function (true if not defined).
 
static ExprPtr NewFreeVar (const ExprPtr var, const std::string &name)
 Create a new free variable (with same sort) under the same host.
 
- Protected Attributes inherited from ilang::Unroller
IExprVec vars_
 The set of dependant state variables.
 
IExprVec k_pred_
 The set of predicates to be asserted of each step.
 
IExprVec k_next_
 The set of state update functions of each step.
 

Detailed Description

Application class for unrolling a path of instruction sequence.

Member Function Documentation

◆ DefineDepVar()

void ilang::PathUnroll::DefineDepVar ( )
protectedvirtual

[Application-specific] Define dependant state variables.

  • "vars_" should be assigned with the state vars uniquely.
  • "vars_" will be cleared before caling this function. = The var order stored in "vars_" will be the globally agree-upon order.

Implements ilang::Unroller.

◆ PathAssn()

ZExpr ilang::PathUnroll::PathAssn ( const std::vector< InstrPtr > &  seq,
const int &  pos = 0 
)

Unroll a sequence of instructions while asserting states are equal between each step.

Parameters
[in]seqthe sequence of instructions.
[in]posthe starting time frame.

◆ PathNone()

ZExpr ilang::PathUnroll::PathNone ( const std::vector< InstrPtr > &  seq,
const int &  pos = 0 
)

Unroll a sequence of instructions without asserting states relations between steps. "N(var_i) == var_i.nxt_suff".

Parameters
[in]seqthe sequence of instructions.
[in]posthe starting time frame.

◆ PathSubs()

ZExpr ilang::PathUnroll::PathSubs ( const std::vector< InstrPtr > &  seq,
const int &  pos = 0 
)

Unroll a sequence of instructions with internal states substituted.

Parameters
[in]seqthe sequence of instructions.
[in]posthe starting time frame.

◆ Transition()

void ilang::PathUnroll::Transition ( const int &  idx)
protectedvirtual

[Application-specific] Define next state update functions.

  • "k_next_" should be assigned with the next state expression.
  • "k_next_" follows the global order as stored in "vars_".
  • "k_next_" will NOT be cleared before calling (is the only modifier).
  • "k_pred_" can be used to store step-specific predicates, e.g. decode.
  • "k_pred_" will NOT be cleared before calling (is the only modifier).

Implements ilang::Unroller.


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