Automatic Checking of Instruction Specifications

Norman Ramsey and Mary Fernández.


Retargeting applications that process machine code is a tedious and error-prone task. We help automate retargeting by describing instruction sets in a high-level specification language and by generating automatically the code for encoding and decoding instructions. Moreover, we provide automated assistance for checking machine descriptions.

We check a specification for consistency both internally and externally. Internal checking forbids impossible instruction specifications, e.g., those that specify two values for a single bit. Internal checking warns about implausible specifications, e.g., those that don't specify values for all bits. Internal checks catch many mistakes, but they cannot guarantee that a specification accurately describes a target machine. Externally, we check a specification for consistency with an independent assembler. This technique increases a user's confidence in a specification's correctness and permits debugging in isolation of the target application. External validation is effective: it identified errors in specifications of the Intel Pentium, the MIPS, and the SPARC, after code generated from the latter two had been used in applications for over a year.

Full paper

A PostScript version of the paper (228K) is available. There is also an HTML version (75K), but the HTML was generated automatically from LaTeX source, and the result isn't always readable, especially the figures. .