A system for generating processor hardware supports a language for
significant extensions to the processor instruction set, where the
designer specifies only the semantics of the new instructions and the
system generates other logic. The extension language provides for the
addition of processor state, including register files, and instructions
that operate on that state. The language also provides for new data types
to be added to the compiler to represent the state added. It allows
separate specification of reference semantics and instruction
implementation, and uses this to automate design verification. In
addition, the system generates formatted instruction set documentation
from the language specification.