Title
Using range-equivalent circuits for facilitating bounded sequential equivalence checking
Abstract
This paper presents a method based on range-equivalent circuit technique for SAT-based bounded sequential equivalence checking. Given two sequential circuits to be verified, instead of straightforward unrolling the miter of two sequential circuits, we iteratively minimize the miter with a range-equivalent circuit technique before adding a new timeframe. This is because the previous timeframes can be considered as a pattern generator that feeds input patterns to the next timeframe. Experimental results show that the proposed method saved up to 91% of time for reaching the same bounded depth compared with previous work on IWLS2005 benchmarks.
Year
DOI
Venue
2018
10.1109/VLSI-DAT.2018.8373231
2018 International Symposium on VLSI Design, Automation and Test (VLSI-DAT)
Keywords
Field
DocType
range-equivalent circuit technique,sequential circuits,SAT-based bounded sequential equivalence checking,timeframe,pattern generator,input patterns,IWLS2005 benchmarks
Formal equivalence checking,Logic gate,Sequential logic,Computer science,Digital pattern generator,Algorithm,Electronic engineering,Miter joint,Equivalent circuit,Benchmark (computing),Bounded function
Conference
ISSN
ISBN
Citations 
2474-2724
978-1-5386-4261-0
0
PageRank 
References 
Authors
0.34
12
7
Name
Order
Citations
PageRank
Yung-Chih Chen141339.89
Wei-An Ji200.34
Chih-Chung Wang320.73
Ching-Yi Huang45810.06
Chia-Cheng Wu533.16
Chia-Chun Lin612815.00
Wang Chun-Yao725136.08