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

Application class for unrolling the ILA as a monolithic transition system. More...

#include <unroller.h>

Inheritance diagram for ilang::MonoUnroll:
ilang::Unroller

Public Member Functions

 MonoUnroll (z3::context &ctx, const std::string &suff="")
 Default constructor.
 
 ~MonoUnroll ()
 Default destructor.
 
ZExpr MonoSubs (const InstrLvlAbsPtr top, const int &length, const int &pos=0)
 Unroll the ILA with internal states substituted. More...
 
ZExpr MonoAssn (const InstrLvlAbsPtr top, const int &length, const int &pos=0)
 Unroll the ILA while asserting states are equal between each step. More...
 
ZExpr MonoNone (const InstrLvlAbsPtr top, const int &length, const int &pos=0)
 Unroll the ILA without asserting states relations between steps. More...
 
ZExpr MonoIncr (const InstrLvlAbsPtr top, const int &length, const int &pos)
 Incrementally unrolling the ILA using MonoAssn (with transition relation being cached). 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

- 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.
 
- 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 the ILA as a monolithic transition system.

Member Function Documentation

◆ DefineDepVar()

void ilang::MonoUnroll::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.

◆ MonoAssn()

ZExpr ilang::MonoUnroll::MonoAssn ( const InstrLvlAbsPtr  top,
const int &  length,
const int &  pos = 0 
)

Unroll the ILA while asserting states are equal between each step.

Parameters
[in]topthe top-level ILA.
[in]lengthnumber of steps to unroll.
[in]posthe starting time frame.

◆ MonoIncr()

ZExpr ilang::MonoUnroll::MonoIncr ( const InstrLvlAbsPtr  top,
const int &  length,
const int &  pos 
)

Incrementally unrolling the ILA using MonoAssn (with transition relation being cached).

Parameters
[in]topthe top-level ILA.
[in]lengthnumber of steps to unroll.
[in]posthe starting time frame.

◆ MonoNone()

ZExpr ilang::MonoUnroll::MonoNone ( const InstrLvlAbsPtr  top,
const int &  length,
const int &  pos = 0 
)

Unroll the ILA without asserting states relations between steps.

Parameters
[in]topthe top-level ILA.
[in]lengthnumber of steps to unroll.
[in]posthe starting time frame.

◆ MonoSubs()

ZExpr ilang::MonoUnroll::MonoSubs ( const InstrLvlAbsPtr  top,
const int &  length,
const int &  pos = 0 
)

Unroll the ILA with internal states substituted.

Parameters
[in]topthe top-level ILA.
[in]lengthnumber of steps to unroll.
[in]posthe starting time frame.

◆ Transition()

void ilang::MonoUnroll::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: