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

Generator for commutating diagram-based 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)
 

Detailed Description

Generator for commutating diagram-based equivalence checking.

Member Function Documentation

◆ EqCheck()

bool ilang::CommDiag::EqCheck ( const int &  max = 10)

Check equivalence between two models based on the refinement relation up to the given unrolling bound.

Parameters
[in]maxunrolling bound.

◆ IncEqCheck()

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.

Parameters
[in]min#step of unrolling.
[in]max#step of unrolling.

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