Abstract

We describe our work concerning X86 ISA specification and its use in verifying the correctness of the VIA Nano design and for verifying X86 binary programs. Our talk will be three part: a brief description of our tools and methods, our modeling and verification of the VIA Nano, and our verification of X86 binary code. The VIA Nano is a X86 -compatible, 64-bit microprocessor; this processor appears in HP and Lenovo products and in many X86 -based, embedded computers.

We will describe our use of the ACL2 logic to model the X86 ISA and verify binary programs. We give a simple example of verifying a word-count program. We also describe our modeling of the VIA Nano design, and describe our efforts at verifying Nano microcode. Microcode is the heart of modern microprocessors, and it implements some of the most complex processor-internal control functions: it is tightly connected to the machine state, written in an assembly-like language that has no support for data or control structures, and it has ever-changing semantics.

Bio: see http://www.cs.utexas.edu/users/hunt/index.html.