Automatic Checking of Instruction Specifications

Abstract

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.