← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/workshops/2000/manolios/pipeline/README

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/workshops/2000/manolios/pipeline/README
 
1
This directory contains the ACL2 proof scripts for the pipelined
 
2
machine verification work described in FMCAD 2000 and in the ACL2 2000
 
3
Workshop.
 
4
 
 
5
Note that each subdirectory has its own README file.  
 
6
 
 
7
The files in this directory are:
 
8
 
 
9
README: This file.
 
10
 
 
11
Makefile: A makefile to certify all the books.
 
12
 
 
13
pipeline: 
 
14
  A directory containing the verification of the variants of Sawada's
 
15
  simple machine described in the above papers, including machines
 
16
  with exceptions, interrupts, and machines described in part at the
 
17
  netlist level.
 
18
 
 
19
trivial:
 
20
  A directory containing the proof that a trivial pipelined machine
 
21
  satisfies the Burch and Dill notion of correctness used by Sawada.