1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
|
The Verification Proof Script for the Three-Stage Pipelined Machine
Author: Jun Sawada (sawada@cs.utexas.edu)
1. Files in this Directory
This directory contains the ACL2 books that define and verify the
three-stage pipelined machine discussed in the book.
There are three types of files: a makefile, files with the ".lisp"
extension, and files with the ".acl2" extension. The makefile is used
for the Unix make command. The files with ".lisp" extension are ACL2
books which includes the ACL2 functions and theorems. The files with
".acl2" extension are used during the certification process.
Following is the list of files with the ".lisp" extension:
b-ops-aux-def.lisp: Auxiliary definitions to the IHS library.
b-ops-aux.lisp: Auxiliary theorems to the IHS library.
basic-def.lisp: The definitions of basic machine components.
basic-lemmas.lisp: Basic theorems about the pipelined machine.
ihs.lisp: Loads the IHS library and set the proper theory.
model.lisp: The definition of the three-stage pipelined machine.
proof.lisp: Proof of the commutative diagram.
table-def.lisp: The definition of the intermediate abstraction MAETT.
trivia.lisp: Some trivial lemmas.
utils.lisp: Definitions of utility functions.
How to re-certify the ACL2 book:
1. You may have to modify the paths to the ACL2 public libraries. At
this moment, the ACL2 does not provide a uniform method to load ACL2
public libraries whose absolute path names may vary. For example, the
IHS libraries are typically found in the "ihs" directory of the "book"
directory of the root directory for the ACL2 source code, but the ACL2
root directory is decided when it is installed. If the load path to
the public libraries are not set properly, the certification process
fails. You may have to change all the paths one-by-one.
2 Run "make".
|
