Verification Scripts for FM9801 Pipelined Microprocessor Design
Highlights Download Verification Scripts
Graphical Viewer List
of Script Files ACL2
This page provides information about the ACL2 scripts for FM9801 verification
We have created a new microprocessor model named FM9801
for studying the verification of modern microprocessors. The model
contains several features found in modern commercial microprocessors, such
as speculative execution with branch predication, out-of-order execution
with reservation stations and re-order buffers, pipelined execution units,
memory write-buffers and load bypassing, and precise exception handling
of internal and external interrupts.
We verified this processor model using the ACL2 theorem prover.
You can rerun the proof with the proof script.
To browse the ACL2 scripts, please see this page.
A Short Overview of the Verification Approach
Our verification approach can be categorized into two steps:
-
Define and verify invariant conditions of our pipelined machine.
-
Verify the correctness criterion using the invariant conditions.
Our correctness criterion checks whether the pipelined machine executes
individual nstructions as exactly specified by the non-pipelined machine.
Our target machine design is too large to directly check this criterion.
Our approach decomposes the problem by defining various pipeline invariant
conditions and incrementally verifying them. Our Micro-Architectural
Execution Trace Table (MAETT) is useful to define these pipeline properties.
The sufficiently strong set of invariant conditions is not easy to define.
Our Invariant Strengthening Procedure helped us to define such a set of
invariant conditions. For more detailed information, please
refer to our reports [1
, 2 , 3].
How to mechanically re-prove the correctness of the FM9801 processor design
You can re-verify our microprocessor model using our ACL2
scripts. This requires ACL2
version 2.3 or later. Following are instructions to certify
our ACL2 scripts:
-
First make sure that you have installed the ACL2
theorem prover 2.3 or later. The ACL2 public libraries coming
with the distribution should have been certified. Usually, the public
library is installed at the sub directory named books under the
ACL2 home directory.
-
Download the Unix tar file of our ACL2 scripts from here,
and save it as MA2-proof.tar.gz in your working directory.
-
Decompress and extract files from the tar file by typing:
% gunzip MA2-proof.tar.gz
% tar xf MA2-proof.tar
-
Change directory to the sub directory MA2-proof.
-
Modify makefile to set variables. For instance, if you want to
set the variable ACL2 to /usr/local/bin/acl2, delete
the already existing line beginning with ACL2 and add a line:
ACL2=/usr/local/bin/acl2
I think modifying the following three variables is all you need to
do.
-
ACL2: should be set to the path to your ACL2 executable.
-
ACL2_BOOK_DIR: should be set to the directory containing
the ACL2 public library. If the ACL2 source code is extracted at
the directory
<ACL2_HOME_DIR>, public library is usually at
<ACL2_HOME_DIR>/books.
-
EXT: The extension for the compiled object. If the ACL2
executable is based on Allegro Common Lisp, this should be set to "fasl".
If it is based on GCL, it should be set to "o".
-
Type:
% make prepare
% make
The last "make" command certifies all the ACL2 books, that means,
proves all the theorems presented in the .lisp files. Confirm that non
of the fACL2 books contain "cheating commands" like defaxiom or
skip-proofs.
And
confirm that exintr.cert is created that implies all lemmas including the
two correctness theorems exintr-correctness-criteria
and correctness-criteria
in exintr.lisp are proved.
The list of files archived in the MA2-proof.tar.gz is given here.
For any questions about this software, please ask Jun Sawada at sawada@us.ibm.com.
Reading the proof script and understanding the proof structure
If you want to browse the ACL2 proof scripts for the FM9801 verification,
please follow the link here. The basic structure of the ACL2 books is as
shown below:
