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

Base class for unrolling ILA execution in different settings. More...

#include <unroller.h>

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

Public Types

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

 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

virtual void DefineDepVar ()=0
 [Application-specific] Define dependant state variables. More...
 
virtual void Transition (const int &idx)=0
 [Application-specific] Define next state update functions. More...
 
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.
 

Static Protected Member Functions

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

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

Base class for unrolling ILA execution in different settings.

Member Function Documentation

◆ DefineDepVar()

virtual void ilang::Unroller::DefineDepVar ( )
protectedpure virtual

[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.

Implemented in ilang::MonoUnroll, and ilang::PathUnroll.

◆ Transition()

virtual void ilang::Unroller::Transition ( const int &  idx)
protectedpure virtual

[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).

Implemented in ilang::MonoUnroll, and ilang::PathUnroll.


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