Abstract

We are verifying commercial circuits by translating them from Verilog to our formal E language, and then performing symbolic analysis. E is a hierarchical, occurrence-oriented HDL that is deeply embedded inside of ACL2 . We use E to represent circuits, and we verify such representations using ACL2 . The semantics of E are specified by an interpreter written in the ACL2 logic and they permit multiple signal equation types: BDD , pairs of BDDs, AIG , pairs of AIGs, dependency, delay, and primitives counts. We are using E to formally verify parts of Centaur Technology’s (www.centtech.com) newest, 64-bit, X86 -compatible microprocessor.

We have verified Centaur’s floating-point adder design, capable of adding four 32-bit pairs, two 64-bit pairs, or one 80-bit pair of numbers with a two-cycle (industry-best?) latency. This verification is performed by a combination of symbolic simulation and theorem proving. We have three models: an E-language model of the RTL mechanically produced from Verilog, an intermediate integer-level model, and a top-level mathematical model that converts floating-point numbers into rationals, adds them, and then rounds the resulting rational according to the flags. Our verification includes verifying both X87 and SSE math flavors and all flag results.