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

Icon  Name                    Last modified      Size  Description
[DIR] Parent Directory                             -   
[   ] Makefile                20-Jul-2009 18:13  1.6K  
[   ] b-ops-aux-def.lisp      13-Oct-2008 14:04  1.6K  
[   ] b-ops-aux.lisp          13-Oct-2008 14:04   23K  
[TXT] basic-def.acl2          13-Oct-2008 14:04  274   
[   ] basic-def.lisp          13-Oct-2008 14:04   29K  
[TXT] basic-lemmas.lisp       13-Oct-2008 14:04   28K  
[   ] define-u-package.lisp   13-Oct-2008 14:04  139   
[TXT] exercise.lisp           13-Oct-2008 14:04  2.7K  
[   ] ihs.lisp                13-Oct-2008 14:04  5.1K  
[TXT] model.lisp              13-Oct-2008 14:04   13K  
[TXT] proof.lisp              13-Oct-2008 14:04   33K  
[TXT] table-def.lisp          13-Oct-2008 14:04   17K  
[   ] trivia.lisp             13-Oct-2008 14:04  2.7K  
[TXT] utils.acl2              13-Oct-2008 14:04  269   
[TXT] utils.lisp              13-Oct-2008 14:04  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.