Centaur Technology Media Unit Verification
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.
KeywordsClock Cycle Theorem Prove Case Split Hardware Model Symbolic Simulation
- 1.Kaufmann, M., Moore, J.S., Boyer, R.S.: ACL2 version 3.4 (2009), http://www.cs.utexas.edu/~moore/acl2/
- 2.Davis, J.: VL Verilog translator (unpublished)Google Scholar
- 3.Krug, R.: Correctness proof of ACL2 floating-point addition specification (unpublished)Google Scholar
- 4.Hunt Jr., W.A., Swords, S.: Use of the E language. In: Hardware design and Functional Languages (2009)Google Scholar
- 5.Aagaard, M.D., Jones, R.B., Seger, C.J.H.: Formal verification using parametric representations of boolean constraints. In: Proceedings of the 36th Design Automation Conference, pp. 402–407 (1999)Google Scholar
- 7.Jacobi, C., Weber, K., Paruthi, V., Baumgartner, J.: Automatic formal verification of fused-multiply-add FPUs. In: Proceedings of Design, Automation and Test in Europe, vol. 2, pp. 1298–1303 (2005)Google Scholar
- 10.IEEE Computer Society: IEEE Standard for Floating-Point Arithmetic. IEEE std 754TM-2008 edn. (2008)Google Scholar
- 11.University of California at Berkeley, Department of Electrical Engineering and Computer Science, Industrial Liaison Program: A compact test suite for P754 arithmetic – version 2.0Google Scholar
- 12.Boyer, R.S., Warren, A., Hunt, J.: Symbolic simulation in ACL2. In: Proceedings of the Eighth International Workshop on the ACL2 Theorem Prover and its Applications (2009)Google Scholar