Automatic Verification of Arithmetic Circuits in RTL Using Stepwise Refinement of Term Rewriting Systems
Issue No. 10 - October (2007 vol. 56)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TC.2007.1073
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.
circuit CAD, digital arithmetic, formal specification, formal verification, hardware description languages, logic design, rewriting systems,automatic arithmetic circuit design verification, register transfer level, stepwise refinement, term rewriting systems, automatic circuit translation, Verilog RTL description, multiplier design verification, Verifire tool,Adders, Circuit synthesis, Algorithm design and analysis, Registers, Optimized production technology, Engines, Logic gates,Verification, Hardware Description Languages, Register Transfer Level implementation, arithmetic logic unit.
"Automatic Verification of Arithmetic Circuits in RTL Using Stepwise Refinement of Term Rewriting Systems", IEEE Transactions on Computers, vol. 56, no. , pp. 1401-1414, October 2007, doi:10.1109/TC.2007.1073