Name
Abstract | ||
|---|---|---|
The paper describes an efficient method to prove equivalence between two integer arithmetic datapath designs specified at the register transfer level. The method is illustrated with an industrial ALU design. As reported in literature, solving it using a commercial equivalence checking tool required case-splitting, which limits its applicability to larger designs. We show how such a task can be solved as a simpler verification problem without case-splitting. We demonstrate both the wordlevel and bit-level approach to this problem and show that the method is scalable to large combinational datapath circuits. Experimental results demonstrate the application of the method to large combinational arithmetic circuits. |
Year | DOI | Venue |
|---|---|---|
2015 | 10.1109/ISCAS.2015.7169020 | International Symposium on Circuits and Systems |
Keywords | Field | DocType |
functional verification, arithmetic circuits, RTL transformations | Formal equivalence checking,Datapath,Boolean circuit,Computer science,Finite state machine with datapath,Arithmetic logic unit,Arithmetic,Combinational logic,Equivalence (measure theory),Register-transfer level | Conference |
ISSN | Citations | PageRank |
0271-4302 | 1 | 0.38 |
References | Authors | |
9 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Cunxi Yu | 1 | 98 | 9.64 |
| Walter Brown | 2 | 47 | 3.10 |
| Maciej J. Ciesielski | 3 | 629 | 74.80 |