Formal Verification

Centaur Logo

We formally model and analyze Centaur processor designs.

ACL2 Books

We are active in the ACL2 Books project.

We host a copy of the ACL2+Books Manual.

Contact Information

Name / email (@centtech.com)

Academic Publications

Jared Davis, Anna Slobodova, and Sol Swords. Microcode Verification—Another Piece of the Microprocessor Verification Puzzle. Invited talk, ITP 2014. Springer LNCS, 8558. July, 2014. Pages 1-16.
Despite significant progress in formal hardware verification in the past decade, little has been published on the verification of microcode. Microcode is the heart of every microprocessor and is one of the most complex parts of the design: it is tightly connected to the huge machine state, written in an assembly-like language that has no support for data or control structures, and has little documentation and changing semantics. At the same time it plays a crucial role in the way the processor works.
We describe the method of formal microcode verification we have developed for an x86-64 microprocessor designed at Centaur Technology. While the previous work on high and low level code verification is based on an unverified abstract machine model, our approach is tightly connected with our effort to verify the register-transfer level implementation of the hardware. The same microoperation specifications developed to verify implementation of teh execution units are used to define operational semantics for the microcode verification.
While the techniques used in the described verification effort are not inherently new, to our knowledge, our effort is the first interconnection of hardware and microcode verification in context of an industrial size design. Both our hardware and microcode verifications are done within the same verification framework.
Jared Davis and Matt Kaufmann. Industrial Strength Documentation for ACL2. In ACL2 2014. July, 2014. EPTCS 152. Pages 9-25.
The ACL2 theorem prover is a complex system. Its libraries are vast. Industrial verification efforts may extend this base with hundreds of thousands of lines of additional modeling tools, specifications, and proof scripts. High quality documentation is vital for teams that are working together on projects of this scale. We have developed XDOC, a flexible, scalable documentation tool for ACL2 that can incorporate the documentation for ACL2 itself, the Community Books, and an organization's internal formal verification projects, and which has many features that help to keep the resulting manuals up to date. Using this tool, we have produced a comprehensive, publicly available ACL2+Books Manual that brings better documentation to all ACL2 users. We have also developed an extended manual for use within Centaur Technology that extends the public manual to cover Centaur's internal books. We expect that other organizations using ACL2 will wish to develop similarly extended manuals.
Jared Davis and Sol Swords. Verified AIG Algorithms in ACL2. In ACL2 2013. May, 2013. EPTCS 114. Pages 95-110.
And-Inverter Graphs (AIGs) are a popular way to represent Boolean functions (like circuits). AIG simplification algorithms can dramatically reduce an AIG, and play an important role in modern hardware verification tools like equivalence checkers. In practice, these tricky algorithms are implemented with optimized C or C++ routines with no guarantee of correctness. Meanwhile, many interactive theorem provers can now employ SAT or SMT solvers to automatically solve finite goals, but no theorem prover makes use of these advanced, AIG-based approaches.
We have developed two ways to represent AIGs within the ACL2 theorem prover. One representation, Hons-AIGs, is especially convenient to use and reason about. The other, Aignet, is the opposite; it is styled after modern AIG packages and allows for efficient algorithms. We have implemented functions for converting between these representations, random vector simulation, conversion to CNF, etc., and developed reasoning strategies for verifying these algorithms.
Aside from these contributions towards verifying AIG algorithms, this work has an immediate, practical benefit for ACL2 users who are using GL to bit-blast finite ACL2 theorems: they can now optionally trust an off-the-shelf SAT solver to carry out the proof, instead of using the built-in BDD package. Looking to the future, it is a first step toward implementing verified AIG simplification algorithms that might further improve GL performance.
Jared Davis. Embedding ACL2 Models in End-User Applications. In Do-Form 2013, AISB 2013, Exeter, UK. April, 2013. Pages 49-56.
Formal verification, based on mechanical theorem proving, can provide unique evidence that systems are correct. Unfortunately this promise of correctness is, for most projects, not enough to justify its high cost. Since formal models and proof scripts offer few other direct benefits to system developers and managers, the idea of formal verification is abandoned.
We have developed a way to embed functions from the ACL2 theorem prover into software that is written in mainstream programming languages. This lets us reuse formal ACL2 models to develop applications with features like graphics, networking, databases, etc. For example, we have written a web-based tool for hardware designers in Ruby on top of a 100,000+ line ACL2 codebase.
This is neat: we can reuse the supporting work needed for formal verification to create tools that are useful beyond the formal verification team. The value added by these tools will help to justify the investment in formal verification, and the project as a whole will benefit from the precision of formal modeling and analysis.
Sol Swords and Jared Davis. Bit-Blasting ACL2 Theorems. In ACL2 2011. November, 2011. EPTCS 70. Pages 84-102.
Interactive theorem proving requires a lot of human guidance. Proving a property involves (1) figuring out why it holds, then (2) coaxing the theorem prover into believing it. Both steps can take a long time. We explain how to use GL, a framework for proving finite ACL2 theorems with BDD- or SAT-based reasoning. This approach makes it unnecessary to deeply understand why a property is true, and automates the process of admitting it as a theorem. We use GL at Centaur Technology to verify execution units for x86 integer, MMX, SSE, and floating-point arithmetic.
Anna Slobodova, Jared Davis, Sol Swords, and Warren A. Hunt, Jr. A Flexible Formal Verification Framework for Industrial Scale Validation. Invited talk, MemoCode 2011. July, 2011. Pages 89-97.
In recent years, leading microprocessor companies have made huge investments to improve the reliability of their products. Besides expanding their validation and CAD tools teams, they have incorporated formal verification methods into their design flows. Formal verification (FV) engineers require extensive training, and FV tools from CAD vendors are expensive. At first glance, it may seem that FV teams are not affordable by smaller companies. We have not found this to be true. This paper describes the formal verification framework we have built on top of publicly-available tools. This framework gives us the flexibility to work on myriad different problems that occur in microprocessor design.
Warren A. Hunt Jr., Sol Swords, Jared Davis, and Anna Slobodova. Use of Formal Verification at Centaur Technology. In David S. Hardin, editor, Design and Verification of Microprocessor Systems for High Assurance Applications. 2010. Springer. Pages 65-88.
We describe the formal methodology we are using to verify components of a commercial 64-bit, x86-compatible microprocessor design at Centaur Technology. This methodology is based on the ACL2 theorem prover. In this methodology, we mechanically translate the RTL design into a formal HDL for which we have an interpreter in ACL2. We use AIG- and BDD-based symbolic simulation and theorem proving techniques to show that the hardware models satisfy their specifications, which are ACL2 functions. Completed verifications yield theorems admitted by ACL2, ensuring that the verification is based on sound reasoning. We have used this methodology to verify instructions such as SIMD floating-point addition and subtraction, integer and floating-point multiplication, comparisons, bit-wise logical operations, and integer/float conversions. We discuss our floating-point addition verification as a case study.
Warren A. Hunt, Jr. Verifying VIA Nano microprocessor components. In FMCAD 2010. October, 2010. Pages 3-10.
We verify parts of the VIA Nano X86-compatible microprocessor design using the ACL2 theorem-proving system. We translate Nano RTL Verilog into the EMOD hardware description language. We specify properties of the Nano in the ACL2 logic and use a combination of theorem-proving and automated techniques to verify the correctness of Nano design elements.
Sol Swords and Warren A. Hunt, Jr. A Mechanically Verified AIG-to-BDD Conversion Algorithm. In ITP 2010. Springer LNCS 6172. July, 2010. Pages 435-449.
We present the mechanical verification of an algorithm for building a BDD from an AND/INVERTER graph (AIG). The algorithm uses two methods to simplify an input AIG using BDDs of limited size; it repeatedly applies these methods while varying the BDD size limit. One method is similar to dynamic weakening in that it replaces oversized BDDs by a conservative approximation; the other method introduces fresh variables to represent oversized BDDs. This algorithm is written in the executable logic of the ACL2 theorem prover. The primary contribution is the verification of our conversion algorithm. We state its correctness theorem and outline the major steps needed to prove it.
Warren A. Hunt, Jr. and Sol Swords. Centaur Technology Media Unit Verification. In CAV 2009. Springer LNCS 5643. June 2009. Pages 353-367.
We have verified floating-point addition/subtraction instructions for the media unit from Centaur's 64-bit, X86-compatible microprocessor. This unit implements over one hundred instructions, with the most complex being floating-point addition/subtraction. This media unit can add/subtract four pairs of floating-point numbers every clock cycle with an industry-leading two-cycle latency.
Using the ACL2 theorem proving system, we model the media unit by translating its Verilog design into an HDL that we have deeply embedded in the ACL2 logic. We specify the addition/subtraction instructions as integer-based ACL2 functions. Using a combination of AIG- and BDD-based symbolic simulation, case splitting, and theorem proving, we produce a mechanically checked theorem in ACL2 for each instruction examined stating that the hardware model yields the same result as the instruction specification.
In pursuit of these verifications, we implemented a formal HDL and symbolic simulation framework, including formally verified BDD and AIG operators, within the ACL2 theorem proving system. The HDL includes an extensible interpreter capable of performing concrete and symbolic simulations as well as non-functional analyses. We know of no other symbolic simulation-based floating-point verification that is performed within a single formal system and produces a theorem in that system without relying on unverified external tools.