Towards a Formal Model of the X86 ISA

Abstract

We present a preliminary formalization of a subset of the x86 instruction set. Our model is written in the logic of the ACL2 theorem prover. It can be executed as a Lisp program on concrete data, which provides the capability to validate the model against results delivered by actual x86 processors. We demonstrate how bugs in our model can also be eliminated by using the ACL2 prover to verify guards (semantic preconditions) for our functions.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Mar 30, 2012
Accession Number
AD1024616

Entities

People

  • Matt Kaufmann
  • Warren A. Jr Hunt

Organizations

  • University of Texas at Austin

Tags

Communities of Interest

  • Advanced Electronics

DTIC Thesaurus Topics

  • Addressing
  • Arithmetic
  • Cecum
  • Computer Languages
  • Computer Programming
  • Computer Science
  • Computing System Architectures
  • Construction
  • Decoders
  • Decoding
  • Directories
  • Displacement
  • Instruction Set Architecture
  • Instructions
  • Language
  • Lisp Programming Language
  • Microarchitecture
  • Programming Languages
  • Shell Scripts
  • Step Functions
  • Supervisors
  • Symbols
  • Verification

Fields of Study

  • Computer science

Readers

  • Database Systems and Applications
  • Mathematical Modeling and Probability Theory.
  • Parallel and Distributed Computing.