V  Modeling Algorithms in C++ and ACL2

A common approach to formal verification of floating-point hardware designs is the use of a commercial equivalence checker to compare the behavior of a design with that of a trusted model, which may be either a previously implemented RTL model or a higher-level C++ program. One deficiency of this method is that the model itself has typically not been formally verified, but is trusted rather by virtue of having survived extensive testing. Another is the complexity limitations that are common to such tools, which are often strained by state-of-the-art implementations of high-precision floating-point operations.

In order to address these concerns, we have identified a modeling language based on of a limited subset of C augmented by several standard C++ class templates, including the register class templates of Algorithmic C, an ANSI standard library intended for system and hardware design. This language has been used by architects, designers, and verification engineers at Intel and ARM in the specification, implementation, and formal verification of arithmetic algorithms and their implementations. The choice of language, the particular restrictions that we impose on it, and the features provided are driven by the following objectives:

Ideally, a C++ model is produced in collaboration between a floating-point architect and a verification engineer, in advance of any RTL design, which is then developed in parallel with the correctness proof of the model. This allows algorithmic bugs to be detected early in the design process in comparison to tradional verification methods, which usually cannot begin until stable RTL is available. Once the RTL and the proof of the model are both in place, the verification process is completed by checking euivalence.

The construction of such a model is driven by two opposing objectives. On the one hand, a higher-level model may more susceptible to mathematical analysis and typically allows a simpler correctness proof. On the other hand, successful equivalence checking of a complex design generally requires a significant amount of proof decomposition, using techniques that exploit structural similarities between the model and the design. As a rule of thumb, the model should be as abstract as possible while performing the same essential computations as the design.

Our modeling language is supported by a special-purpose parser, written in C++ and based on Flex and Bison, that performs the following functions:

The parser and ACL2 translator reside in the directory books/projects/masc/ of the ACL2 repository, in the subdirectories src and lisp, respectively. As a simple illustration, the subdirectory examples/imul contains a model imul.cpp of a toy integer multiplier, along with the Verilog module imul.vs from which it was derived, and with which equivalence has been established with Hector [HECTOR]. Also included are the pretty-printed version of the model (imul.m), the ACL2 translation (imul.lisp), and the ACL2 script for the correctness proof (proof.lisp), which is documented elsewhere [OLE14].

The applications subdirectory of the masc directory contains several models of more practical significance, each of which has been implemented in the floating-point unit of an ARM processor. These include modules that perform the floating-point operations of fused-multiply-add, division, and square root extraction. In each case, equivalence between the Verilog module and the C++ model has been proved with SLEC [slec]. Each C++ module is accompanied by the ACL2 translation and proof script. Following a description of the modeling language, we shall present detailed expositions of these proofs in subsequent chapters.

David Russinoff 2017-08-01