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

Simplified bounded model checking engine for ILAs. More...

#include <legacy_bmc.h>

Public Member Functions

 LegacyBmc ()
 Default constructor.
 
 ~LegacyBmc ()
 Default destructor.
 
void AddInit (ExprPtr init)
 Add initial condition to the solver.
 
void AddInvariant (ExprPtr inv)
 Add invariant to the solver.
 
void AddProperty (ExprPtr prop)
 Add property of one ILA.
 
z3::check_result Check (InstrLvlAbsPtr m0, const int &k0, InstrLvlAbsPtr m1, const int &k1)
 Legacy BMC where two ILAs are unrolled and compared monolithically.
 

Detailed Description

Simplified bounded model checking engine for ILAs.


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