Automatic Verification of Arithmetic Circuits in RTL using Term Rewriting Systems

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 transla-tion 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 cir-cuit 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 ver-ification of several multiplier designs which have hitherto been impossible to verify with existing approaches and tools