This directory contains the ACL2 proof scripts for the pipelined
machine verification work described in FMCAD 2000 and in the ACL2 2000
Workshop.

Note that each subdirectory has its own README file.  

The files in this directory are:

README: This file.

Makefile: A makefile to certify all the books.

pipeline: 
  A directory containing the verification of the variants of Sawada's
  simple machine described in the above papers, including machines
  with exceptions, interrupts, and machines described in part at the
  netlist level.

trivial:
  A directory containing the proof that a trivial pipelined machine
  satisfies the Burch and Dill notion of correctness used by Sawada.