Formal Sequential Equivalence Checking of Digital Systems by Symbolic Simulation
A new approach to sequential verification of designs at different levels of abstraction by symbolic simulation is proposed. The automatic formal verification tool has been used for equivalence checking of structural descriptions at rt-level and their corresponding behavioral specifications. Gate-lev...
| Main Author: | |
|---|---|
| Format: | Others |
| Language: | English en |
| Published: |
2001
|
| Online Access: | http://tuprints.ulb.tu-darmstadt.de/113/1/thesis.pdf Ritter, Gerd <http://tuprints.ulb.tu-darmstadt.de/view/person/Ritter=3AGerd=3A=3A.html> : Formal Sequential Equivalence Checking of Digital Systems by Symbolic Simulation. [Online-Edition] Technische Universität, Darmstadt [Ph.D. Thesis], (2001) |
| Summary: | A new approach to sequential verification of designs at different levels of abstraction by symbolic simulation is proposed. The automatic formal verification tool has been used for equivalence checking of structural descriptions at rt-level and their corresponding behavioral specifications. Gate-level results of a commercial synthesis tool have been compared to specifications at behavioral or structural rt-level. The specification need not be synthesizable nor cycle equivalent to the implementation. In addition, a future application of the method to property verification is proposed. Symbolic simulation is guided along logically consistent paths in the two descriptions to be compared. An open library of different equivalence detection techniques is used in order to find a good compromise between accuracy and speed. Decision diagram (OBDD) based techniques detect corner-cases of equivalence. Graph explosion is avoided by using the results of the other equivalence detection techniques and by representing only small parts of the verification problem by decision diagrams. The cooperation of all techniques as well as good debugging support are made feasible by notifying detected relationships at equivalence classes instead of manipulating symbolic terms. |
|---|