ilang
0.9.1
ILAng: A Modeling and Verification Platform for SoCs

Generator for commutating diagrambased equivalence checking. More...
#include <eq_check_crr.h>
Public Types  
typedef MonoUnroll  Unroll 
Public Member Functions  
CommDiag (z3::context &ctx, const CrrPtr crr)  
Default constructor.  
~CommDiag ()  
Default destructor.  
bool  EqCheck (const int &max=10) 
Check equivalence between two models based on the refinement relation up to the given unrolling bound. More...  
bool  IncEqCheck (const int &min=0, const int &max=10, const int &step=1) 
Incrementally checking equivalence between two models based on the refinement relation up to the given unrolling bound. More...  
bool  IncCheck (const int &min=0, const int &max=10, const int &step=1) 
Generator for commutating diagrambased equivalence checking.
bool ilang::CommDiag::EqCheck  (  const int &  max = 10  ) 
Check equivalence between two models based on the refinement relation up to the given unrolling bound.
[in]  max  unrolling bound. 
bool ilang::CommDiag::IncEqCheck  (  const int &  min = 0 , 
const int &  max = 10 , 

const int &  step = 1 

) 
Incrementally checking equivalence between two models based on the refinement relation up to the given unrolling bound.
[in]  min  #step of unrolling. 
[in]  max  #step of unrolling. 