The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.10 - October (2007 vol.56)
pp: 1401-1414
ABSTRACT
This paper presents a novel technique for proving the correctness of arithmetic circuit designs described at the Register Transfer Level (RTL). The technique begins with the automatic translation of circuits from a Verilog RTL description into a Term Rewriting System (TRS). We prove the correctness of the designs via an equivalence proof between TRSs for the implementation circuit design and a much simpler specification circuit design. We present this notion of equivalence between the TRSs and a stepwise refinement method for its decomposition, which we leverage in our tool Verifire. We demonstrate the effectiveness of our technique by using the tool for the verification of several multiplier designs that have hitherto been impossible to verify with existing approaches and tools.
INDEX TERMS
Verification, Hardware Description Languages, Register Transfer Level implementation, arithmetic logic unit.
CITATION
Vinod Viswanath, Shobha Vasudevan, Jacob A. Abraham, "Automatic Verification of Arithmetic Circuits in RTL Using Stepwise Refinement of Term Rewriting Systems", IEEE Transactions on Computers, vol.56, no. 10, pp. 1401-1414, October 2007, doi:10.1109/TC.2007.1073
20 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool