Centaur Technology Media Unit Verification

Add to your list(s) Download to your calendar using vCal

• Professor Warren A. Hunt, Jr., University of Texas and Centaur Technology, Inc.
• Friday 24 July 2009, 14:00-16:00
• Huxley room 217.

If you have a question about this talk, please contact w.luk.

We have verified a number of instructions for the media unit from Centaur’s Nano 64-bit, X86 -compatible microprocessor. This unit implements over one hundred logical, arithmetic, and conversion instructions, with the most complex instructions 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. 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. This is joint work with Sol Swords.

Biography: Dr. Hunt is a Professor at the University of Texas and a Senior Principal Engineer for Centaur Technology, Inc. He has been involved with the use of formal methods for hardware verification for the last 27 years, and he has been involved with the formal verification of a number of microprocessors: FM8501 , FM8502 , FM9001, FM9801 , Motorola’s CAP DSP , and Centaur’s Nano. Hunt is also one of the contributing authors of the ACL2 system.

Map: http://www3.imperial.ac.uk/computing/about/mapandtravel

This talk is part of the Featured talks series.

This talk is included in these lists:

• Andrea Picciau's list
• COMMSP & CP list
• COMMSP Seminar
• Featured talks
• Huxley room 217
• SAP Talks

Note that ex-directory lists are not shown.