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

TL;DR

This paper introduces a methodology that combines RTL equivalence checking with theorem proving by translating Verilog models into a simplified C-like language and then into ACL2 for formal verification.

Contribution

It presents a novel approach for verifying arithmetic RTL designs by translating a hand-coded RAC model into ACL2 for formal correctness proofs.

Findings

Efficient translation from RAC to ACL2 enables formal verification.

Combines equivalence checking with theorem proving for robust verification.

Facilitates formal analysis of RTL designs with a new translation technique.

Abstract

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.