Matching in the presence of don't cares and redundant sequential elements for sequential equivalence checking - LIRMM - Laboratoire d’Informatique, de Robotique et de Microélectronique de Montpellier
Conference Papers Year : 2003

Matching in the presence of don't cares and redundant sequential elements for sequential equivalence checking

Abstract

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.
Fichier principal
Vignette du fichier
D162.PDF.pdf (97.96 Ko) Télécharger le fichier

Dates and versions

lirmm-00269707 , version 1 (07-09-2022)

Identifiers

Cite

Solaiman Rahim, Bruno Rouzeyre, Lionel Torres, Jerome Rampon. Matching in the presence of don't cares and redundant sequential elements for sequential equivalence checking. HLDVT 2003 - 8th IEEE International High-Level Design Validation and Test Workshop, Nov 2003, San Francisco, United States. pp.129-135, ⟨10.1109/HLDVT.2003.1252486⟩. ⟨lirmm-00269707⟩
348 View
359 Download

Altmetric

Share

More