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 Chen | 1 | 413 | 39.89 |
Wei-An Ji | 2 | 0 | 0.34 |
Chih-Chung Wang | 3 | 2 | 0.73 |
Ching-Yi Huang | 4 | 58 | 10.06 |
Chia-Cheng Wu | 5 | 3 | 3.16 |
Chia-Chun Lin | 6 | 128 | 15.00 |
Wang Chun-Yao | 7 | 251 | 36.08 |