Verification of Pipeline Circuits

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:

Edit the fourth form in cert.lisp, as indicated.
Execute the following in the shell:
```
cat cert.lisp | acl2
```

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

`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