  We present a methodology for formal verification of arithmetic RTL designs
that combines sequential logic equivalence checking with interactive theorem
proving. An intermediate model of a Verilog module is hand-coded in Restricted
Algorithmic C (RAC), a primitive subset of C augmented by the integer and
fixed-point register class templates of Algorithmic C. The model is designed to
be as abstract and compact as possible, but sufficiently faithful to the RTL to
allow efficient equivalence checking with a commercial tool. It is then
automatically translated to the logic of ACL2, enabling a mechanically checked
proof of correctness with respect to a formal architectural specification. In
this paper, we describe the RAC language, the translation process, and some
techniques that facilitate formal analysis of the resulting ACL2 code.
