[acl2-books] r2767 committed - Reversed names to respect the order of authors on the paper.

[acl2-...@googlecode.com]

Revision: 2767
Author: kauf...@cs.utexas.edu
Date: Thu May 22 13:28:24 2014 UTC
Log: Reversed names to respect the order of authors on the paper.
http://code.google.com/p/acl2-books/source/detail?r=2767

Added:
/trunk/workshops/2014/russinoff-oleary
/trunk/workshops/2014/russinoff-oleary/support
/trunk/workshops/2014/russinoff-oleary/support/README
/trunk/workshops/2014/russinoff-oleary/support/imul.ast.lsp
/trunk/workshops/2014/russinoff-oleary/support/imul.cpp
/trunk/workshops/2014/russinoff-oleary/support/imul.lisp
/trunk/workshops/2014/russinoff-oleary/support/imul.m
/trunk/workshops/2014/russinoff-oleary/support/masc.h
/trunk/workshops/2014/russinoff-oleary/support/proof.lisp
/trunk/workshops/2014/russinoff-oleary/support/translate.lisp
Deleted:
/trunk/workshops/2014/oleary-russinoff

=======================================
--- /dev/null
+++ /trunk/workshops/2014/russinoff-oleary/support/README Thu May 22
13:28:24 2014 UTC
@@ -0,0 +1,70 @@
+This directory contains the following files:
+
+masc.h: The class templates that must be loaded with any MASC SystemC
model.
+
+translate.lisp: The translator that converts the S-expression
representation
+ of a MASC model (generated by the MASC parser) to an ACL2
program.
+
+imul.cpp: A SystemC model of a 32-bit radix-4 Booth integer multiplier.
+
+imul.m: The MASC version of the model generated by the MASC parser.
+
+imul.ast.lsp: The S-expression representation of the model generated by
+ the MASC parser.
+
+imul.lisp: The ACL2 translation of the model generated by the MASC parser
+ and "translate.lisp".
+
+proof.lisp: The script for a proof of correctness of the model.
+
+------------------------------------------------------------------------------
+
+Note that our use of GL requires that we also use ACL2H, the experimental
+modification of ACL2 for HONS, memoization, and applicative hash tables.
+
+------------------------------------------------------------------------------
+
+The file imul.lisp may be recreated and certified as follows:
+
+ACL2 !>(certify-book "translate")
+
+ACL2 !>(translate-program "imul.ast.lsp" "imul.lisp" state)
+
+ACL2 !>:u
+
+ACL2 !>(set-inhibit-output-lst '(prove event proof-tree))
+
+ACL2 !>(certify-book "imul")
+
+------------------------------------------------------------------------------
+
+The function imultest takes a pair of 32-bit integers and returns 3 values.
+The first is a boolean (1 or 0) indicating agreement between the other two,
+which are the products computed by * and imul, respectively:
+
+
+ACL2 !>(include-book "imul")
+
+ACL2 !>(imultest 2 3)
+(imultest 2 3)
+(1 6 6)
+
+ACL2 !>(set-print-base 16 state)
+(set-print-base 16 state)
+<state>
+
+ACL2 !>(imultest #xFEDCBA98 #x12345678)
+(imultest #xFEDCBA98 #x12345678)
+(1 121FA00A35068740 121FA00A35068740)
+
+------------------------------------------------------------------------------
+
+To certify the proof script:
+
+ACL2 !>:ubt! 1
+
+ACL2 !>(include-book "centaur/gl/gl" :dir :system)
+
+ACL2 !>(certify-book "proof" 1)
+
+
=======================================
--- /dev/null
+++ /trunk/workshops/2014/russinoff-oleary/support/imul.ast.lsp Thu May 22
13:28:24 2014 UTC
@@ -0,0 +1,26 @@
+
+
+(funcdef Encode (slice) (block (declare enc 0) (switch slice (4 (assign
enc (bits 6 2
+ 0))) ((5 6) (assign enc (bits 5 2
+ 0))) ((7 0) (assign enc (bits 0 2
+ 0))) ((1 2) (assign enc (bits 1 2
+ 0))) (3 (assign enc (bits 2 2
+ 0))) (t (assert (false$) Encode))) (return enc)))(funcdef Booth (x)
(block (declare x35 (bits (ash x 1) 34
+ 0)) (declare a ()) (for ((declare k 0) (log< k 17) (+ k 1)) (block
(assign a (as k (Encode (bits x35 (+ (* 2 k) 2) (* 2 k))) a)))) (return
a)))(funcdef PartialProducts (m21 y) (block (declare pp ()) (for ((declare
k 0) (log< k 17) (+ k 1)) (block (declare row 0) (switch (bits (ag k m21) 1
0) (2 (assign row (bits (ash y 1) 32
+ 0))) (1 (assign row y)) (t (assign row (bits 0 32
+ 0)))) (assign pp (as k (bits (if1 (bitn (ag k m21) 2) (lognot row) row) 32
+ 0) pp)))) (return pp)))(funcdef Align (bds pps) (block (declare sb ())
(declare psb ()) (for ((declare k 0) (log< k 17) (+ k 1)) (block (assign sb
(as k (bitn (ag k bds) 2) sb)) (assign psb (as (+ k 1) (bitn (ag k bds) 2)
psb)))) (declare tble ()) (for ((declare k 0) (log< k 17) (+ k 1)) (block
(declare tmp (bits 0 66
+ 0)) (assign tmp (setbits tmp 67
+ (+ (* 2 k) 32) (* 2 k) (ag k pps))) (if (log= k 0) (block (assign tmp
(setbitn tmp 67
+ 33 (ag k sb))) (assign tmp (setbitn tmp 67
+ 34 (ag k sb))) (assign tmp (setbitn tmp 67
+ 35 (lognot1 (ag k sb))))) (block (assign tmp (setbitn tmp 67
+ (- (* 2 k) 2) (ag k psb))) (assign tmp (setbitn tmp 67
+ (+ (* 2 k) 33) (lognot1 (ag k sb)))) (assign tmp (setbitn tmp 67
+ (+ (* 2 k) 34) 1)))) (assign tble (as k (bits tmp 63 0) tble)))) (return
tble)))(funcdef Compress32 (in0 in1 in2) (block (declare out0 (logxor
(logxor in0 in1) in2)) (declare out1 (logior (logior (logand in0 in1)
(logand in0 in2)) (logand in1 in2))) (assign out1 (bits (ash out1 1) 63
+ 0)) (return (mv out0 out1))))(funcdef Compress42 (in0 in1 in2 in3) (block
(declare temp (bits (ash (logior (logior (logand in1 in2) (logand in1 in3))
(logand in2 in3)) 1) 63
+ 0)) (declare out0 (logxor (logxor (logxor (logxor in0 in1) in2) in3)
temp)) (declare out1 (logior (logand in0 (bits (lognot (logxor (logxor
(logxor in0 in1) in2) in3)) 63
+ 0)) (logand temp (logxor (logxor (logxor in0 in1) in2) in3)))) (assign
out1 (bits (ash out1 1) 63
+ 0)) (return (mv out0 out1))))(funcdef Sum (in) (block (declare A1 ())
(for ((declare i 0) (log< i 4) (+ i 1)) (block (block (declare temp-1)
(declare temp-0) (mv-assign (temp-0 temp-1) (Compress42 (ag (* 4 i) in) (ag
(+ (* 4 i) 1) in) (ag (+ (* 4 i) 2) in) (ag (+ (* 4 i) 3) in))) (assign A1
(as (+ (* 2 i) 0) temp-0 A1)) (assign A1 (as (+ (* 2 i) 1) temp-1 A1)))))
(declare A2 ()) (for ((declare i 0) (log< i 2) (+ i 1)) (block (block
(declare temp-1) (declare temp-0) (mv-assign (temp-0 temp-1) (Compress42
(ag (* 4 i) A1) (ag (+ (* 4 i) 1) A1) (ag (+ (* 4 i) 2) A1) (ag (+ (* 4 i)
3) A1))) (assign A2 (as (+ (* 2 i) 0) temp-0 A2)) (assign A2 (as (+ (* 2 i)
1) temp-1 A2))))) (declare A3 ()) (block (declare temp-1) (declare temp-0)
(mv-assign (temp-0 temp-1) (Compress42 (ag 0 A2) (ag 1 A2) (ag 2 A2) (ag 3
A2))) (assign A3 (as 0 temp-0 A3)) (assign A3 (as 1 temp-1 A3))) (declare
A4 ()) (block (declare temp-1) (declare temp-0) (mv-assign (temp-0 temp-1)
(Compress32 (ag 0 A3) (ag 1 A3) (ag 16 in))) (assign A4 (as 0 temp-0 A4))
(assign A4 (as 1 temp-1 A4))) (return (bits (+ (ag 0 A4) (ag 1 A4)) 63
+ 0))))(funcdef Imul (s1 s2) (block (declare bd (Booth s1)) (declare pp
(PartialProducts bd s2)) (declare tble (Align bd pp)) (declare prod (Sum
tble)) (return prod)))(funcdef ImulTest (s1 s2) (block (declare spec_result
(bits (* s1 s2) 63
+ 0)) (declare imul_result (Imul s1 s2)) (return (mv (log= spec_result
imul_result) spec_result imul_result))))
=======================================
--- /dev/null
+++ /trunk/workshops/2014/russinoff-oleary/support/imul.cpp Thu May 22
13:28:24 2014 UTC
@@ -0,0 +1,235 @@
+// Simple Masc example: integer multiplication
+// John O'Leary, 28 May 2013
+
+#include <systemc.h>
+#include <masc.h>
+
+// Masc begin
+
+// This Masc code describes a 32x32 -> 64 unsigned integer multiplier
+// Adapted from significand_multiplier_r4_param in Warren Ferguson's
+// library of Verilog reference models.
+
+typedef sc_uint<32> ui32;
+typedef sc_uint<64> ui64;
+typedef sc_uint<35> ui35;
+typedef sc_uint<3> ui3;
+typedef sc_biguint<33> ui33;
+typedef sc_biguint<67> ui67;
+
+// Step 1: construct an array of radix-4 digits for a source multiplier.
+
+// For each 3-bit slice x[2*k+1:2*k-1] of the multiplier, we compute a
+// 3-bit sign-magnitude encoding of x[2*k-1] + x[2*k] - 2 * x[2*k+1]:
+
+ui3 Encode(ui3 slice) {
+ ui3 enc;
+ switch (slice) {
+ case 4:
+ enc = 6; // -2 -> 110
+ break;
+ case 5: case 6:
+ enc = 5; // -1 -> 101
+ break;
+ case 7: case 0:
+ enc = 0; // 0 -> 000
+ break;
+ case 1: case 2:
+ enc = 1; // +1 -> 001
+ break;
+ case 3:
+ enc = 2; // +2 -> 010
+ break;
+ default:
+ assert(false);
+ }
+ return enc;
+}
+
+array<17, ui3> Booth (ui32 x) {
+
+ // Pad the multiplier with 2 leading zeroes and 1 trailing zero:
+ ui35 x35 = x << 1;
+
+ // Compute the booth encodings:
+ array<17, ui3> a;
+ for (int k=0; k<17; k++) {
+ a.elt[k] = Encode(x35.range(2*k+2, 2*k));
+ }
+ return a;
+}
+
+// Step 2: Form the partial products.
+
+array<17, ui33> PartialProducts (array<17, ui3> m21, ui32 y) {
+ array<17, ui33> pp;
+
+ for (int k=0; k<17; k++) {
+ ui33 row;
+ switch (m21.elt[k].range(1,0).to_uint()) {
+ case 2:
+ row = y << 1;
+ break;
+ case 1:
+ row = y;
+ break;
+ default:
+ row = 0;
+ }
+ pp.elt[k] = m21.elt[k][2] ? ~row : row;
+ }
+
+ return pp;
+}
+
+// Step 3: Construct the table of aligned partial products.
+
+array<17, ui64> Align(array<17, ui3> bds, array<17, ui33> pps) {
+
+ // Extract the sign bits from the booth encodings:
+ array<17, bool> sb;
+ array<18, bool> psb;
+ for (int k=0; k<17; k++) {
+ sb.elt[k] = bds.elt[k][2];
+ psb.elt[k+1] = bds.elt[k][2];
+ }
+
+ // Build the table:
+ array<17, ui64> tble;
+ for (int k=0; k<17; k++) {
+ ui67 tmp = 0;
+ tmp.range(2*k+32, 2*k) = pps.elt[k];
+ if (k == 0) {
+ tmp[33] = sb.elt[k];
+ tmp[34] = sb.elt[k];
+ tmp[35] = !sb.elt[k];
+ }
+ else {
+ tmp[2*k-2] = psb.elt[k];
+ tmp[2*k+33] = !sb.elt[k];
+ tmp[2*k+34] = 1;
+ }
+
+ tble.elt[k] = tmp.range(63, 0);
+ }
+
+ return tble;
+}
+
+// Step 4: Sum the rows of the table of aligned partial products
+
+// The compression tree is constucted from two basic modules:
+
+mv<ui64, ui64> Compress32(ui64 in0, ui64 in1, ui64 in2) {
+ ui64 out0 = in0 ^ in1 ^ in2;
+ ui64 out1 = in0 & in1 | in0 &in2 | in1 & in2;
+ out1 <<= 1;
+ return mv<ui64, ui64>(out0, out1);
+}
+
+mv<ui64, ui64> Compress42(ui64 in0, ui64 in1, ui64 in2, ui64 in3) {
+ ui64 temp = (in1 & in2 | in1 & in3 | in2 & in3) << 1;
+ ui64 out0 = in0 ^ in1 ^ in2 ^ in3 ^ temp;
+ ui64 out1 = (in0 & ~(in0 ^ in1 ^ in2 ^ in3)) | (temp & (in0 ^ in1 ^ in2
^ in3));
+ out1 <<= 1;
+ return mv<ui64, ui64>(out0, out1);
+}
+
+ui64 Sum(array<17, ui64> in) {
+
+ // level 1 consists of 4 4:2 compressors
+ array<8, ui64> A1;
+ for (uint i=0; i<4; i++) {
+ Compress42(in.elt[4*i], in.elt[4*i+1], in.elt[4*i+2],
in.elt[4*i+3]).assign(A1.elt[2*i+0], A1.elt[2*i+1]);
+ }
+
+ // level 2 consists of 2 4:2 compressors
+ array<4, ui64> A2;
+ for (uint i=0; i<2; i++) {
+ Compress42(A1.elt[4*i], A1.elt[4*i+1], A1.elt[4*i+2],
A1.elt[4*i+3]).assign(A2.elt[2*i+0], A2.elt[2*i+1]);
+ }
+
+ // level 3 consists of 1 4:2 compressor
+ array<2, ui64> A3;
+ Compress42(A2.elt[0], A2.elt[1], A2.elt[2], A2.elt[3]).assign(A3.elt[0],
A3.elt[1]);
+
+ // level 4 consists of 1 3:2 compressor
+ array<2, ui64> A4;
+ Compress32(A3.elt[0], A3.elt[1], in.elt[16]).assign(A4.elt[0],
A4.elt[1]);
+
+ // The final sum:
+ return A4.elt[0] + A4.elt[1];
+}
+
+// Stitch it together
+
+ui64 Imul(ui32 s1, ui32 s2) {
+
+// cout << "Operands: << endl;
+// cout << hex << s1 << endl;
+// cout << hex << s1 << endl;
+
+ array<17, ui3> bd = Booth(s1);
+
+// cout << "Booth digits:" << endl;
+// for (int i=0; i<17; i++) {
+// cout << i << ": " << bds.elt[i][2] << bds.elt[i][1] <<
bds.elt[i][0] << endl;
+// }
+
+ array<17, ui33> pp = PartialProducts(bd, s2);
+
+// cout << "Partial products:" << endl;
+// for (int i=0; i<17; i++) {
+// cout << i << ": " << hex << pps.elt[i] << endl;
+// }
+
+ array<17, ui64> tble = Align (bd, pp);
+
+// cout << "Aligned partial products:" << endl;
+// for (int i=0; i<17; i++) {
+// cout << i << ": " << hex << tble.elt[i] << endl;
+// }
+
+ ui64 prod = Sum(tble);
+
+// cout << "Product: << endl;
+// cout << hex << prod << endl;
+
+ return prod;
+
+}
+
+mv<bool, ui64, ui64>ImulTest(ui32 s1, ui32 s2) {
+ ui64 spec_result = s1 * s2;
+ ui64 imul_result = Imul(s1, s2);
+ return mv<bool, ui64, ui64>(spec_result == imul_result, spec_result,
imul_result);
+}
+
+// Masc end
+
+int sc_main (int argc, char *argv[]) {
+
+ ui32 src1;
+ ui32 src2;
+ ui64 spec_result;
+ ui64 imul_result;
+ bool passed;
+
+ while (! cin.eof()) {
+
+ cin >> src1;
+ cin >> src2;
+
+ ImulTest(src1, src2).assign(passed, spec_result, imul_result);
+
+ cout << src1 << " " << src2 << " " << imul_result << " ";
+ if (passed) {
+ cout << "passed";
+ } else {
+ cout << "failed (spec: " << spec_result << "; imul: " << imul_result
<< ")";
+ }
+ cout << endl;
+ }
+
+}
+
=======================================
--- /dev/null
+++ /trunk/workshops/2014/russinoff-oleary/support/imul.lisp Thu May 22
13:28:24 2014 UTC
@@ -0,0 +1,185 @@
+(IN-PACKAGE "ACL2")
+
+; Note: Below, :DIR :SYSTEM has been manually moved onto the same line as
+; INCLUDE-BOOK, in order to support the use of cert.pl.
+(INCLUDE-BOOK "rtl/rel9/lib/masc" :DIR :SYSTEM)
+
+(SET-IGNORE-OK T)
+
+(SET-IRRELEVANT-FORMALS-OK T)
+
+(DEFUN ENCODE (SLICE)
+ (LET ((ENC 0))
+ (CASE SLICE (4 (BITS 6 2 0))
+ ((5 6) (BITS 5 2 0))
+ ((7 0) (BITS 0 2 0))
+ ((1 2) (BITS 1 2 0))
+ (3 (BITS 2 2 0))
+ (T (LET ((ASSERT (IN-FUNCTION ENCODE (FALSE$))))
+ ENC)))))
+
+(DEFUN BOOTH-LOOP-0 (K X35 A)
+ (DECLARE (XARGS :MEASURE (NFIX (- 17 K))))
+ (IF (AND (INTEGERP K) (< K 17))
+ (LET ((A (AS K
+ (ENCODE (BITS X35 (+ (* 2 K) 2) (* 2 K)))
+ A)))
+ (BOOTH-LOOP-0 (+ K 1) X35 A))
+ A))
+
+(DEFUN BOOTH (X)
+ (LET ((X35 (BITS (ASH X 1) 34 0)) (A NIL))
+ (BOOTH-LOOP-0 0 X35 A)))
+
+(DEFUN PARTIALPRODUCTS-LOOP-0 (K Y M21 PP)
+ (DECLARE (XARGS :MEASURE (NFIX (- 17 K))))
+ (IF (AND (INTEGERP K) (< K 17))
+ (LET* ((ROW 0)
+ (ROW (CASE (BITS (AG K M21) 1 0)
+ (2 (BITS (ASH Y 1) 32 0))
+ (1 Y)
+ (T (BITS 0 32 0))))
+ (PP (AS K
+ (BITS (IF1 (BITN (AG K M21) 2)
+ (LOGNOT ROW)
+ ROW)
+ 32 0)
+ PP)))
+ (PARTIALPRODUCTS-LOOP-0 (+ K 1)
+ Y M21 PP))
+ PP))
+
+(DEFUN PARTIALPRODUCTS (M21 Y)
+ (LET ((PP NIL))
+ (PARTIALPRODUCTS-LOOP-0 0 Y M21 PP)))
+
+(DEFUN ALIGN-LOOP-0 (K PPS PSB SB TBLE)
+ (DECLARE (XARGS :MEASURE (NFIX (- 17 K))))
+ (IF (AND (INTEGERP K) (< K 17))
+ (LET* ((TMP (BITS 0 66 0))
+ (TMP (SETBITS TMP 67 (+ (* 2 K) 32)
+ (* 2 K)
+ (AG K PPS)))
+ (TMP (IF1 (LOG= K 0)
+ (LET* ((TMP (SETBITN TMP 67 33 (AG K SB)))
+ (TMP (SETBITN TMP 67 34 (AG K SB))))
+ (SETBITN TMP 67 35 (LOGNOT1 (AG K SB))))
+ (LET* ((TMP (SETBITN TMP 67 (- (* 2 K) 2)
+ (AG K PSB)))
+ (TMP (SETBITN TMP 67 (+ (* 2 K) 33)
+ (LOGNOT1 (AG K SB)))))
+ (SETBITN TMP 67 (+ (* 2 K) 34) 1))))
+ (TBLE (AS K (BITS TMP 63 0) TBLE)))
+ (ALIGN-LOOP-0 (+ K 1) PPS PSB SB TBLE))
+ TBLE))
+
+(DEFUN ALIGN-LOOP-1 (K BDS SB PSB)
+ (DECLARE (XARGS :MEASURE (NFIX (- 17 K))))
+ (IF (AND (INTEGERP K) (< K 17))
+ (LET ((SB (AS K (BITN (AG K BDS) 2) SB))
+ (PSB (AS (+ K 1) (BITN (AG K BDS) 2) PSB)))
+ (ALIGN-LOOP-1 (+ K 1) BDS SB PSB))
+ (MV SB PSB)))
+
+(DEFUN ALIGN (BDS PPS)
+ (LET ((SB NIL) (PSB NIL))
+ (MV-LET (SB PSB)
+ (ALIGN-LOOP-1 0 BDS SB PSB)
+ (LET ((TBLE NIL))
+ (ALIGN-LOOP-0 0 PPS PSB SB TBLE)))))
+
+(DEFUN COMPRESS32 (IN0 IN1 IN2)
+ (MV (LOGXOR (LOGXOR IN0 IN1) IN2)
+ (BITS (ASH (LOGIOR (LOGIOR (LOGAND IN0 IN1)
+ (LOGAND IN0 IN2))
+ (LOGAND IN1 IN2))
+ 1)
+ 63 0)))
+
+(DEFUN
+ COMPRESS42 (IN0 IN1 IN2 IN3)
+ (LET
+ ((TEMP (BITS (ASH (LOGIOR (LOGIOR (LOGAND IN1 IN2)
+ (LOGAND IN1 IN3))
+ (LOGAND IN2 IN3))
+ 1)
+ 63 0)))
+ (MV
+ (LOGXOR (LOGXOR (LOGXOR (LOGXOR IN0 IN1) IN2)
+ IN3)
+ TEMP)
+ (BITS
+ (ASH (LOGIOR (LOGAND IN0
+ (BITS (LOGNOT (LOGXOR (LOGXOR (LOGXOR IN0
IN1) IN2)
+ IN3))
+ 63 0))
+ (LOGAND TEMP
+ (LOGXOR (LOGXOR (LOGXOR IN0 IN1) IN2)
+ IN3)))
+ 1)
+ 63 0))))
+
+(DEFUN SUM-LOOP-0 (I A1 A2)
+ (DECLARE (XARGS :MEASURE (NFIX (- 2 I))))
+ (IF (AND (INTEGERP I) (< I 2))
+ (LET ((A2 (LET ((TEMP-1 NIL) (TEMP-0 NIL))
+ (MV-LET (TEMP-0 TEMP-1)
+ (COMPRESS42 (AG (* 4 I) A1)
+ (AG (+ (* 4 I) 1) A1)
+ (AG (+ (* 4 I) 2) A1)
+ (AG (+ (* 4 I) 3) A1))
+ (LET ((A2 (AS (+ (* 2 I) 0) TEMP-0 A2)))
+ (AS (+ (* 2 I) 1) TEMP-1 A2))))))
+ (SUM-LOOP-0 (+ I 1) A1 A2))
+ A2))
+
+(DEFUN SUM-LOOP-1 (I IN A1)
+ (DECLARE (XARGS :MEASURE (NFIX (- 4 I))))
+ (IF (AND (INTEGERP I) (< I 4))
+ (LET ((A1 (LET ((TEMP-1 NIL) (TEMP-0 NIL))
+ (MV-LET (TEMP-0 TEMP-1)
+ (COMPRESS42 (AG (* 4 I) IN)
+ (AG (+ (* 4 I) 1) IN)
+ (AG (+ (* 4 I) 2) IN)
+ (AG (+ (* 4 I) 3) IN))
+ (LET ((A1 (AS (+ (* 2 I) 0) TEMP-0 A1)))
+ (AS (+ (* 2 I) 1) TEMP-1 A1))))))
+ (SUM-LOOP-1 (+ I 1) IN A1))
+ A1))
+
+(DEFUN SUM (IN)
+ (LET* ((A1 NIL)
+ (A1 (SUM-LOOP-1 0 IN A1))
+ (A2 NIL)
+ (A2 (SUM-LOOP-0 0 A1 A2))
+ (A3 NIL)
+ (A3 (LET ((TEMP-1 NIL) (TEMP-0 NIL))
+ (MV-LET (TEMP-0 TEMP-1)
+ (COMPRESS42 (AG 0 A2)
+ (AG 1 A2)
+ (AG 2 A2)
+ (AG 3 A2))
+ (LET ((A3 (AS 0 TEMP-0 A3)))
+ (AS 1 TEMP-1 A3)))))
+ (A4 NIL)
+ (A4 (LET ((TEMP-1 NIL) (TEMP-0 NIL))
+ (MV-LET (TEMP-0 TEMP-1)
+ (COMPRESS32 (AG 0 A3)
+ (AG 1 A3)
+ (AG 16 IN))
+ (LET ((A4 (AS 0 TEMP-0 A4)))
+ (AS 1 TEMP-1 A4))))))
+ (BITS (+ (AG 0 A4) (AG 1 A4)) 63 0)))
+
+(DEFUN IMUL (S1 S2)
+ (LET* ((BD (BOOTH S1))
+ (PP (PARTIALPRODUCTS BD S2))
+ (TBLE (ALIGN BD PP)))
+ (SUM TBLE)))
+
+(DEFUN IMULTEST (S1 S2)
+ (LET ((SPEC_RESULT (BITS (* S1 S2) 63 0))
+ (IMUL_RESULT (IMUL S1 S2)))
+ (MV (LOG= SPEC_RESULT IMUL_RESULT)
+ SPEC_RESULT IMUL_RESULT)))
+
=======================================
--- /dev/null
+++ /trunk/workshops/2014/russinoff-oleary/support/imul.m Thu May 22
13:28:24 2014 UTC
@@ -0,0 +1,130 @@
+
+
+
+ui3 Encode(ui3 slice) {
+ ui3 enc;
+ switch (slice) {
+ case 4:
+ enc = 6;
+ break;
+ case 5:
+ case 6:
+ enc = 5;
+ break;
+ case 7:
+ case 0:
+ enc = 0;
+ break;
+ case 1:
+ case 2:
+ enc = 1;
+ break;
+ case 3:
+ enc = 2;
+ break;
+ default:
+ assert(false);
+ }
+ return enc;
+}
+
+ui3[17] Booth(ui32 x) {
+ ui35 x35 = x << 1;
+ ui3 a[17];
+ for (int k = 0; k < 17; k++) {
+ a[k] = Encode(x35[2 * k + 2:2 * k]);
+ }
+ return a;
+}
+
+ui33[17] PartialProducts(ui3 m21[17], ui32 y) {
+ ui33 pp[17];
+ for (int k = 0; k < 17; k++) {
+ ui33 row;
+ switch (m21[k][1:0]) {
+ case 2:
+ row = y << 1;
+ break;
+ case 1:
+ row = y;
+ break;
+ default:
+ row = 0;
+ }
+ pp[k] = m21[k][2] ? ~row : row;
+ }
+ return pp;
+}
+
+ui64[17] Align(ui3 bds[17], ui33 pps[17]) {
+ ui64 tble[17];
+ bool sb[17];
+ bool psb[18];
+ ui67 tmp;
+ for (int k = 0; k < 17; k++) {
+ sb[k] = bds[k][2];
+ psb[k + 1] = bds[k][2];
+ }
+ for (int k = 0; k < 17; k++) {
+ tmp = 0;
+ tmp[2 * k + 32:2 * k] = pps[k];
+ if (k == 0) {
+ tmp[33] = sb[k];
+ tmp[34] = sb[k];
+ tmp[35] = !sb[k];
+ }
+ else {
+ tmp[2 * k - 2] = psb[k];
+ tmp[2 * k + 33] = !sb[k];
+ tmp[2 * k + 34] = 1;
+ }
+ tble[k] = tmp[63:0];
+ }
+ return tble;
+}
+
+<ui64, ui64> Compress32(ui64 in0, ui64 in1, ui64 in2) {
+ ui64 out0 = in0 ^ in1 ^ in2;
+ ui64 out1 = in0 & in1 | in0 & in2 | in1 & in2;
+ out1 <<= 1;
+ return <out0, out1>;
+}
+
+<ui64, ui64> Compress42(ui64 in0, ui64 in1, ui64 in2, ui64 in3) {
+ ui64 temp = (in1 & in2 | in1 & in3 | in2 & in3) << 1;
+ ui64 out0 = in0 ^ in1 ^ in2 ^ in3 ^ temp;
+ ui64 out1 = (in0 & ~(in0 ^ in1 ^ in2 ^ in3)) | (temp & (in0 ^ in1 ^ in2
^ in3));
+ out1 <<= 1;
+ return <out0, out1>;
+}
+
+ui64 Sum(ui64 in[17]) {
+ ui64 level1[8];
+ for (uint i = 0; i < 4; i++) {
+ <level1[2 * i + 0], level1[2 * i + 1]> = Compress42(in[4 * i], in[4 *
i + 1], in[4 * i + 2], in[4 * i + 3]);
+ }
+ ui64 level2[4];
+ for (uint i = 0; i < 2; i++) {
+ <level2[2 * i + 0], level2[2 * i + 1]> = Compress42(level1[4 * i],
level1[4 * i + 1], level1[4 * i + 2], level1[4 * i + 3]);
+ }
+ ui64 level3[2];
+ <level3[0], level3[1]> = Compress42(level2[0], level2[1], level2[2],
level2[3]);
+ ui64 level4[2];
+ <level4[0], level4[1]> = Compress32(level3[0], level3[1], in[16]);
+ return level4[0] + level4[1];
+}
+
+ui64 Imul(ui32 s1, ui32 s2) {
+ ui3 bd[17] = Booth(s1);
+ ui33 pp[17] = PartialProducts(bd, s2);
+ ui64 tble[17] = Align(bd, pp);
+ ui64 prod = Sum(tble);
+ return prod;
+}
+
+<bool, ui64, ui64> ImulTest(ui32 s1, ui32 s2) {
+ ui64 spec_result = s1 * s2;
+ ui64 imul_result = Imul(s1, s2);
+ return <spec_result == imul_result, spec_result, imul_result>;
+}
+
=======================================
--- /dev/null
+++ /trunk/workshops/2014/russinoff-oleary/support/masc.h Thu May 22
13:28:24 2014 UTC
@@ -0,0 +1,36 @@
+#ifndef MASC_H
+#define MASC_H
+
+// ---------------------------------------------------------------------
+// Templates for passing & returning tuples and arrays
+
+template <class T1, class T2, class T3 = bool, class T4 = bool>
+class mv {
+ T1 first;
+ T2 second;
+ T3 third;
+ T4 fourth;
+ public:
+ mv(T1 x, T2 y) {first = x; second = y;}
+ mv(T1 x, T2 y, T3 z) {first = x; second = y; third = z;}
+ mv(T1 x, T2 y, T3 z, T4 w) {first = x; second = y; third = z; fourth =
w;}
+ void assign(T1 &x, T2 &y) {x = first; y = second;}
+ void assign(T1 &x, T2 &y, T3 &z) {x = first; y = second; z = third;}
+ void assign(T1 &x, T2 &y, T3 &z, T4 &w) {x = first; y = second; z =
third; w = fourth;}
+};
+
+template <uint m, class T>
+class array {
+ public:
+ T elt[m];
+};
+
+
+// Assert is sometimes a macro, which screws up our translation.
+// If we are using the MASC translator we want to prevent its expansion.
+#ifdef __MASC__
+#undef assert
+#endif
+
+#endif
+
=======================================
--- /dev/null
+++ /trunk/workshops/2014/russinoff-oleary/support/proof.lisp Thu May 22
13:28:24 2014 UTC
@@ -0,0 +1,534 @@
+(in-package "ACL2")
+
+(include-book "rtl/rel9/lib/top" :dir :system) ;; The basic RTL library
+
+(include-book "rtl/rel9/lib/mult" :dir :system) ;; The Booth
multiplication book
+
+(include-book "rtl/rel9/lib/gl" :dir :system) ;; Connect lib with gl
+
+(include-book "arithmetic-5/top" :dir :system) ;; It's hard to do any
arithmetic without this
+
+(include-book "imul") ;; The IMUL model
+
+
+;;***********************************************************************************
+;; Utility functions
+;;***********************************************************************************
+
+;; a[m], ..., a[n-1] are all 64-bit vectors:
+
+(defun all-bvecp (a m n)
+ (declare (xargs :measure (nfix (- n m))))
+ (if (and (natp m) (natp n) (< m n))
+ (and (bvecp (ag m a) 64)
+ (all-bvecp a (1+ m) n))
+ t))
+
+(defthm all-bvecp-integerp
+ (implies (and (all-bvecp a m n)
+ (natp n)
+ (natp m)
+ (natp k)
+ (<= m k)
+ (< k n))
+ (integerp (ag k a)))
+ :rule-classes (:rewrite :type-prescription))
+
+(defthm all-bvecp-bvecp
+ (implies (and (all-bvecp a m n)
+ (natp n)
+ (natp m)
+ (natp k)
+ (<= m k)
+ (< k n))
+ (bvecp (ag k a) 64))
+ :rule-classes (:rewrite :type-prescription))
+
+(defthm all-bvecp-leq
+ (implies (and (all-bvecp a m p)
+ (natp m)
+ (natp n)
+ (natp p)
+ (<= m n)
+ (<= n p))
+ (all-bvecp a m n)))
+
+(defthm all-bvecp-subrange
+ (implies (and (all-bvecp a q p)
+ (natp m)
+ (natp n)
+ (natp p)
+ (natp q)
+ (<= q m)
+ (<= m n)
+ (<= n p))
+ (all-bvecp a m n)))
+
+;; (a[0] + ... + a[k-1])[63:0]:
+
+(defun sum-simple (a k)
+ (if (zp k)
+ 0
+ (bits (+ (ag (1- k) a) (sum-simple a (1- k)))
+ 63 0)))
+
+(defthm bvecp-sum-simple
+ (bvecp (sum-simple a n) 64)
+ :rule-classes (:rewrite :type-prescription))
+
+;; a[m] + .. + a[n]:
+
+(defun sum-range (a m n)
+ (if (or (zp n) (<= n m))
+ 0
+ (+ (ag (1- n) a) (sum-range a m (1- n)))))
+
+(defthm integerp-sum-range
+ (implies (and (all-bvecp a m n)
+ (natp m)
+ (natp n)
+ (<= m n))
+ (integerp (sum-range a m n)))
+ :rule-classes (:rewrite :type-prescription)
+ :hints (("Goal" :induct (nats n))))
+
+(defthmd sum-range-sum-simple
+ (implies (and (natp n)
+ (all-bvecp a 0 n))
+ (equal (bits (sum-range a 0 n) 63 0)
+ (sum-simple a n)))
+ :hints (("Goal" :in-theory (enable sum-range sum-simple))
+ ("Subgoal *1/5" :in-theory (enable sum-range sum-simple)
+ :use ((:instance bits-bits-sum
+ (x (sum-range a 0 (+ -1 n)))
+ (y (ag (+ -1 n) a))
+ (k 63)
+ (i 63)
+ (j 0))))))
+
+;; Sums of sums of adjacent ranges:
+
+(defthm sum-ranges
+ (implies (and (natp m)
+ (natp n)
+ (natp k)
+ (<= m k)
+ (<= k n)
+ (all-bvecp a m n))
+ (equal (+ (sum-range a m k) (sum-range a k n))
+ (sum-range a m n)))
+ :rule-classes ()
+ :hints (("Goal" :induct (nats n))))
+
+;; This lemma is critical in the analysis of the compression tree:
+
+(defthmd sum-range-split
+ (implies (and (all-bvecp a m n)
+ (natp m)
+ (natp n)
+ (< m n)
+ (evenp (+ m n)))
+ (equal (bits (sum-range a m n) 63 0)
+ (bits (+ (bits (sum-range a m (/ (+ m n) 2)) 63 0)
+ (bits (sum-range a (/ (+ m n) 2) n) 63 0))
+ 63 0)))
+ :hints (("Goal" :use ((:instance sum-ranges (k (/ (+ m n) 2)))))))
+
+
+;;***********************************************************************************
+;; Booth
+;;***********************************************************************************
+
+;; The function Booth computes an array of 3-bit encodings of the
+;; Booth digits (theta k y), 0 <= k < 17:
+
+(def-gl-thm encode-lemma
+ :hyp (and (bvecp y 32)
+ (natp k)
+ (< k 17))
+ :concl (equal (encode (bits (* 2 y) (+ 2 (* 2 k)) (* 2 k)))
+ (cat (neg (theta k y)) 1 (abs (theta k y)) 2))
+ :g-bindings (gl::auto-bindings (:nat k 5) (:nat y 32)))
+
+(in-theory (disable encode))
+
+(defthm booth-recursion-1
+ (implies (and (natp k)
+ (natp j)
+ (< j k))
+ (equal (ag j (booth-loop-0 k y35 a))
+ (ag j a))))
+
+(defthm booth-recursion-2
+ (implies (and (natp y)
+ (natp k)
+ (natp j)
+ (<= k j)
+ (< j 17))
+ (equal (ag j (booth-loop-0 k y35 a))
+ (encode (bits y35 (+ (* 2 j) 2) (* 2 j)))))
+ :hints (("Subgoal *1/3" :expand (:free (k) (booth-loop-0 k y35 a)))))
+
+(defthm booth-lemma
+ (implies (and (bvecp y 32)
+ (natp k)
+ (< k 17))
+ (equal (ag k (booth y))
+ (cat (neg (theta k y)) 1 (abs (theta k y)) 2))))
+
+(in-theory (disable booth))
+
+
+;;***********************************************************************************
+;; PartialProducts
+;;***********************************************************************************
+
+;; The function PartialProducts computes an array of the partial
+;; products (bmux4 (theta k y) x 33), 0 <= k < 17:
+
+(defthm partialproducts-recursion-1
+ (implies (and (natp j)
+ (natp k)
+ (< j k))
+ (equal (ag j (partialproducts-loop-0 k x m21 pp))
+ (ag j pp))))
+
+(defthm partialproducts-recursion-2
+ (implies (and (natp k)
+ (natp j)
+ (<= k j)
+ (< j 17))
+ (equal (ag j (partialproducts-loop-0 k x m21 pp))
+ (let ((row (case (bits (ag j m21) 1 0)
+ (2 (bits (ash x 1) 32 0))
+ (1 x)
+ (t 0))))
+ (bits (if1 (bitn (ag j m21) 2)
+ (lognot row)
+ row)
+ 32 0))))
+ :hints (("subgoal *1/1" :expand
+ ((:free (pp) (partialproducts-loop-0 k x m21 pp))
+ (:free (pp) (partialproducts-loop-0 0 x m21
pp))))))
+
+(def-gl-thm partialproducts-lemma
+ :hyp (and (bvecp x 32)
+ (bvecp y 32)
+ (natp k)
+ (< k 17))
+ :concl (equal (ag k (partialproducts (booth y) x))
+ (bmux4 (theta k y) x 33))
+ :g-bindings (gl::auto-bindings (:nat k 5) (:nat x 32) (:nat y 32)))
+
+(in-theory (disable partialproducts theta bmux4))
+
+
+;;***********************************************************************************
+;; Align
+;;***********************************************************************************
+
+;; The function Align computes an array of the aligned partial products
+;; (bits (pp4p-theta k x y 33) 63 0):
+
+(defthm sign-bits-recursion-1
+ (implies (and (natp j)
+ (natp k)
+ (< j k))
+ (mv-let (sb psb) (align-loop-1 k bds sb0 psb0)
+ (declare (ignore psb))
+ (equal (ag j sb)
+ (ag j sb0)))))
+
+(defthm sign-bits-recursion-2
+ (implies (and (natp j)
+ (natp k)
+ (<= j k))
+ (mv-let (sb psb) (align-loop-1 k bds sb0 psb0)
+ (declare (ignore sb))
+ (equal (ag j psb)
+ (ag j psb0)))))
+
+(defthm sign-bits-recursion-3
+ (implies (and (natp x)
+ (natp k)
+ (natp j)
+ (<= k j)
+ (< j 17))
+ (mv-let (sb psb) (align-loop-1 k bds sb0 psb0)
+ (and (equal (ag j sb)
+ (bitn (ag j bds) 2))
+ (equal (ag (1+ j) psb)
+ (bitn (ag j bds) 2)))))
+ :hints (("Subgoal *1/3" :expand
+ ((:free (j bds sb psb) (align-loop-1 j bds sb
psb))))))
+
+(defthm sign-bits-lemma
+ (implies (and (bvecp y 32)
+ (natp k)
+ (< k 17))
+ (mv-let (sb psb) (align-loop-1 0 (booth y) () ())
+ (and (equal (ag k sb)
+ (neg (theta k y)))
+ (equal (ag (1+ k) psb)
+ (neg (theta k y)))))))
+
+(defthm align-recursion-1
+ (implies (and (natp j)
+ (natp k)
+ (< j k))
+ (let ((tble (align-loop-0 k pp psb sb tble0)))
+ (equal (ag j tble)
+ (ag j tble0)))))
+
+(defthm align-recursion-2
+ (implies (and (natp k)
+ (natp j)
+ (<= k j)
+ (< j 17))
+ (equal (ag j (align-loop-0 k pp psb sb tble0))
+ (if (zp j)
+ (bits (setbitn (setbitn (setbitn (setbits 0 67 (+ (*
2 j) 32) (* 2 j) (ag j pp))
+ 67 33 (ag j sb))
+ 67 34 (ag j sb))
+ 67 35 (lognot1 (ag j sb)))
+ 63 0)
+ (bits (setbitn (setbitn (setbitn (setbits 0 67 (+ (* 2
j) 32) (* 2 j) (ag j pp))
+ 67 (- (* 2 j) 2) (ag
j psb))
+ 67 (+ (* 2 j) 33) (lognot1 (ag
j sb)))
+ 67 (+ (* 2 j) 34) 1)
+ 63 0))))
+ :hints (("subgoal *1/1" :expand ((:free (j bds sb psb) (align-loop-0 j
pp psb sb tble0))))))
+
+(def-gl-thm align-lemma
+ :hyp (and (bvecp x 32)
+ (bvecp y 32)
+ (natp k)
+ (< k 17))
+ :concl (equal (ag k (align (booth y) (partialproducts (booth y) x)))
+ (bits (pp4p-theta k x y 33) 63 0))
+ :g-bindings (gl::auto-bindings (:nat k 5) (:nat x 32) (:nat y 32)))
+
+(defthm bvecp-align
+ (implies (and (bvecp x 32)
+ (bvecp y 32)
+ (natp k)
+ (< k 17))
+ (bvecp (ag k (align (booth y) (partialproducts (booth y) x)))
64))
+ :rule-classes (:rewrite :type-prescription))
+
+(defthm all-bvecp-align
+ (implies (and (bvecp x 32)
+ (bvecp y 32)
+ (natp m))
+ (all-bvecp (align (booth y) (partialproducts (booth y) x)) m
17)))
+
+(in-theory (disable align bmux4 neg pp4-theta pp4p-theta))
+
+(defthm sum-simple-pp4p-theta
+ (implies (and (bvecp x 32)
+ (bvecp y 32)
+ (natp k)
+ (<= k 17))
+ (equal (sum-simple (align (booth y) (partialproducts (booth y)
x)) k)
+ (bits (sum-pp4p-theta x y k 33) 63 0))))
+
+;; The following is a consequence of booth4-corollary-2:
+
+(defthm sum-simple-align-prod
+ (implies (and (bvecp x 32) (bvecp y 32))
+ (equal (sum-simple (align (booth y) (partialproducts (booth y)
x)) 17)
+ (* x y)))
+ :hints (("Goal" :in-theory (e/d (bvecp-monotone) (bits-bits))
+ :use ((:instance bvecp-product (m 32) (n 32))
+ (:instance bits-bits (x (sum-pp4p-theta x y 17 33))
+ (i 66) (j 0) (k 63) (l 0))
+ (:instance booth4-corollary-2 (n 33) (m 17))))))
+
+
+;;***********************************************************************************
+;; Sum
+;;***********************************************************************************
+
+;; The function Sum computes the sum of the aligned partial products by
means of a
+;; 17:2 compression tree and a final 64-bit adder.
+
+;; The compression tree consists of 7 4:2 compressors and 1 3:2
compressor. The
+;; functionality of these components is proved automatically by gl:
+
+(def-gl-thm compress32-lemma
+ :hyp (and (bvecp in0 64)
+ (bvecp in1 64)
+ (bvecp in2 64))
+ :concl (mv-let (out0 out1)
+ (compress32 in0 in1 in2)
+ (and (bvecp out0 64)
+ (bvecp out1 64)
+ (equal (bits (+ in0 in1 in2) 63 0)
+ (bits (+ out0 out1) 63 0))))
+ :g-bindings (gl::auto-bindings (:mix (:nat in0 64)
+ (:nat in1 64)
+ (:nat in2 64))))
+
+(def-gl-thm compress42-lemma
+ :hyp (and (bvecp in0 64)
+ (bvecp in1 64)
+ (bvecp in2 64)
+ (bvecp in3 64))
+ :concl (mv-let (out0 out1)
+ (compress42 in0 in1 in2 in3)
+ (and (bvecp out0 64)
+ (bvecp out1 64)
+ (equal (bits (+ in0 in1 in2 in3) 63 0)
+ (bits (+ out0 out1) 63 0))))
+ :g-bindings (gl::auto-bindings (:mix (:nat in0 64)
+ (:nat in1 64)
+ (:nat in2 64)
+ (:nat in3 64))))
+
+(in-theory (disable compress32 compress42))
+
+;; The compression is performed in 4 stages.
+
+;; Level 1 compresses the first 16 entries to 8 vectors using 4 4:2
compressors:
+
+(defun level1 (in)
+ (sum-loop-1 0 in ()))
+
+;; Level 2 compresses the output of level 1 to 4 vectors using 2 4:2
compressors:
+
+(defun level2 (a1)
+ (sum-loop-0 0 a1 ()))
+
+;; Level 3 compresses the output of level 2 to 2 vectors using a 4:2
compressor:
+
+(defun level3 (a2)
+ (mv-let (temp-0 temp-1)
+ (compress42 (ag 0 a2) (ag 1 a2) (ag 2 a2) (ag 3 a2))
+ (as 1 temp-1 (as 0 temp-0 a2))))
+
+;; Level 3 combines the output of level 3 and the last array entry with a
3:2 compressor:
+
+(defun level4 (a3 in)
+ (mv-let (temp-0 temp-1)
+ (compress32 (ag 0 a3) (ag 1 a3) (ag 16 in))
+ (as 1 temp-1 (as 0 temp-0 ()))))
+
+;; The adder is applied to the output of the level 4:
+
+(defthm sum-rewrite
+ (equal (sum in)
+ (let ((comp (level4 (level3 (level2 (level1 in))) in)))
+ (bits (+ (ag 0 comp) (ag 1 comp)) 63 0))))
+
+(in-theory (disable sum))
+
+;; For each level, through repeated applications of the lemma
bits-sum-range,
+;; we show that the sum of the outputs is the sum of the inputs (mod
2^(64)).
+;; For each of the first 3 levels, we must also show that the outputs are
all
+;; 64-bit vectors in order to apply bits-sum-range to the next level.
+
+
+(defthm level1-all-bvecp
+ (implies (all-bvecp in 0 17)
+ (all-bvecp (level1 in) 0 8))
+ :rule-classes (:forward-chaining)
+ :hints (("Goal" :expand ((:free (k a1) (sum-loop-1 k in a1))))))
+
+(defthm level1-4-2
+ (implies (and (all-bvecp in 0 17) (member i '(0 4 8 12) ) (= j (+ 4 i)))
+ (equal (bits (sum-range in i j) 63 0)
+ (bits (sum-range (level1 in) (/ i 2) (/ j 2)) 63 0)))
+ :hints (("Goal" :expand ((:free (k a1) (sum-loop-1 k in a1))))))
+
+(in-theory (disable level1))
+
+(defthm level1-sum
+ (implies (all-bvecp in 0 17)
+ (equal (bits (sum-range in 0 16) 63 0)
+ (bits (sum-range (level1 in) 0 8) 63 0)))
+ :hints (("Goal" :in-theory (enable sum-range-split))))
+
+(defthm level2-all-bvecp
+ (implies (all-bvecp a1 0 8)
+ (all-bvecp (level2 a1) 0 4))
+ :rule-classes (:forward-chaining)
+ :hints (("Goal" :expand ((:free (k a2) (sum-loop-0 k a1 a2))))))
+
+(defthm a2-4-2
+ (implies (and (all-bvecp a1 0 8) (member i '(0 4)) (= j (+ 4 i)))
+ (equal (bits (sum-range a1 i j) 63 0)
+ (bits (sum-range (level2 a1) (/ i 2) (/ j 2)) 63 0)))
+ :hints (("Goal" :expand ((:free (k a2) (sum-loop-0 k a1 a2))
+ (:free (a m n) (sum-range a m n))))))
+
+(in-theory (disable level2))
+
+(defthm level2-sum
+ (implies (all-bvecp a1 0 8)
+ (equal (bits (sum-range a1 0 8) 63 0)
+ (bits (sum-range (level2 a1) 0 4) 63 0)))
+ :hints (("Goal" :in-theory (enable sum-range-split))))
+
+(defthm level3-all-bvecp
+ (implies (all-bvecp a2 0 4)
+ (all-bvecp (level3 a2) 0 2))
+ :rule-classes (:forward-chaining)
+ :hints (("Goal" :expand ((:free (a m n) (all-bvecp a m n))))))
+
+(defthm level3-sum
+ (implies (all-bvecp a2 0 4)
+ (equal (bits (sum-range a2 0 4) 63 0)
+ (bits (sum-range (level3 a2) 0 2) 63 0)))
+ :hints (("Goal" :expand ((:free (a m n) (sum-range a m n))))))
+
+(in-theory (disable level3))
+
+(defthm level4-sum
+ (implies (and (bvecp (ag 16 in) 64)
+ (all-bvecp a3 0 2))
+ (equal (bits (+ (ag 16 in) (sum-range a3 0 2)) 63 0)
+ (bits (+ (ag 0 (level4 a3 in))
+ (ag 1 (level4 a3 in)))
+ 63 0)))
+ :hints (("Goal" :expand ((:free (a m n) (sum-range a m n))))))
+
+(in-theory (disable level4))
+
+;; Combine the preceding results:
+
+(defthm sum-sum-range
+ (implies (all-bvecp in 0 17)
+ (equal (sum in)
+ (bits (sum-range in 0 17) 63 0)))
+ :hints (("Goal" :in-theory (disable bits-bits-sum)
+ :use ((:instance bits-bits-sum
+ (x (sum-range (level3 (level2 (level1
in))) 0 2))
+ (y (ag 16 in))
+ (i 63) (j 0) (k 63))
+ (:instance bits-bits-sum
+ (x (sum-range in 0 16))
+ (y (ag 16 in))
+ (i 63) (j 0) (k 63))))))
+
+(in-theory (disable sum-rewrite))
+
+;; Combine the lemmas sum-sum-range and sum-range-sum-simple:
+
+(in-theory (enable sum-range-sum-simple))
+
+(defthm sum-sum-simple
+ (implies (all-bvecp in 0 17)
+ (equal (sum in)
+ (sum-simple in 17))))
+
+;;***********************************************************************************
+;; Final Theorem
+;;***********************************************************************************
+
+;; The main result follows from sum-sum-simple sum-simple-align-prod:
+
+(defthm imul-thm
+ (implies (and (bvecp s1 32)
+ (bvecp s2 32))
+ (equal (imul s1 s2)
+ (* s1 s2))))
=======================================
--- /dev/null
+++ /trunk/workshops/2014/russinoff-oleary/support/translate.lisp Thu May
22 13:28:24 2014 UTC
@@ -0,0 +1,507 @@
+(in-package "ACL2")
+
+(include-book "misc/file-io" :dir :system)
+
+(program)
+
+#|
+The translation of a MASC model to ACL2 is performed in two phases:
+
+(1) The MASC parser generates a file containing an S-expression
representation of
+each global constant and each function of the model.
+
+(2) The ACL2 program contained in this file converts these S-expressions
into ACL2
+functions.
+
+The S-expression for a constant declaration is (DECLARE var term). This
is converted
+to an ACL2 function as follows:
+|#
+
+(defun translate-global-constant (dec)
+ `(defun ,(cadr dec) () ,(caddr dec)))
+
+#|
+The S-expression generated by the parser for a MASC function has the form
+
+ (defunc fname (arg1 ... argk) body)
+
+where fname is the name of the function, arg1,...,argk are its formal
parameters,
+and body is a list of S-expressions corresponding to its body, which is
assumed to be
+a statement block. The parser generates an S-expression for each
statement as follows:
+
+* Block: (BLOCK stmt1 ... stmtk)
+
+* Assignment: (ASSIGN var term)
+
+* Multiple assignment: (MV-ASSIGN (var1 ... vark) fncall)
+
+* Variable or constant declaration: (DECLARE var term) or (ARRAY var
term-list)
+
+* Multiple variable or constant declaration: (LIST . decs), where decs is
a list of
+ variable or constant declarations
+
+* Conditional branch: (IF term left right), where left is a block and
right is either
+ a block or NIL
+
+* Return: (RETURN term)
+
+* For loop: (FOR (init test update) body), where
+
+ (1) init is either (DECLARE var val) or (ASSIGN var val)
+
+ (2) test is either (op var limit) or (logand1 (op var limit) term),
where op is log<,
+ log<=, log>, or log>=, and var is the same variable that appears in
init
+
+ (3) update is a term, the value of which is assigned to var before each
iteration
+ after the first
+
+ (4) body is a statement block
+
+* Switch statement: (SWITCH test (lab1 . stmts1) ... (labk . stmtsk)),
where each
+ labi is either an integer or a list of integers and each stmtsi is a
list of statements.
+
+* Assertion: (ASSERT fn term), where fn is the name of the function in
which the assertion
+ occurs and term is a term that is expected to evaluate to true.
+
+A return statement may occur only in the final statement of a function
body. More
+precisely, we assume that every function body is admissible, where a
statement block is
+is said to be an admissible function body if (a) no return statement
occurs in any
+statement of the block other than the final one and (b) the final
statement is either
+a return statement or an if statement with non-trivial right branch such
that both
+branches are admissible function bodies.
+
+The overall strategy in the translation of a MASC function to ACL2 is to
construct a nest
+of LET, LET*, and MV-LET terms. Each statement in the function body
except the last
+corresponds to one or more variables that are bound in this nest. For
each of these
+statements, the translator generates a triple (ins outs term), which we
shall call a binding,
+with the following components:
+
+ (1) ins: a list of the variables whose previous values are read by the
statement.
+
+ (2) outs: a list of the variables that are written by the statement;
+
+ (3) term: evaluation of this expression returns a multiple value
consisting of the
+ updated values of the variables of outs, or a single value if outs
is a singleton.
+
+The bindings of the nest are derived from these triples. The body of the
nest is
+generated from the final statement of the function body.
+
+Assertions are handled specially because they are statements that do not
affect any
+program variables. An assertion (ASSERT fn term) results in a binding of
the dummy variable
+ASSERT to the value (IN-FUNCTION fn term), where IN-FUNCTION is a macro
that throws an
+error if term is false, with a message indicating the function in which
the error occurred.
+
+In addition to the top-level ACL2 function corrrsponding to a MASC
function, a separate
+recursive function is generated for each for loop. Its returned values
are the variables
+that are assigned values within the loop. Its arguments include these
variables, along
+with any variables that are required in the execution of the loop, as well
as any variables
+that occur in the loop initialization or test. This function is
constructed in a manner
+similar to that of the top-level function, but the final statement of the
body is not
+treated specially. Instead, the body of the nest of bindings is a
recursive call in which
+the loop variable is replaced by its updated value. The resulting term
becomes the left
+branch of an IF expression, of which the right branch is simply the
returned variable
+(if there is only one) or a multiple value consisting of the returned
variables (if there
+are more than one). The test of the IF is simply the test of the loop.
+|#
+
+;; In the S-expression for an array declaration, the initial value (if
provided) is
+;; represented as a simple list of constant values. For a local
declaration, this is
+;;converted to an ACL2 array as follows:
+
+(defun array-init (l n)
+ (if (consp l)
+ (if (eql (car l) 0)
+ (array-init (cdr l) (1+ n))
+ (cons (cons n (car l)) (array-init (cdr l) (1+ n))))
+ ()))
+
+;; get-vars returns a list of the variables that occur in an expression:
+
+(mutual-recursion
+
+(defun get-vars (expr)
+ (if (consp expr)
+ (if (fquotep expr)
+ ()
+ (get-vars-list (cdr expr)))
+ (if (and expr (symbolp expr))
+ (list expr)
+ ())))
+
+(defun get-vars-list (exprs)
+ (if (consp exprs)
+ (union-eq (get-vars (car exprs)) (get-vars-list (cdr exprs)))
+ ()))
+
+)
+
+;; The following functions are used in conjuction with the built-in
subst-var,
+;; which substitutes a term for each occurrence of a variable in an
expression.
+
+;; var-count counts the number of occurrences of a variable in an
expression:
+
+(mutual-recursion
+
+(defun var-count (var expr)
+ (if (consp expr)
+ (if (fquotep expr)
+ 0
+ (var-count-list var (cdr expr)))
+ (if (eql var expr)
+ 1
+ 0)))
+
+(defun var-count-list (var exprs)
+ (if (consp exprs)
+ (+ (var-count var (car exprs)) (var-count-list var (cdr exprs)))
+ 0))
+
+)
+
+;; get-ins returns a list of the variables that are required by a list of
bindings:
+
+(defun get-ins (binds)
+ (if (consp binds)
+ (union-eq (caar binds)
+ (set-difference-eq (get-ins (cdr binds))
+ (cadar binds)))
+ ()))
+
+;; get-locals returns a list of the local variables that are declared in a
+;; list of statements:
+
+(defun get-locals (stmts)
+ (if stmts
+ (if (eq (caar stmts) 'declare)
+ (cons (cadar stmts) (get-locals (cdr stmts)))
+ (if (eq (caar stmts) 'list)
+ (get-locals (append (cdar stmts) (cdr stmts)))
+ (get-locals (cdr stmts))))
+ ()))
+
+;; get-outs returns a list of the non-local variables that are written by
+;; a sequence of bindings. Since ASSERT is a dummy variable, it is not
included
+;; unless it is the only variable in the list:
+
+(defun get-bound-vars (binds)
+ (if (consp binds)
+ (union-eq (cadar binds) (get-bound-vars (cdr binds)))
+ ()))
+
+(defun get-outs (binds locals)
+ (remove 'assert (set-difference-eq (get-bound-vars binds) locals)))
+
+; bind-vars converts a list of bindings and a body to a nested
LET/LET*/MV-LET-term:
+
+(defun used-in-binds-p (var binds)
+ (if binds
+ (or (member var (caar binds))
+ (member var (cadar binds))
+ (used-in-binds-p var (cdr binds)))
+ ()))
+
+;;As an optimization, when possible, the final element of a list of binds
is eliminated
+;; by replacing its out with its term in body:
+
+(defun reduce-single-binds (binds body)
+ (if (consp binds)
+ (let* ((bind (car (last binds)))
+ (out (caadr bind))
+ (term (caddr bind)))
+ (if (or (eql body out)
+ (and (consp body) (eql (car body) 'mv) (eql (var-count out
body) 1)))
+ (reduce-single-binds (butlast binds 1) (subst-var term out
body))
+ (mv binds body)))
+ (mv () body)))
+
+;; The first argument of let-or-let* is a list of binds each of which has
the
+;; property that its outs list is a singleton. In every non-recursive call,
+;; result and let*p are NIL. It converts binds into result, which is
suitable
+;; as a first argument of let or let*.
+
+(defun let-or-let* (binds body result let*p)
+ (if binds
+ (let* ((bind (car binds))
+ (out (caadr bind))
+ (term (caddr bind)))
+ (let-or-let* (cdr binds)
+ body
+ (append result (list (list out term)))
+ (or let*p (used-in-binds-p out (cdr binds)))))
+ (if result
+ (list (if let*p 'let* 'let) result body)
+ body)))
+
+
+(mutual-recursion
+
+(defun bind-vars (binds body)
+ (if binds
+ (let ((outs (cadar binds))
+ (term (caddar binds)))
+ (if (cdr outs)
+ (if (and (null (cdr binds)) (equal body `(mv ,@outs)))
+ term
+ `(mv-let ,outs ,term ,(bind-vars (cdr binds) body)))
+ (bind-single-vars (list (car binds)) (cdr binds) body)))
+ body))
+
+(defun bind-single-vars (sbinds binds body)
+ (if binds
+ (let ((outs (cadar binds))
+ (term (caddar binds)))
+ (if (cdr outs)
+ (bind-single-vars sbinds () (bind-vars binds body))
+ (if (and (null (cdr binds)) (equal body (car outs)))
+ (bind-single-vars sbinds () term)
+ (bind-single-vars (append sbinds (list (car binds)))
+ (cdr binds)
+ body))))
+ (mv-let (sbinds body) (reduce-single-binds sbinds body)
+ (let-or-let* sbinds body () ()))))
+
+)
+
+;; The following converts a boolean expression to a term that fails with a
value of NIL
+;; rather than 0:
+
+(defun lispify-boolean (test)
+ (case (car test)
+ (logand1 `(and ,(lispify-boolean (cadr test)) ,(lispify-boolean (caddr
test))))
+ (logior1 `(or ,(lispify-boolean (cadr test)) ,(lispify-boolean (caddr
test))))
+ (lognot1 `(not ,(lispify-boolean (cadr test))))
+ (log= `(eql ,@(cdr test)))
+ (log<> `(not (eql ,@(cdr test))))
+ (log< `(< ,@(cdr test)))
+ (log<= `(<= ,@(cdr test)))
+ (log> `(> ,@(cdr test)))
+ (log>= `(>= ,@(cdr test)))
+ ((true$ false$) test)
+ (otherwise `(not (eql ,test 0)))))
+
+;; The name of a recursive for-loop function is egnerated by
make-loop-name:
+
+(defun make-loop-name (fname n)
+ (intern (string-append (string-append (string fname) "-LOOP-")
+ (coerce (explode-atom n 10) 'string))
+ "ACL2"))
+
+;; Extract the comparator and limit from a loop test:
+
+(defun loop-op (test)
+ (if (eql (car test) 'and)
+ (loop-op (cadr test))
+ (car test)))
+
+(defun loop-limit (test)
+ (if (eql (car test) 'and)
+ (loop-limit (cadr test))
+ (caddr test)))
+
+;; A measure is required for a loop function, depending on the op of the
test:
+
+(defun loop-decl (op var limit)
+ (case op
+ (< `(declare (xargs :measure (nfix (- ,limit ,var)))))
+ (<= `(declare (xargs :measure (nfix (- (1+ ,limit) ,var)))))
+ (> `(declare (xargs :measure (nfix (- ,var ,limit)))))
+ (>= `(declare (xargs :measure (nfix (- ,var (1- ,limit))))))))
+
+;; The test of the IF of a loop function says that everything is an
integer and the
+;; test of the for loop holds:
+
+(defun loop-integerp-test (vars)
+ (if (consp vars)
+ (cons (list 'integerp (car vars))
+ (loop-integerp-test (cdr vars)))
+ ()))
+
+(defun loop-test (init test)
+ `(and ,@(loop-integerp-test (union-eq (get-vars init) (get-vars
test))) ,test))
+
+;; Each of the main functions that generate ACL2 representations of
statements or lists of
+;; statements takes two additional arguments, which are used in the naming
of any auxiliary
+;; functions (corresponding to embedded for loops): fname is the name of
the top-level function,
+;; and loops is the number of auxiliary functions that have been created
for that function so
+;; far. Among the values returned by each of these functions is defs, a
list of definitions of
+;; the auxiliary functions that are created during its execution.
+
+(mutual-recursion
+
+;; This function is applied to each statement of a top-level function
except the last, and each
+;; statement in the body of a for loop, and produces a binding.
+
+(defun translate-statement (stmt fname loops)
+ (case (car stmt)
+ ((assign declare)
+ (let* ((out (cadr stmt))
+ (expr (caddr stmt))
+ (ins (get-vars expr)))
+ (mv ins (list out) expr ())))
+ (mv-assign
+ (let* ((outs (cadr stmt))
+ (expr (caddr stmt))
+ (ins (get-vars expr)))
+ (mv ins outs expr ())))
+ (assert
+ (let* ((outs (list 'assert))
+ (expr (cadr stmt))
+ (fn (caddr stmt))
+ (ins (get-vars expr)))
+ (mv ins outs `(in-function ,fn ,(lispify-boolean expr)) ())))
+ (block
+ (mv-let (binds defs) (translate-list (cdr stmt) fname loops)
+ (let* ((ins (get-ins binds))
+ (outs (get-outs binds (get-locals (cdr stmt))))
+ (val (if (cdr outs) `(mv ,@outs) (if outs (car outs) ())))
+ (term (bind-vars binds val)))
+ (mv ins outs term defs))))
+ (if
+ (let ((test (cadr stmt))
+ (left (caddr stmt))
+ (right (cadddr stmt)))
+ (mv-let (rbinds rdefs) (translate-list (cdr right) fname loops)
+ (mv-let (lbinds ldefs)
+ (translate-list (cdr left) fname (+ loops (length
rdefs)))
+ (let* ((ins (union-eq (get-vars test) (union-eq (get-ins
rbinds) (get-ins lbinds))))
+ (outs (union-eq (get-outs rbinds (get-locals (cdr
right)))
+ (get-outs lbinds (get-locals (cdr
left)))))
+ (val (if (cdr outs) `(mv ,@outs) (if outs (car outs)
())))
+ (term `(if1 ,test ,(bind-vars lbinds val) ,(bind-vars
rbinds val))))
+ (mv ins outs term (append rdefs ldefs)))))))
+ (switch
+ (let ((test (cadr stmt))
+ (cases (cddr stmt)))
+ (mv-let (ins outs labels binds defs) (switch-first-pass cases
fname loops)
+ (mv (union-eq (get-vars test) ins)
+ outs
+ (let ((val (if (cdr outs) `(mv ,@outs) (if outs (car outs)
()))))
+ `(case ,test ,@(switch-second-pass labels binds val)))
+ defs))))
+ (for
+ (let* ((info (cadr stmt))
+ (init (car info))
+ (localp (eq (car init) 'declare))
+ (var (cadr init))
+ (initval (caddr init))
+ (test (lispify-boolean (cadr info)))
+ (op (loop-op test))
+ (limit (loop-limit test))
+ (update (caddr info))
+ (body (caddr stmt)))
+ (mv-let (binds defs) (translate-list (cdr body) fname loops)
+ (let* ((fname (make-loop-name fname (+ loops (length defs))))
+ (decl (loop-decl op var limit))
+ (test (loop-test initval test))
+ (ins (remove var (union-eq (union-eq (get-vars initval)
(get-vars test)) (get-ins binds))))
+ (outs (union-eq (if localp () (list var)) (get-outs binds
(get-locals (cdr body)))))
+ (params (remove var (union-eq ins outs)))
+ (left (bind-vars binds `(,fname ,update ,@params)))
+ (right (if (cdr outs) `(mv ,@outs) (car outs)))
+ (def `(defun ,fname (,var ,@params) ,decl
(if ,test ,left ,right))))
+ (mv ins outs `(,fname ,initval ,@params) (append defs (list
def)))))))
+ (otherwise
+ (mv () () () ()))))
+
+;; Translation of a switch statement is performed in two passes:
+
+(defun switch-first-pass (cases fname loops)
+ (if (consp cases)
+ (mv-let (ins outs labels binds defs) (switch-first-pass (cdr cases)
fname loops)
+ (mv-let (binds1 defs1) (translate-list (cdar cases) fname (+ loops
(length defs)))
+ (mv (union-eq ins (get-ins binds1))
+ (union-eq outs (get-outs binds1 (get-locals (cdar cases))))
+ (cons (caar cases) labels)
+ (cons binds1 binds)
+ (append defs1 defs))))
+ (mv () () () () ())))
+
+(defun switch-second-pass (labels binds val)
+ (if (consp labels)
+ (cons (list (car labels) (bind-vars (car binds) val))
+ (switch-second-pass (cdr labels) (cdr binds) val))
+ ()))
+
+;; This function calls translate-statement on each statement in a list.
For each of these
+;; calls, it forms the list (ins out term). It returns a list of these
triples.
+
+(defun translate-list (stmts fname loops)
+ (if (consp stmts)
+ (if (or (eq (caar stmts) 'list)
+ (and (eq (caar stmts) 'block)
+ (null (get-locals (cdar stmts)))))
+ (translate-list (append (cdar stmts) (cdr stmts)) fname loops)
+ (mv-let (binds defs1) (translate-list (cdr stmts) fname loops)
+ (mv-let (ins outs term defs2)
+ (translate-statement (car stmts) fname (+ loops (length
defs1)))
+ (if outs
+ (mv (cons (list ins outs term) binds)
+ (append defs1 defs2))
+ (mv binds defs1)))))
+ (mv () ())))
+
+)
+
+(mutual-recursion
+
+;; This function translates the statements forming the body of a top-level
function
+;; order, calling translate-final-statement on the final statement and
translate-list on
+;; the others. It then calls bind-vars to convert the resulting term and
bindings into
+;; a LET/LET*/MV-LET nest. The same function is also called on each
branch of any IF
+;; statement that is encountered during the execution of
translate-final-statement.
+
+(defun translate-function-block (stmts fname loops)
+ (if (consp stmts)
+ (mv-let (term defs1) (translate-final-statement (car (last stmts))
fname loops)
+ (mv-let (binds defs2) (translate-list (butlast stmts 1) fname (+
loops (length defs1)))
+ (mv (bind-vars binds term) (append defs1 defs2))))
+ (mv () ())))
+
+;; The final statement in the body of a top-level function is handled
specially by this
+;; function. It returns a term, the evaluation of which corresponds to
execution of
+;; the statement, preserving the if-structure of the statement.
+
+(defun translate-final-statement (stmt fname loops)
+ (case (car stmt)
+ (return
+ (mv (cadr stmt) ()))
+ (if
+ (let ((test (cadr stmt))
+ (left (caddr stmt))
+ (right (cadddr stmt)))
+ (mv-let (lterm ldefs) (translate-function-block left fname loops)
+ (mv-let (rterm rdefs) (translate-function-block right fname (+
loops (length ldefs)))
+ (mv `(if1 ,test ,lterm ,rterm) (append ldefs rdefs))))))
+ (otherwise
+ (mv () ()))))
+
+)
+
+(defun translate-function (f)
+ (let ((fname (cadr f))
+ (args (caddr f))
+ (body (cadddr f)))
+ (mv-let (term defs) (translate-function-block (cdr body) fname 0)
+ (append defs (list `(defun ,fname ,args ,term))))))
+
+(defun translate-program-list (lst)
+ (if (consp lst)
+ (case (caar lst)
+ ((declare array) (cons (translate-global-constant (car lst))
(translate-program-list (cdr lst))))
+ (funcdef (append (translate-function (car lst))
(translate-program-list (cdr lst)))))
+ ()))
+
+(set-state-ok t)
+
+(defun translate-program (infile outfile state)
+ (mv-let (foo lst state)
+ (read-list infile () state)
+ (declare (ignore foo))
+ (write-list (append '((in-package "ACL2")
+
(include-book "rtl/rel9/lib/masc" :dir :system)
+ (set-ignore-ok t)
+ (set-irrelevant-formals-ok t))
+ (translate-program-list lst) )
+ outfile
+ ()
+ state)))