Matching in the Presence of don't Cares and Redundant Sequential Elements for Sequential Equivalence Checking
| Autor: | B. Rouzeyre, J. Rampon, Solaiman Rahim, L. Torres |
|---|---|
| Přispěvatelé: | Laboratoire d'Informatique de Robotique et de Microélectronique de Montpellier (LIRMM), Centre National de la Recherche Scientifique (CNRS)-Université de Montpellier (UM), Conception et Test de Systèmes MICroélectroniques (SysMIC), Centre National de la Recherche Scientifique (CNRS)-Université de Montpellier (UM)-Centre National de la Recherche Scientifique (CNRS)-Université de Montpellier (UM), Carvalho De Matos, Christine |
| Jazyk: | angličtina |
| Rok vydání: | 2008 |
| Předmět: |
[SPI.OTHER]Engineering Sciences [physics]/Other
Matching (statistics) Theoretical computer science Sequential logic Computer science [SPI.OTHER] Engineering Sciences [physics]/Other Formal equivalence checking 02 engineering and technology 020202 computer hardware & architecture High-level synthesis 0202 electrical engineering electronic engineering information engineering Redundancy (engineering) State space 020201 artificial intelligence & image processing Formal verification Equivalence (measure theory) Algorithm ComputingMilieux_MISCELLANEOUS Hardware_LOGICDESIGN |
| Zdroj: | HLDVT'03: High Level Design Validation and Test Workshop HLDVT'03: High Level Design Validation and Test Workshop, San Francisco (USA), France. pp. 129-135 HLDVT HLDVT'03: High Level Design Validation and Test Workshop, San Francisco, United States. pp.129-135 |
| Popis: | Full sequential equivalence checking by state space traversal has been shown to be unpractical for large designs. To address state space explosion new approaches have been proposed that exploit structural characteristics of a design and make use of multiple analysis engines (e.g. BDDs, Simulation, SAT) to transform the sequential equivalence checking problem into a combinational equivalence checking problem. While these approaches, based on induction techniques, have been successful in general, they are not able to reach proof of equivalence in presence of complex transformations between the reference design and its implementation. One of these transformations is redundant Flip-Flops (FFs) removal. FFs may be removed by redundancy removal, or don't care optimization techniques applied by synthesis tools. Consequently, some FFs in the reference design may have no equivalent FFs in the implementation net-list. Latest researches in this area have proposed specific solutions for particular cases. Matching in the presence of redundant constant input FFs has been addressed and identification of sequential redundancy is performed. This paper presents an indepth study of some possible causes of unmatched FFs due to redundancy removal, and proposes a generic approach to achieve prove of equivalence in presence of redundant FFs. Our approach is independent from specific synthesis transformations. It is able to achieve matching in presence of complex redundancies, and is able to perform formal equivalence checking in presence of don't cares. The experimental results show a significant improvement in the matching rates of FFs when compared to industrial equivalence checking tools. This higher matching is directly translated to a higher success rate in proving equivalency. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|