diff options
Diffstat (limited to 'books/workshops/2000/russinoff-kaufmann/supporting-materials')
17 files changed, 645 insertions, 0 deletions
diff --git a/books/workshops/2000/russinoff-kaufmann/supporting-materials/constants.acl2 b/books/workshops/2000/russinoff-kaufmann/supporting-materials/constants.acl2 new file mode 100644 index 0000000..4e9ca35 --- /dev/null +++ b/books/workshops/2000/russinoff-kaufmann/supporting-materials/constants.acl2 @@ -0,0 +1,16 @@ +(value :q) +(lp) + +(ld "packages.lsp") + +(include-book "../../../../rtl/rel1/lib3/top") + +(encapsulate ((unknown (key size n) t)) + (local (defun unknown (key size n) (declare (ignore key size n)) 0)) + (defthm bvecp-unknown (bvecp (unknown key size n) size) + :hints (("Goal" :in-theory (enable bvecp))) + :rule-classes (:type-prescription + :rewrite + (:forward-chaining :trigger-terms ((unknown key size n)))))) + +(certify-book "constants" ? t) diff --git a/books/workshops/2000/russinoff-kaufmann/supporting-materials/constants.lisp b/books/workshops/2000/russinoff-kaufmann/supporting-materials/constants.lisp new file mode 100644 index 0000000..6ebcb78 --- /dev/null +++ b/books/workshops/2000/russinoff-kaufmann/supporting-materials/constants.lisp @@ -0,0 +1,43 @@ +(IN-PACKAGE "*") + +(INCLUDE-BOOK "exec") + +(INCLUDE-BOOK "declarations") + +(DEFUN LONGOP_FLOPPED + NIL (+::LONGOP_FLOPPED (LONGOP))) + +(DEFUN S01 NIL (+::S01 (IN))) + +(DEFUN S01_MUXED + NIL (+::S01_MUXED (LONGOP) (S01))) + +(DEFUN S01_MUXED_FLOPPED + NIL (+::S01_MUXED_FLOPPED (S01_MUXED))) + +(DEFUN S23 NIL (+::S23 (IN))) + +(DEFUN S23_FLOPPED NIL (+::S23_FLOPPED (S23))) + +(DEFUN S0123 NIL + (+::S0123 (S01_MUXED_FLOPPED) + (S23_FLOPPED))) + +(DEFUN OUT NIL + (+::OUT (LONGOP_FLOPPED) + (S01_MUXED_FLOPPED) + (S0123))) + +(IN-THEORY (DISABLE (:EXECUTABLE-COUNTERPART LONGOP_FLOPPED) + (:EXECUTABLE-COUNTERPART S01) + (:EXECUTABLE-COUNTERPART S01_MUXED) + (:EXECUTABLE-COUNTERPART S01_MUXED_FLOPPED) + (:EXECUTABLE-COUNTERPART S23) + (:EXECUTABLE-COUNTERPART S23_FLOPPED) + (:EXECUTABLE-COUNTERPART S0123) + (:EXECUTABLE-COUNTERPART OUT))) + +(IN-THEORY (DISABLE LONGOP_FLOPPED + S01 S01_MUXED S01_MUXED_FLOPPED + S23 S23_FLOPPED S0123 OUT)) + diff --git a/books/workshops/2000/russinoff-kaufmann/supporting-materials/declarations.acl2 b/books/workshops/2000/russinoff-kaufmann/supporting-materials/declarations.acl2 new file mode 100644 index 0000000..e797016 --- /dev/null +++ b/books/workshops/2000/russinoff-kaufmann/supporting-materials/declarations.acl2 @@ -0,0 +1,17 @@ +(value :q) +(lp) + +(ld "packages.lsp") + +;; (include-book "rtl/rel9/lib/top" :dir :system) ; breaks constants.lisp +(include-book "rtl/rel1/lib3/top" :dir :system) + +(encapsulate ((unknown (key size n) t)) + (local (defun unknown (key size n) (declare (ignore key size n)) 0)) + (defthm bvecp-unknown (bvecp (unknown key size n) size) + :hints (("Goal" :in-theory (enable bvecp))) + :rule-classes (:type-prescription + :rewrite + (:forward-chaining :trigger-terms ((unknown key size n)))))) + +(certify-book "declarations" ? t) diff --git a/books/workshops/2000/russinoff-kaufmann/supporting-materials/declarations.lisp b/books/workshops/2000/russinoff-kaufmann/supporting-materials/declarations.lisp new file mode 100644 index 0000000..ad871ff --- /dev/null +++ b/books/workshops/2000/russinoff-kaufmann/supporting-materials/declarations.lisp @@ -0,0 +1,11 @@ +(in-package "*") + +(encapsulate ; Input declarations. + ((in () t) + (longop () t)) + (local (defun in () 0)) + (local (defun longop () 0)) + (defthm acl2::input-spec-thm + (and (bvecp (in) 4) + (bvecp (longop) 1)) + :rule-classes ())) diff --git a/books/workshops/2000/russinoff-kaufmann/supporting-materials/exec.acl2 b/books/workshops/2000/russinoff-kaufmann/supporting-materials/exec.acl2 new file mode 100644 index 0000000..1cec3e7 --- /dev/null +++ b/books/workshops/2000/russinoff-kaufmann/supporting-materials/exec.acl2 @@ -0,0 +1,16 @@ +(value :q) +(lp) + +(ld "packages.lsp") + +(include-book "../../../../rtl/rel1/lib3/top") + +(encapsulate ((unknown (key size n) t)) + (local (defun unknown (key size n) (declare (ignore key size n)) 0)) + (defthm bvecp-unknown (bvecp (unknown key size n) size) + :hints (("Goal" :in-theory (enable bvecp))) + :rule-classes (:type-prescription + :rewrite + (:forward-chaining :trigger-terms ((unknown key size n)))))) + +(certify-book "exec" ? t) diff --git a/books/workshops/2000/russinoff-kaufmann/supporting-materials/exec.lisp b/books/workshops/2000/russinoff-kaufmann/supporting-materials/exec.lisp new file mode 100644 index 0000000..58f3319 --- /dev/null +++ b/books/workshops/2000/russinoff-kaufmann/supporting-materials/exec.lisp @@ -0,0 +1,44 @@ +(IN-PACKAGE "+") + +(DEFUN LONGOP_FLOPPED (LONGOP) LONGOP) + +(DEFUN S01 (IN) + (LOGAND (BITN IN 0) (BITN IN 1))) + +(DEFUN S01_MUXED (LONGOP S01) + (IF (EQL LONGOP 0) (COMP1 S01 1) S01)) + +(DEFUN S01_MUXED_FLOPPED (S01_MUXED) + S01_MUXED) + +(DEFUN S23 (IN) + (LOGAND (BITN IN 2) (BITN IN 3))) + +(DEFUN S23_FLOPPED (S23) S23) + +(DEFUN S0123 (S01_MUXED_FLOPPED S23_FLOPPED) + (LOGAND S01_MUXED_FLOPPED S23_FLOPPED)) + +(DEFUN OUT + (LONGOP_FLOPPED S01_MUXED_FLOPPED S0123) + (IF (EQL LONGOP_FLOPPED 0) + S01_MUXED_FLOPPED S0123)) + +(SET-IRRELEVANT-FORMALS-OK T) + +(SET-IGNORE-OK T) + +(DEFUN ACL2::TOY (VAR LONGOP IN) + (LET* ((LONGOP_FLOPPED (LONGOP_FLOPPED LONGOP)) + (S01 (S01 IN)) + (S01_MUXED (S01_MUXED LONGOP S01)) + (S01_MUXED_FLOPPED (S01_MUXED_FLOPPED S01_MUXED)) + (S23 (S23 IN)) + (S23_FLOPPED (S23_FLOPPED S23)) + (S0123 (S0123 S01_MUXED_FLOPPED S23_FLOPPED)) + (OUT (OUT LONGOP_FLOPPED + S01_MUXED_FLOPPED S0123))) + (CASE VAR (ACL2::OUT OUT) + (T (STRING-APPEND (SYMBOL-NAME VAR) + " is not a valid output"))))) + 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 </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> diff --git a/books/workshops/2000/russinoff-kaufmann/supporting-materials/inputs.acl2 b/books/workshops/2000/russinoff-kaufmann/supporting-materials/inputs.acl2 new file mode 100644 index 0000000..5a09b8e --- /dev/null +++ b/books/workshops/2000/russinoff-kaufmann/supporting-materials/inputs.acl2 @@ -0,0 +1,16 @@ +(value :q) +(lp) + +(ld "packages.lsp") + +(include-book "../../../../rtl/rel1/lib3/top") + +(encapsulate ((unknown (key size n) t)) + (local (defun unknown (key size n) (declare (ignore key size n)) 0)) + (defthm bvecp-unknown (bvecp (unknown key size n) size) + :hints (("Goal" :in-theory (enable bvecp))) + :rule-classes (:type-prescription + :rewrite + (:forward-chaining :trigger-terms ((unknown key size n)))))) + +(certify-book "inputs" ? t) diff --git a/books/workshops/2000/russinoff-kaufmann/supporting-materials/inputs.lisp b/books/workshops/2000/russinoff-kaufmann/supporting-materials/inputs.lisp new file mode 100644 index 0000000..be58d11 --- /dev/null +++ b/books/workshops/2000/russinoff-kaufmann/supporting-materials/inputs.lisp @@ -0,0 +1,11 @@ +(in-package "ACL2") + +(include-book "model") ; ACL2 model + +(defun input-assumptions (n) + (and (not (zp n)) + +; "Long op" is initiated at n and asserted at n+2. + + (equal (longop n) 1) + (equal (longop (+ 1 n)) 1))) diff --git a/books/workshops/2000/russinoff-kaufmann/supporting-materials/main.acl2 b/books/workshops/2000/russinoff-kaufmann/supporting-materials/main.acl2 new file mode 100644 index 0000000..f201349 --- /dev/null +++ b/books/workshops/2000/russinoff-kaufmann/supporting-materials/main.acl2 @@ -0,0 +1,16 @@ +(value :q) +(lp) + +(ld "packages.lsp") + +(include-book "../../../../rtl/rel1/lib3/top") + +(encapsulate ((unknown (key size n) t)) + (local (defun unknown (key size n) (declare (ignore key size n)) 0)) + (defthm bvecp-unknown (bvecp (unknown key size n) size) + :hints (("Goal" :in-theory (enable bvecp))) + :rule-classes (:type-prescription + :rewrite + (:forward-chaining :trigger-terms ((unknown key size n)))))) + +(certify-book "main" ? t) diff --git a/books/workshops/2000/russinoff-kaufmann/supporting-materials/main.lisp b/books/workshops/2000/russinoff-kaufmann/supporting-materials/main.lisp new file mode 100644 index 0000000..79e8d3e --- /dev/null +++ b/books/workshops/2000/russinoff-kaufmann/supporting-materials/main.lisp @@ -0,0 +1,80 @@ +(in-package "ACL2") + +; Need to define the "*" package, before (certify-book "main" 7): +; (ld "packages.lisp") + +; Include the "*" model. +(include-book "constants") + +; Include input-assumptions. +(include-book "inputs") + +; Here is the desired relation between input and output, given appropriate +; constraints on other signals. +(defun result (in out) + (equal out + (logand (logand (bitn in 0) (bitn in 1)) + (logand (bitn in 2) (bitn in 3))))) + +; We sometimes assume the following relationships between inputs in our two +; models. Eventually we will functionally instantiate the "*" functions with +; the "ACL2" functions, removing any such assumption from our main result. +(defmacro bindings (n) + `(and (equal (*::longop) (longop ,n)) + (equal (*::in) (in ,n)))) + +; The following definition of spec states what must be true of the inputs in +; the "*" model in order to prove the desired result for the "*" model +; (spec-lemma-2 below). It should be straightforward that spec holds of the +; "ACL2" model inputs (spec-lemma-1). + +(defun spec (in longop) + (declare (ignore in)) + (equal longop 1)) + +; This should be easy. +(defthm spec-lemma-1 + (implies (input-assumptions n) + (spec (in n) (longop n)))) + +; Here is where all the effort goes, in general. For our toy model the proof +; is very easy simply by enabling all the "*" functions. +(defthm spec-lemma-2 + (implies (spec (*::in) (*::longop)) + (result (*::in) (*::out))) + :hints (("Goal" :in-theory + (enable *::S01 *::S01_MUXED *::S01_MUXED_FLOPPED + *::S23 *::S23_FLOPPED *::S0123 + *::LONGOP_FLOPPED *::OUT)))) + +; The rest of our development requires only the above facts about the functions +; we now disable, together with pipeline-lemma below. +(in-theory (disable result input-assumptions spec)) + +(encapsulate + () + (local (include-book "pipe")) + (defthm pipeline-lemma + (implies (and (input-assumptions n) + (bindings n)) + (equal (out (+ 2 n)) (*::out))) + :hints (("Goal" + :use ((:definition input-assumptions*)))))) + +(defthm lemma-to-be-instantiated + (implies (and (input-assumptions n) + (bindings n) + (spec (*::in) (*::longop))) + (result (*::in) + (out (+ 2 n))))) + +(defthm correctness-of-pipeline + (implies (input-assumptions n) + (result (in n) + (out (+ 2 n)))) + :hints (("Goal" :use ((:instance + (:functional-instance + lemma-to-be-instantiated + (*::in (lambda () (in k))) + (*::longop (lambda () (longop k)))) + (k n)))))) diff --git a/books/workshops/2000/russinoff-kaufmann/supporting-materials/model.acl2 b/books/workshops/2000/russinoff-kaufmann/supporting-materials/model.acl2 new file mode 100644 index 0000000..c8b45b1 --- /dev/null +++ b/books/workshops/2000/russinoff-kaufmann/supporting-materials/model.acl2 @@ -0,0 +1,16 @@ +(value :q) +(lp) + +(ld "packages.lsp") + +(include-book "../../../../rtl/rel1/lib3/top") + +(encapsulate ((unknown (key size n) t)) + (local (defun unknown (key size n) (declare (ignore key size n)) 0)) + (defthm bvecp-unknown (bvecp (unknown key size n) size) + :hints (("Goal" :in-theory (enable bvecp))) + :rule-classes (:type-prescription + :rewrite + (:forward-chaining :trigger-terms ((unknown key size n)))))) + +(certify-book "model" ? t) diff --git a/books/workshops/2000/russinoff-kaufmann/supporting-materials/model.lisp b/books/workshops/2000/russinoff-kaufmann/supporting-materials/model.lisp new file mode 100644 index 0000000..0c8e542 --- /dev/null +++ b/books/workshops/2000/russinoff-kaufmann/supporting-materials/model.lisp @@ -0,0 +1,73 @@ +(IN-PACKAGE "ACL2") + +(ENCAPSULATE + ((LONGOP (N) T) (IN (N) T)) + (LOCAL (DEFUN LONGOP (N) + (DECLARE (IGNORE N)) + 0)) + (LOCAL (DEFUN IN (N) (DECLARE (IGNORE N)) 0)) + (DEFTHM BVECP$LONGOP (BVECP (LONGOP N) 1) + :RULE-CLASSES + (:REWRITE (:FORWARD-CHAINING :TRIGGER-TERMS ((LONGOP N))) + (:TYPE-PRESCRIPTION :COROLLARY + (AND (INTEGERP (LONGOP N)) + (>= (LONGOP N) 0)) + :HINTS + (("Goal" :IN-THEORY '(IMPLIES BVECP))))) + :HINTS + (("Goal" :IN-THEORY (ENABLE LONGOP)))) + (DEFTHM BVECP$IN (BVECP (IN N) 4) + :RULE-CLASSES + (:REWRITE (:FORWARD-CHAINING :TRIGGER-TERMS ((IN N))) + (:TYPE-PRESCRIPTION :COROLLARY + (AND (INTEGERP (IN N)) (>= (IN N) 0)) + :HINTS + (("Goal" :IN-THEORY '(IMPLIES BVECP))))) + :HINTS + (("Goal" :IN-THEORY (ENABLE IN))))) + +(DEFUN RESET (N) (= N 0)) + +(DEFUN LONGOP_FLOPPED (N) + (IF (ZP N) + (UNKNOWN 'LONGOP_FLOPPED 1 N) + (LONGOP (1- N)))) + +(DEFUN S01 (N) + (LOGAND (BITN (IN N) 0) + (BITN (IN N) 1))) + +(DEFUN S01_MUXED (N) + (IF (EQL (LONGOP N) 0) +;; Rager 11/2014: The rel9 version of comp1 is named lnot. + (COMP1 (S01 N) 1) + (S01 N))) + +(DEFUN S01_MUXED_FLOPPED (N) + (IF (ZP N) + (UNKNOWN 'S01_MUXED_FLOPPED 1 N) + (S01_MUXED (1- N)))) + +(DEFUN S23 (N) + (LOGAND (BITN (IN N) 2) + (BITN (IN N) 3))) + +(DEFUN S23_FLOPPED (N) + (IF (ZP N) + (UNKNOWN 'S23_FLOPPED 1 N) + (S23 (1- N)))) + +(DEFUN S0123 (N) + (IF (ZP N) + (UNKNOWN 'S0123 1 N) + (LOGAND (S01_MUXED_FLOPPED (1- N)) + (S23_FLOPPED (1- N))))) + +(DEFUN OUT (N) + (IF (EQL (LONGOP_FLOPPED N) 0) + (S01_MUXED_FLOPPED N) + (S0123 N))) + +(IN-THEORY (DISABLE S01 S01_MUXED S23 OUT LONGOP_FLOPPED + S01_MUXED_FLOPPED S23_FLOPPED S0123)) + diff --git a/books/workshops/2000/russinoff-kaufmann/supporting-materials/packages.lsp b/books/workshops/2000/russinoff-kaufmann/supporting-materials/packages.lsp new file mode 100644 index 0000000..4080eb9 --- /dev/null +++ b/books/workshops/2000/russinoff-kaufmann/supporting-materials/packages.lsp @@ -0,0 +1,35 @@ +(in-package "ACL2") + +;;ACL2 symbols that are imported by all packages: + +(defmacro shared-symbols () + '(union-eq *acl2-exports* + (union-eq *common-lisp-symbols-from-main-lisp-package* + (union-eq (other-acl2-symbols) + (union-eq (fp-symbols) + (union-eq (rtl-symbols) + (nondet-symbols))))))) + +;;Miscellaneous symbols that are not in *acl2-exports*: + +(defmacro other-acl2-symbols () + ''(zp set-ignore-ok set-irrelevant-formals-ok disable enable defthm string-append)) + +;;Functions that are defioned in the FP library: + +(defmacro fp-symbols () ; many omitted for this toy + ''(fl cg)) + +;;RTL functions: + +(defmacro rtl-symbols () + ''(?? log< log<= log> log>= log= log<> logand1 logior1 comp1 bitn bits shft cat mulcat bvecp)) + +;;Nondeterministic functions: + +(defmacro nondet-symbols () ; many omitted for this toy + ''(natp unknown)) + +(defpkg "*" (shared-symbols)) + +(defpkg "+" (shared-symbols)) diff --git a/books/workshops/2000/russinoff-kaufmann/supporting-materials/pipe.acl2 b/books/workshops/2000/russinoff-kaufmann/supporting-materials/pipe.acl2 new file mode 100644 index 0000000..3aacf91 --- /dev/null +++ b/books/workshops/2000/russinoff-kaufmann/supporting-materials/pipe.acl2 @@ -0,0 +1,16 @@ +(value :q) +(lp) + +(ld "packages.lsp") + +(include-book "../../../../rtl/rel1/lib3/top") + +(encapsulate ((unknown (key size n) t)) + (local (defun unknown (key size n) (declare (ignore key size n)) 0)) + (defthm bvecp-unknown (bvecp (unknown key size n) size) + :hints (("Goal" :in-theory (enable bvecp))) + :rule-classes (:type-prescription + :rewrite + (:forward-chaining :trigger-terms ((unknown key size n)))))) + +(certify-book "pipe" ? t) diff --git a/books/workshops/2000/russinoff-kaufmann/supporting-materials/pipe.lisp b/books/workshops/2000/russinoff-kaufmann/supporting-materials/pipe.lisp new file mode 100644 index 0000000..56b9098 --- /dev/null +++ b/books/workshops/2000/russinoff-kaufmann/supporting-materials/pipe.lisp @@ -0,0 +1,121 @@ +(IN-PACKAGE "ACL2") + +; !! Our original approach was to include the following book in the portcullis. +(include-book "model") +(include-book "constants") +(include-book "inputs") + +(DEFUN INPUT-BINDINGS (N) + (AND (EQUAL (*::LONGOP) (LONGOP N)) + (EQUAL (*::IN) (IN N)))) + +(DEFUN INPUT-ASSUMPTIONS* (N) + (AND (INPUT-ASSUMPTIONS N) + (INPUT-BINDINGS N))) + +(DEFTHM INPUT$INPUT* + (IMPLIES (INPUT-ASSUMPTIONS* N) + (INPUT-ASSUMPTIONS N))) + +(DEFTHM INPUT$BINDINGS + (IMPLIES (INPUT-ASSUMPTIONS* N) + (AND (EQUAL (*::IN) (IN N)) + (EQUAL (*::LONGOP) (LONGOP N))))) + +(IN-THEORY (DISABLE INPUT-ASSUMPTIONS* + (INPUT-ASSUMPTIONS*))) + +;;********************************************************************* + +(DEFTHM SIMP$LONGOP$1 + (IMPLIES (INPUT-ASSUMPTIONS N) + (EQUAL (LONGOP (+ 1 N)) 1)) + :HINTS + (("Goal" :IN-THEORY (ENABLE INPUT-ASSUMPTIONS)))) + +(DEFTHM SIMP$LONGOP$0 + (IMPLIES (INPUT-ASSUMPTIONS N) + (EQUAL (LONGOP N) 1)) + :HINTS + (("Goal" :IN-THEORY (ENABLE INPUT-ASSUMPTIONS)))) + +(DEFTHM LONGOP_FLOPPED$PIPE$REWRITE + (IMPLIES (INPUT-ASSUMPTIONS* N) + (EQUAL (*::LONGOP_FLOPPED) 1)) + :HINTS + (("Goal" :IN-THEORY + (ENABLE LONGOP_FLOPPED *::LONGOP_FLOPPED)))) + +(DEFTHM SIMP$LONGOP_FLOPPED$1 + (IMPLIES (INPUT-ASSUMPTIONS N) + (EQUAL (LONGOP_FLOPPED (+ 1 N)) 1)) + :HINTS + (("Goal" :IN-THEORY (ENABLE LONGOP_FLOPPED)))) + +(DEFTHM SIMP$LONGOP_FLOPPED$2 + (IMPLIES (INPUT-ASSUMPTIONS N) + (EQUAL (LONGOP_FLOPPED (+ 2 N)) 1)) + :HINTS + (("Goal" :IN-THEORY (ENABLE LONGOP_FLOPPED)))) + +;;********************************************************************* + +(DEFTHM S01$PIPE$REWRITE + (IMPLIES (INPUT-ASSUMPTIONS* N) + (EQUAL (*::S01) (S01 N))) + :HINTS + (("Goal" :IN-THEORY (ENABLE S01 *::S01)))) + +(DEFTHM S01_MUXED$PIPE$REWRITE + (IMPLIES (INPUT-ASSUMPTIONS* N) + (EQUAL (*::S01_MUXED) (S01_MUXED N))) + :HINTS + (("Goal" :IN-THEORY + (ENABLE S01_MUXED *::S01_MUXED)))) + +; !! The following is needed for S01_MUXED_FLOPPED$PIPE$REWRITE. + +(defthm input-assumptions*-forward + (implies (input-assumptions* n) + (and (integerp n) + (< 0 n) + (equal (longop n) 1) + (equal (longop (+ 1 n)) 1))) + :hints (("Goal" :in-theory (enable input-assumptions*))) + :rule-classes :forward-chaining) + +(DEFTHM S01_MUXED_FLOPPED$PIPE$REWRITE + (IMPLIES (INPUT-ASSUMPTIONS* N) + (EQUAL (*::S01_MUXED_FLOPPED) + (S01_MUXED_FLOPPED (+ 1 N)))) + :HINTS + (("Goal" :IN-THEORY + (ENABLE S01_MUXED_FLOPPED + *::S01_MUXED_FLOPPED)))) + +(DEFTHM S23$PIPE$REWRITE + (IMPLIES (INPUT-ASSUMPTIONS* N) + (EQUAL (*::S23) (S23 N))) + :HINTS + (("Goal" :IN-THEORY (ENABLE S23 *::S23)))) + +(DEFTHM S23_FLOPPED$PIPE$REWRITE + (IMPLIES (INPUT-ASSUMPTIONS* N) + (EQUAL (*::S23_FLOPPED) + (S23_FLOPPED (+ 1 N)))) + :HINTS + (("Goal" :IN-THEORY + (ENABLE S23_FLOPPED *::S23_FLOPPED)))) + +(DEFTHM S0123$PIPE$REWRITE + (IMPLIES (INPUT-ASSUMPTIONS* N) + (EQUAL (*::S0123) (S0123 (+ 2 N)))) + :HINTS + (("Goal" :IN-THEORY (ENABLE S0123 *::S0123)))) + +(DEFTHM OUT$PIPE$REWRITE + (IMPLIES (INPUT-ASSUMPTIONS* N) + (EQUAL (*::OUT) (OUT (+ 2 N)))) + :HINTS + (("Goal" :IN-THEORY (ENABLE OUT *::OUT)))) + diff --git a/books/workshops/2000/russinoff-kaufmann/supporting-materials/toy.rtl b/books/workshops/2000/russinoff-kaufmann/supporting-materials/toy.rtl new file mode 100644 index 0000000..3c72d76 --- /dev/null +++ b/books/workshops/2000/russinoff-kaufmann/supporting-materials/toy.rtl @@ -0,0 +1,21 @@ +module toy; + +input in[3:0]; +input longop; +output out; + +s01 = in[0] & in[1]; +s23 = in[2] & in[3]; + +s01_muxed = (longop) ? s01 : ~s01; // or, (longop == s01) + +s01_muxed_flopped <= s01_muxed; +s23_flopped <= s23; + +s0123 <= s01_muxed_flopped & s23_flopped; + +longop_flopped <= longop; + +out = (longop_flopped) ? s0123 : s01_muxed_flopped; + +endmodule // toy |