1 files changed, 93 insertions, 0 deletions
diff --git a/books/workshops/2000/russinoff-kaufmann/supporting-materials/index.html b/books/workshops/2000/russinoff-kaufmann/supporting-materials/index.html
new file mode 100644
index 0000000..c738554
--- /dev/null
+++ b/books/workshops/2000/russinoff-kaufmann/supporting-materials/index.html
@@ -0,0 +1,93 @@
+<HTML>
+<HEAD><TITLE>Verification of Pipeline Circuits</TITLE></HEAD>
+<BODY BGCOLOR="#FFFFFF">
+ 
+This directory contains the supporting materials for the paper:<br><br>
+
+Verification of Pipeline Circuits<br>
+Matt Kaufmann and David Russinoff<br>
+<i>ACL2 Workshop 2000 Proceedings</i>, Austin, TX, October 2000.<br><br>
+
+You can also obtain:<br>
+
+<a HREF="../supporting-materials.tar.gz">A gzipped tar file for this directory</a>.
+
+<p>
+
+To certify book <code>main</code>:
+<ul>
+<li> Edit the fourth form in cert.lisp, as indicated.
+<li> Execute the following in the shell:
+<pre>
+cat cert.lisp | acl2
+</pre>
+</ul>
+
+Contents of this directory:
+
+<p>
+
+<table>
+
+<tr>
+<td><code>README.html</code></td>
+<td>this file</td>
+
+<tr>
+<td><code><A HREF="cert.lisp">cert.lisp</A></code></td>
+<td>for certifying books</td>
+</tr>
+
+<tr>
+<td><code><A HREF="declarations.lisp">declarations.lisp&nbsp;&nbsp;</A></code></td>
+<td>input axioms for <code>"*"</code> model</td>
+</tr>
+
+<tr>
+<td><code><A HREF="inputs.lisp">inputs.lisp</A></code></td>
+<td>input contraints for sequential model</td>
+</tr>
+
+<tr>
+<td><code><A HREF="main.lisp">main.lisp</A></code></td>
+<td>proof of main result</td>
+</tr>
+
+<tr>
+<td><code><A HREF="packages.lisp">packages.lisp</A></code></td>
+<td>package definitions</td>
+</tr>
+
+<tr>
+<td><code><A HREF="toy.rtl">toy.rtl</A></code></td>
+<td>RTL source</td>
+</tr>
+
+<tr>
+<td COLSPAN="2">And, the following automatically-generated files:</td>
+</tr>
+
+<tr>
+<td><code><A HREF="constants.lisp">constants.lisp</A></code></td>
+<td><code>"*"</code> model</td>
+</tr>
+
+<tr>
+<td><code><A HREF="exec.lisp">exec.lisp</A></code></td>
+<td><code>"+"</code> model</td>
+</tr>
+
+<tr>
+<td><code><A HREF="model.lisp">model.lisp</A></code></td>
+<td>sequential (<code>"ACL2"</code>) model</td>
+</tr>
+
+<tr>
+<td><code><A HREF="pipe.lisp">pipe.lisp</A></code></td>
+<td>edited slightly as shown</td>
+</tr>
+
+</table>
+
+</body>
+</html>