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

The wrapper of generating z3::expr for verification. More...

#include <ilang++.h>

Public Member Functions

 IlaZ3Unroller (z3::context &ctx, const std::string &suff="")
 Default constructor.
 
 ~IlaZ3Unroller ()
 Default virtual destructor.
 
void AddGlobPred (const ExprRef &p)
 Add a predicate that should be asserted globally when unrolled.
 
void AddInitPred (const ExprRef &p)
 Add a predicate that should be asserted in the initial condition.
 
void AddStepPred (const int &k, const ExprRef &p)
 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.
 
z3::expr UnrollMonoConn (const Ila &top, const int &k, const int &init=0)
 Unroll the ILA monolithically with each step connected. More...
 
z3::expr UnrollMonoFree (const Ila &top, const int &k, const int &init=0)
 Unroll the ILA monolithically with each step freely defined. More...
 
z3::expr UnrollPathConn (const std::vector< InstrRef > &path, const int &init=0)
 Unroll a path with each step connected. More...
 
z3::expr UnrollPathFree (const std::vector< InstrRef > &path, const int &init=0)
 Unroll a path with each step freely defined. More...
 
z3::expr CurrState (const ExprRef &v, const int &t)
 Return the z3::expr representing the current state at the time.
 
z3::expr NextState (const ExprRef &v, const int &t)
 Return the z3::expr representing the next state at the time.
 
z3::expr GetZ3Expr (const ExprRef &v, const int &t=0)
 Return the z3::expr representing the current-based Expr at the time.
 
z3::expr Equal (const ExprRef &va, const int &ta, const ExprRef &vb, const int &tb)
 Return the z3::expr representing a and b are equal at their time.
 

Detailed Description

The wrapper of generating z3::expr for verification.

Member Function Documentation

◆ UnrollMonoConn()

z3::expr ilang::IlaZ3Unroller::UnrollMonoConn ( const Ila top,
const int &  k,
const int &  init = 0 
)

Unroll the ILA monolithically with each step connected.

Parameters
[in]topthe top-level ILA of the hierarchy.
[in]kthe number of steps to unroll.
[in]initthe starting time frame.

◆ UnrollMonoFree()

z3::expr ilang::IlaZ3Unroller::UnrollMonoFree ( const Ila top,
const int &  k,
const int &  init = 0 
)

Unroll the ILA monolithically with each step freely defined.

Parameters
[in]topthe top-level ILA of the hierarchy.
[in]kthe number of steps to unroll.
[in]initthe starting time frame.

◆ UnrollPathConn()

z3::expr ilang::IlaZ3Unroller::UnrollPathConn ( const std::vector< InstrRef > &  path,
const int &  init = 0 
)

Unroll a path with each step connected.

Parameters
[in]paththe sequence of instructions.
[in]initthe starting time frame.

◆ UnrollPathFree()

z3::expr ilang::IlaZ3Unroller::UnrollPathFree ( const std::vector< InstrRef > &  path,
const int &  init = 0 
)

Unroll a path with each step freely defined.

Parameters
[in]paththe sequence of instructions.
[in]initthe starting time frame.

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