blob: 1c8ed68060599ef6710d334a0639388095a401a0 (
plain)
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
|
The Verification Proof Script for the Three-Stage Pipelined Machine
Author: Jun Sawada (sawada@cs.utexas.edu)
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.
define-u-package.lisp: Book used to define package "u".
exercise.lisp: Solutions to book exercise.
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.
You can re-certify the ACL2 books using make.
For further questions, please send e-mail to sawada@cs.utexas.edu.
|
