BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Formal Verification of Centaur Technology's X86-Compatible Media U
 nit - Warren A. Hunt (University of Texas)
DTSTART:20090331T120000Z
DTEND:20090331T130000Z
UID:TALK17344@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION: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 insi
 de of ACL2.  We use E to represent circuits\, and we verify such represent
 ations using ACL2.  The semantics of E are specified by an interpreter wri
 tten in the ACL2 logic and they permit multiple signal equation types: BDD
 \, pairs of BDDs\, AIG\, pairs of AIGs\, dependency\, delay\, and primitiv
 es counts.  We are using E to formally verify parts of Centaur Technology'
 s (www.centtech.com)\nnewest\, 64-bit\, X86-compatible microprocessor.\n\n
 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\nproving.  We have three m
 odels: 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\nnumbers into rationals\, adds them\, and the
 n rounds the resulting rational according to the flags.  Our verification 
 includes verifying both X87 and SSE math flavors and all flag results.
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR