Paper Info
Title
Exploiting constraints in transformation-based verification
Abstract
The modeling of design environments using constraints has gained widespread industrial application, and most verification languages include constructs for specifying constraints. It is therefore critical for verification tools to intelligently leverage constraints to enhance the overall verification process. However, little prior research has addressed the applicability of transformation algorithms to designs with constraints. Even when addressed, prior work lacks optimality and in cases violates constraint semantics. In this paper, we introduce the theory and practice of transformation-based verification in the presence of constraints. We discuss how various existing transformations, such as redundancy removal and retiming, may be optimally applied while preserving constraint semantics, including dead-end states. We additionally introduce novel constraint elimination, introduction, and simplification techniques that preserve property checking. We have implemented all of the techniques proposed in this paper, and have found their synergistic application to be critical to the automated solution of many complex verification problems with constraints.
Year
DOI
Venue
2005
10.1007/11560548_21
CHARME
Keywords
Field
DocType
exploiting constraint,constraint semantics,prior research,verification tool,leverage constraint,overall verification process,prior work,verification language,novel constraint elimination,transformation-based verification,complex verification problem
Retiming,Functional verification,Model checking,Computer science,Circuit design,Theoretical computer science,Redundancy (engineering),Semantics,Distributed computing
Conference
Volume
ISSN
ISBN
3725
0302-9743
3-540-29105-9
Citations 
PageRank 
References 
7
0.50
20
Authors
3
Name
Order
Citations
PageRank
Hari Mony118613.30
Jason Baumgartner231323.36
Adnan Aziz31778149.76