v_eq_check_refinement.h File Reference

#include <z3++.h>
#include <ilang/ila-mngr/u_unroller.h>
#include <ilang/ila/instr_lvl_abs.h>

Go to the source code of this file.

Classes
class	ilang::RefinementMap
	Refinement mapping defines how to map micro-architectural states to architectural states for comparison. More...
class	ilang::RelationMap
	Relation mapping defines how arch states of two models are mapped, i.e., state mapping. More...
class	ilang::CompRefRel
	Compositional refinement relation defines a unit (element for the composition) of refinement relation, which specifies. More...
class	ilang::CommDiag
	Generator for commutating diagram-based equivalence checking. More...

Namespaces
	ilang

Typedefs
typedef RefinementMap::RefPtr	ilang::RefPtr
	Pointer type for passing around the refinement mapping.
typedef RelationMap::RelPtr	ilang::RelPtr
	Pointer type for passing around the relation mapping.
typedef CompRefRel::CrrPtr	ilang::CrrPtr
	Pointer type for passing around the compositional relation mapping.

Detailed Description

Refinement-based ILA equivalence checking using the commutative diagram approach.