This page provides the information and the link to our processor model. Our model is specified in the ACL2 logic. The processor is a multi-issue, out-of-order execution, pipelined machine which can speculatively execute more than ten instructions. It also implements precise handling of internal and external exceptions. This machine design is our target of pipeline verification research, and this processor model is not designed as a real micro-processor. Rather, it is a "toy example" to enable us to investigate verification of pipelined machines with complex features. Even though the implemented instruction set is small, it implements more realistic features of current microprocessors, such as a re-order buffer, reservation stations, branch prediction mechanism, and so on. A simple block diagram is given here.
Our processor has been specified at two levels: at the micro-architectural(MA) level and instruction set architecture (ISA) level. At either level, the machine behavior is specified as an ACL2 behavioral function, which takes a current machine state and external inputs (oracles), and returns the next state. Different time abstraction is used at the two levels. The MA behavioral function returns the MA state one machine clock cycle after the current state; however, the ISA behavioral function returns the ISA machine state after executing a single instruction. The MA is a pipelined machine design, while the ISA is a non-pipelined machine. It is also important to point out that an ISA state contains only programmer visible components, while the MA state contains the states of implementation registers.
The ISA and MA machine designs are specified in ISA-def.lisp and MA2-def.lisp. The whole ACL2 books are also available in gzipped, Unix tar format:
This tar file also contains various lemmas about the machine design, and the upper level proof of the correctness of our pipelined machine. (However, this processor specification in this script is only subjected to the simulation but not the formal verification, and we have found a number of bugs in the specification. If you are interested in getting a bug free version of the machine specification, get MA2-proof.tar.gz, which contains a completely verified version of the machine. ) In order to run this machine specification, you need: The simple direction to compile the machine specification and rerun the ACL2 proof script is given in README. For the information about the proof, please see Sawada's dissertation.For any questions about this software, please
send email to