-
Notifications
You must be signed in to change notification settings - Fork 9
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
2f58ef7
commit 6f691ed
Showing
2 changed files
with
67 additions
and
73 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,18 +1,20 @@ | ||
| (module add) | ||
|
|
||
| (defcolumns | ||
| STAMP | ||
| CT | ||
| INST | ||
| ARG_1_HI | ||
| ARG_1_LO | ||
| ARG_2_HI | ||
| ARG_2_LO | ||
| RES_HI | ||
| RES_LO | ||
| (BYTE_1 :byte) | ||
| (BYTE_2 :byte) | ||
| ACC_1 | ||
| ACC_2 | ||
| (OVERFLOW :binary) | ||
| ) | ||
| (defcolumns | ||
| STAMP | ||
| (CT_MAX :byte) | ||
| (CT :byte) | ||
| (INST :byte :display :opcode) | ||
| ARG_1_HI | ||
| ARG_1_LO | ||
| ARG_2_HI | ||
| ARG_2_LO | ||
| RES_HI | ||
| RES_LO | ||
| (BYTE_1 :byte) | ||
| (BYTE_2 :byte) | ||
| ACC_1 | ||
| ACC_2 | ||
| (OVERFLOW :binary)) | ||
|
|
||
|
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,86 +1,78 @@ | ||
| (module add) | ||
|
|
||
| (defconst | ||
| ADD 1 | ||
| SUB 3 | ||
| LLARGEMO 15 | ||
| THETA 340282366920938463463374607431768211456) ;; note that 340282366920938463463374607431768211456 = 256^16 | ||
| (defconst | ||
| ADD 1 | ||
| SUB 3 | ||
| LLARGEMO 15 | ||
| LLARGE 16 | ||
| THETA 340282366920938463463374607431768211456) ;; note that 340282366920938463463374607431768211456 = 256^16 | ||
|
|
||
| (defconstraint stamp-constancies () | ||
| (begin (stamp-constancy STAMP ARG_1_HI) | ||
| (stamp-constancy STAMP ARG_1_LO) | ||
| (stamp-constancy STAMP ARG_2_HI) | ||
| (stamp-constancy STAMP ARG_2_LO) | ||
| (stamp-constancy STAMP RES_HI) | ||
| (stamp-constancy STAMP RES_LO) | ||
| (stamp-constancy STAMP INST) | ||
| (stamp-constancy STAMP CT_MAX))) | ||
|
|
||
| ;;;;;;;;;;;;;;;;;;;;;;;;; | ||
| ;; ;; | ||
| ;; 1.3 heartbeat ;; | ||
| ;; ;; | ||
| ;;;;;;;;;;;;;;;;;;;;;;;;; | ||
|
|
||
| (defconstraint first-row (:domain {0}) | ||
| (vanishes! STAMP)) | ||
| (vanishes! STAMP)) | ||
|
|
||
| (defconstraint heartbeat () | ||
| (begin | ||
| (if-zero STAMP | ||
| (begin | ||
| (vanishes! CT) | ||
| (vanishes! INST) | ||
| (debug (vanishes! ARG_1_HI)) | ||
| (debug (vanishes! ARG_1_LO)) | ||
| (debug (vanishes! ARG_2_HI)) | ||
| (debug (vanishes! ARG_2_LO)) | ||
| (debug (vanishes! RES_HI)) | ||
| (debug (vanishes! RES_LO)))) | ||
| (* (will-remain-constant! STAMP) (will-inc! STAMP 1)) | ||
| (if-not-zero (will-remain-constant! STAMP) (vanishes! (next CT))) | ||
| (if-not-zero STAMP | ||
| (if-eq-else CT LLARGEMO | ||
| (will-inc! STAMP 1) | ||
| (will-inc! CT 1))))) | ||
| (begin (if-zero STAMP | ||
| (begin (vanishes! INST) | ||
| (debug (vanishes! CT)) | ||
| (debug (vanishes! CT_MAX)))) | ||
| (any! (will-remain-constant! STAMP) (will-inc! STAMP 1)) | ||
| (if-not-zero (will-remain-constant! STAMP) | ||
| (vanishes! (next CT))) | ||
| (if-not-zero STAMP | ||
| (begin (any! (eq! INST ADD) (eq! INST SUB)) | ||
| (if-eq-else CT LLARGEMO (will-inc! STAMP 1) (will-inc! CT 1)) | ||
| (eq! (~ (* (- CT LLARGE) CT_MAX)) | ||
| 1))))) | ||
|
|
||
| (defconstraint last-row (:domain {-1}) | ||
| (if-not-zero STAMP (= CT LLARGEMO))) | ||
|
|
||
| (defconstraint stamp-constancies () | ||
| (begin | ||
| (stamp-constancy STAMP ARG_1_HI) | ||
| (stamp-constancy STAMP ARG_1_LO) | ||
| (stamp-constancy STAMP ARG_2_HI) | ||
| (stamp-constancy STAMP ARG_2_LO) | ||
| (stamp-constancy STAMP RES_HI) | ||
| (stamp-constancy STAMP RES_LO) | ||
| (stamp-constancy STAMP INST))) | ||
|
|
||
| (eq! CT CT_MAX)) | ||
|
|
||
| ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; | ||
| ;; ;; | ||
| ;; 1.4 binary, bytehood and byte decompositions ;; | ||
| ;; ;; | ||
| ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; | ||
|
|
||
| (defconstraint binary-and-byte-decompositions () | ||
| (begin | ||
| (is-binary OVERFLOW) | ||
| (byte-decomposition CT ACC_1 BYTE_1) | ||
| (byte-decomposition CT ACC_2 BYTE_2))) | ||
| (begin (is-binary OVERFLOW) | ||
| (byte-decomposition CT ACC_1 BYTE_1) | ||
| (byte-decomposition CT ACC_2 BYTE_2))) | ||
|
|
||
| ;; TODO: bytehood constraints | ||
|
|
||
|
|
||
| ;;;;;;;;;;;;;;;;;;;;;;;;;;; | ||
| ;; ;; | ||
| ;; 1.5 constraints ;; | ||
| ;; ;; | ||
| ;;;;;;;;;;;;;;;;;;;;;;;;;;; | ||
| (defconstraint adder-constraints (:guard STAMP) | ||
| (if-eq CT CT_MAX | ||
| (begin (eq! RES_HI ACC_1) | ||
| (eq! RES_LO ACC_2) | ||
| (if-not-zero (- INST SUB) | ||
| (begin (eq! (+ ARG_1_LO ARG_2_LO) | ||
| (+ RES_LO (* THETA OVERFLOW))) | ||
| (eq! (+ ARG_1_HI ARG_2_HI OVERFLOW) | ||
| (+ RES_HI | ||
| (* THETA (prev OVERFLOW)))))) | ||
| (if-not-zero (- INST ADD) | ||
| (begin (eq! (+ RES_LO ARG_2_LO) | ||
| (+ ARG_1_LO (* THETA OVERFLOW))) | ||
| (eq! (+ RES_HI ARG_2_HI OVERFLOW) | ||
| (+ ARG_1_HI | ||
| (* THETA (prev OVERFLOW))))))))) | ||
|
|
||
|
|
||
| (defconstraint adder-constraints () | ||
| (if-eq CT LLARGEMO | ||
| (begin (= RES_HI ACC_1) | ||
| (= RES_LO ACC_2) | ||
| (if-not-zero (- INST SUB) | ||
| (begin (= (+ ARG_1_LO ARG_2_LO) | ||
| (+ RES_LO (* THETA OVERFLOW))) | ||
| (= (+ ARG_1_HI ARG_2_HI OVERFLOW) | ||
| (+ RES_HI (* THETA (prev OVERFLOW)))))) | ||
| (if-not-zero (- INST ADD) | ||
| (begin (= (+ RES_LO ARG_2_LO) | ||
| (+ ARG_1_LO (* THETA OVERFLOW))) | ||
| (= (+ RES_HI ARG_2_HI OVERFLOW) | ||
| (+ ARG_1_HI (* THETA (prev OVERFLOW))))))))) |