Formal Verification of Arithmetic RTL: Translating Verilog to C++ to ACL2

David M. Russinoff

We present a methodology for formal verification of arithmetic RTL designs that combines sequential logic equivalence checking with interactive theorem proving. An intermediate mod…