Index of /users/moore/acl2/v3-0/distrib/acl2-sources/books/workshops/1999/pipeline

Icon  Name                    Last modified      Size  Description
[DIR] Parent Directory                             -   
[   ] Makefile                18-May-2006 14:59  1.6K  
[   ] b-ops-aux-def.lisp      20-Dec-1999 16:23  1.6K  
[   ] b-ops-aux.lisp          20-Dec-1999 16:23   23K  
[TXT] basic-def.acl2          05-May-2000 16:55  274   
[   ] basic-def.lisp          17-Jul-2005 13:20   28K  
[TXT] basic-lemmas.lisp       21-Dec-1999 14:04   28K  
[   ] define-u-package.lisp   20-Dec-1999 16:23  139   
[TXT] exercise.lisp           10-Apr-2000 12:48  2.7K  
[   ] ihs.lisp                10-Apr-2001 22:55  5.1K  
[TXT] model.lisp              23-Feb-2000 14:15   13K  
[TXT] proof.lisp              23-Feb-2001 16:11   33K  
[TXT] table-def.lisp          21-Dec-1999 14:27   17K  
[   ] trivia.lisp             10-Apr-2001 22:55  2.7K  
[TXT] utils.acl2              05-May-2000 16:55  269   
[TXT] utils.lisp              10-Apr-2001 22:55  4.2K  

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.