Skip to Main content Skip to Navigation
Conference papers

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.
Complete list of metadata
Contributor : Christine Carvalho De Matos Connect in order to contact the contributor
Submitted on : Wednesday, September 7, 2022 - 6:23:41 PM
Last modification on : Wednesday, September 7, 2022 - 6:24:20 PM


Files produced by the author(s)




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⟩



Record views


Files downloads