This directory contains the supporting materials for the paper:

Verification of Pipeline Circuits
Matt Kaufmann and David Russinoff
ACL2 Workshop 2000 Proceedings, Austin, TX, October 2000.

You can also obtain:
A gzipped tar file for this directory.

To certify book main:

Contents of this directory:

README.html this file
cert.lisp for certifying books
declarations.lisp   input axioms for "*" model
inputs.lisp input contraints for sequential model
main.lisp proof of main result
packages.lisp package definitions
toy.rtl RTL source
And, the following automatically-generated files:
constants.lisp "*" model
exec.lisp "+" model
model.lisp sequential ("ACL2") model
pipe.lisp edited slightly as shown