;;; Copyright (C) 1990-1994 Computational Logic, Inc. All Rights
;;; Reserved. See the file LICENSE in this directory for the
;;; complete license agreement.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;
;;; RTL-LEVEL-SPEC.EVENTS
;;;
;;; Bishop C. Brock & Warren A. Hunt, Jr.
;;;
;;; This file contains an almost minimal set of events necessary to define
;;; the intermediate-level specification for the FM9001, RUN-FM9001. The
;;; definitions are presented in a top-down fashion. A few of the
;;; definitions required by the functions defined here appear in the file
;;; "high-level-spec.events". This file is intended to be loaded after
;;; that file. A Common Lisp "wrapper" around the events allows this file
;;; to be loaded as-is into an Nqthm session.
;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
#.`(PROGN ,@(reverse '(
;;;++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
;;;
;;; RTL-LEVEL Interpreters.
;;;
;;;++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
;;; RUN-FM9001 -- Simulates N clock cycles.
(defn run-fm9001 (state inputs n)
(if (zerop n)
state
(run-fm9001 (fm9001-next-state state (car inputs))
(cdr inputs)
(sub1 n))))
;;; FM9001-NEXT-STATE
;;;
;;; The specification of the next state of the processor and memory for a
;;; single clock cycle.
(defn FM9001-next-state (total-state external-inputs)
(let
((p-state (car total-state))
(mem-state (cadr total-state)))
(let
((regs (regs p-state))
(flags (flags p-state))
(a-reg (a-reg p-state))
(b-reg (b-reg p-state))
(i-reg (i-reg p-state))
(data-out (data-out p-state))
(addr-out (addr-out p-state))
(last-reset- (reset- p-state))
(last-dtack- (dtack- p-state))
(last-hold- (hold- p-state))
(last-pc-reg (pc-reg p-state))
(cntl-state (cntl-state p-state))
(reset- (reset--input external-inputs))
(hold- (hold--input external-inputs))
(pc-reg-in (pc-reg-input external-inputs)))
(let
((state (state (v-threefix cntl-state)))
(rw- (rw- (v-threefix cntl-state)))
(strobe- (strobe- (v-threefix cntl-state)))
(hdack- (hdack- (v-threefix cntl-state)))
(we-regs (we-regs (v-threefix cntl-state)))
(we-flags (we-flags (v-threefix cntl-state)))
(we-a-reg (we-a-reg (v-threefix cntl-state)))
(we-b-reg (we-b-reg (v-threefix cntl-state)))
(we-i-reg (we-i-reg (v-threefix cntl-state)))
(we-data-out (we-data-out (v-threefix cntl-state)))
(we-addr-out (we-addr-out (v-threefix cntl-state)))
(we-hold- (we-hold- (v-threefix cntl-state)))
(we-pc-reg (we-pc-reg (v-threefix cntl-state)))
(data-in-select (data-in-select (v-threefix cntl-state)))
(dec-addr-out (dec-addr-out (v-threefix cntl-state)))
(select-immediate (select-immediate (v-threefix cntl-state)))
(regs-address (regs-address (v-threefix cntl-state)))
(alu-c (alu-c (v-threefix cntl-state)))
(alu-op (alu-op (v-threefix cntl-state)))
(alu-zero (alu-zero (v-threefix cntl-state)))
(alu-mpg (alu-mpg (v-threefix cntl-state))))
;; ADDR-OUT, RW- and STROBE- are tristate when HOLDing, and pulled
;; high by external pullups. The EXT- (external) signals are used
;; only by the memory interface.
(let
((ext-addr-out
(v-pullup (vft-buf (f-buf hdack-)
(v-threefix addr-out))))
(ext-rw-
(f-pullup (ft-buf (f-buf hdack-) (f-buf rw-))))
(ext-strobe-
(f-pullup (ft-buf (f-buf hdack-) strobe-)))
(ext-data-out
(vft-buf (f-not (f-buf rw-)) (v-threefix data-out))))
(let
((mem-response
(memory-value mem-state ext-strobe- ext-rw-
ext-addr-out
(make-list 32 (x)))))
(let
((dtack- (car mem-response))
(ext-data-bus (v-pullup
(v-wire ext-data-out (cdr mem-response)))))
(let
((reg-bus (f$extend-immediate
select-immediate
(a-immediate (v-threefix i-reg))
(f$read-regs regs-address regs)))
(alu-bus (f$core-alu alu-c
(v-threefix a-reg)
(v-threefix b-reg)
alu-zero alu-mpg alu-op
(make-tree 32)))
(data-in (v-threefix (v-wire ext-data-bus ext-data-out))))
(let
((addr-out-bus (f$dec-pass dec-addr-out reg-bus))
(abi-bus
(fv-if (f-nand data-in-select
(f-not last-dtack-))
reg-bus
data-in)))
(list
(list
(f$write-regs we-regs regs-address regs (bv alu-bus))
(f$update-flags flags we-flags alu-bus)
(fv-if we-a-reg abi-bus a-reg)
(fv-if we-b-reg abi-bus b-reg)
(fv-if we-i-reg abi-bus i-reg)
(fv-if we-data-out (bv alu-bus) data-out)
(fv-if we-addr-out addr-out-bus addr-out)
(f-buf reset-)
(f-or strobe- (f-buf dtack-))
(f-if we-hold- (f-buf hold-) last-hold-)
(fv-if we-pc-reg pc-reg-in last-pc-reg)
(v-threefix (f$next-cntl-state
(f-buf last-reset-)
(f-buf last-dtack-)
(f-buf last-hold-)
rw-
state
(v-threefix i-reg)
(v-threefix flags)
(v-threefix last-pc-reg)
regs-address)))
(next-memory-state
mem-state ext-strobe- ext-rw-
ext-addr-out
ext-data-bus)))))))))))
;;;++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
;;;
;;; State and Input Definitions.
;;;
;;;++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
;;; Internal states.
;(defn regs (state) (nth 0 state))
;(defn flags (state) (nth 1 state))
(defn a-reg (state) (nth 2 state))
(defn b-reg (state) (nth 3 state))
(defn i-reg (state) (nth 4 state))
(defn data-out (state) (nth 5 state))
(defn addr-out (state) (nth 6 state))
(defn reset- (state) (nth 7 state))
(defn dtack- (state) (nth 8 state))
(defn hold- (state) (nth 9 state))
(defn pc-reg (state) (nth 10 state))
(defn cntl-state (state) (nth 11 state))
;;; External Inputs.
(defn reset--input (ext-in) (nth 0 ext-in))
(defn hold--input (ext-in) (nth 1 ext-in))
(defn pc-reg-input (ext-in) (subrange ext-in 2 5))
;;; Control state.
(defn rw- (cntl-state) (nth 0 cntl-state))
(defn strobe- (cntl-state) (nth 1 cntl-state))
(defn hdack- (cntl-state) (nth 2 cntl-state))
(defn we-regs (cntl-state) (nth 3 cntl-state))
(defn we-a-reg (cntl-state) (nth 4 cntl-state))
(defn we-b-reg (cntl-state) (nth 5 cntl-state))
(defn we-i-reg (cntl-state) (nth 6 cntl-state))
(defn we-data-out (cntl-state) (nth 7 cntl-state))
(defn we-addr-out (cntl-state) (nth 8 cntl-state))
(defn we-hold- (cntl-state) (nth 9 cntl-state))
(defn we-pc-reg (cntl-state) (nth 10 cntl-state))
(defn data-in-select (cntl-state) (nth 11 cntl-state))
(defn dec-addr-out (cntl-state) (nth 12 cntl-state))
(defn select-immediate (cntl-state) (nth 13 cntl-state))
(defn alu-c (cntl-state) (nth 14 cntl-state))
(defn alu-zero (cntl-state) (nth 15 cntl-state))
(defn state (cntl-state) (subrange cntl-state 16 20))
(defn we-flags (cntl-state) (subrange cntl-state 21 24))
(defn regs-address (cntl-state) (subrange cntl-state 25 28))
(defn alu-op (cntl-state) (subrange cntl-state 29 32))
(defn alu-mpg (cntl-state) (subrange cntl-state 33 39))
;;;++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
;;;
;;; REGISTER FILE
;;;
;;;++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
;;; F$READ-REGS -- Read a value from the register file.
(defn f$read-regs (address regs)
(let ((regfile (car regs))
(last-we (cadr regs))
(last-data (caddr regs))
(last-address (cadddr regs)))
(fv-if
(f-and3 (f-buf last-we)
(f$v-equal address (v-threefix last-address))
t)
(v-threefix last-data)
(dual-port-ram-value
32 4
(append address
(append (v-threefix last-address)
(cons (f-nand t (f-buf last-we))
(v-threefix last-data))))
regfile))))
;;; F$WRITE-REGS -- Write a value to the register file.
(defn f$write-regs (we address regs data)
(let ((regfile (car regs))
(last-we (cadr regs))
(last-data (caddr regs))
(last-address (cadddr regs)))
(list
(dual-port-ram-state
32 4
(append address
(append (v-threefix last-address)
(cons (f-nand t (f-buf last-we))
(v-threefix last-data))))
regfile)
(threefix we)
(fv-if we
data
last-data)
(fv-if we
address
last-address))))
;;; (DUAL-PORT-RAM-VALUE bits address-lines args state)
;;;
;;; returns the RAM output, i.e., the contents of the memory addressed by the
;;; read-adress port.
;;;
;;; (DUAL-PORT-RAM-STATE bits address-lines args state)
;;;
;;; updates the state of the RAM.
;;;
;;; The ARGS are assumed to be structured as follows:
;;;
;;; 0..(ADDRESS-LINES - 1) -- A (read port) address.
;;; ADDRESS-LINES..(2*ADDRESS-LINES - 1) -- B (write port) address.
;;; (2*ADDRESS-LINES) -- WEN, active low.
;;; remainder -- DATA lines.
;;;
;;; WARNING -- This is a sequential model of what is essentially a
;;; level-sensitive device. Note that this state-holding device has no clock
;;; input. Spikes on WEN, or changes on B-ADDRESS while WEN is active may
;;; cause unanticipated changes in the memory state of the real device.
;;;
;;; The dual-port RAM used in the register file of the FM9001 is surrounded
;;; by sequential logic that ensures that setup and hold constraints are met.
;;; See the file "regfile.events".
(defn dual-port-ram-value (bits address-lines args state)
(let ((a-address (subrange args 0 (sub1 address-lines)))
(b-address (subrange args address-lines
(sub1 (times 2 address-lines))))
(wen (nth (times 2 address-lines) args)))
;; If the read address is unknown, or the device is potentially write
;; enabled and there is a potential write at the read address, then read
;; out X's. Otherwise, read out the vector from the STATE.
(if (or (not (bvp a-address))
(and (not (equal wen t))
(or (not (bvp b-address))
(equal a-address b-address))))
(make-list bits (x))
(let ((val (read-mem a-address state)))
(if (and (properp val)
(equal (length val) bits))
val
;; Return an unknown proper list of the right length if we don't read
;; a proper list of the right length.
(make-list bits (x)))))))
(defn dual-port-ram-state (bits address-lines args state)
(let ((b-address (subrange args address-lines
(sub1 (times 2 address-lines))))
(wen (nth (times 2 address-lines) args))
;; Use SUBRANGE instead of RESTN so that we are guaranteed
;; that this argument has the right length and is a PROPERP.
;; Note that we use bits below rather than (length args)
;; in order to ensure that data has the right length.
(data
(subrange args
(add1 (times 2 address-lines))
(plus (times 2 address-lines) bits))))
;; If WEN is solidly high, do nothing.
(if (equal wen t)
state
;; There is a potential write. If the address is unknown, wipe out the
;; state.
(if (not (bvp b-address))
(constant-ram state (make-list bits (x)))
;; If WEN is solidly low, update the state with data, otherwise X out
;; the addressed entry.
(if (equal wen f)
(write-mem b-address state data)
(write-mem b-address state (make-list bits (x))))))))
;;; F$V-EQUAL -- A comparator.
(defn f$v-equal (a b)
(f$tv-zerop (fv-xor a b) (make-tree (length a))))
;;; F$TV-ZEROP -- An OR-NOR tree. See also F$FAST-ZERO below.
(defn f$tv-zerop (a tree)
(let ((odd-height (equal (remainder (tree-height tree) 2) 1)))
(if odd-height
(f-not (tr-or-nor a f tree))
(tr-or-nor a t tree))))
;;;++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
;;;
;;; THE ALU
;;;
;;;++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
;;; CORE-ALU is the hardware implementation of the high-level specification
;;; V-ALU. In addition to the functions provided by V-ALU, CORE-ALU also can
;;; be forced to 0, and includes INC B and DEC B operations for address
;;; calculations. Note that the control lines for the function generators
;;; (MPG) are supplied by the control logic.
;;;
;;; Since CORE-ALU is defined in terms of F$FAST-ZERO, only ALU sizes of >= 3
;;; bits have the desired properties.
(defn f$core-alu (c a b zero mpg op tree)
(let ((op0 (car op))
(op1 (cadr op))
(op2 (caddr op))
(op3 (cadddr op)))
(let ((last-bit (sub1 (length a))))
(let ((alu-help (f$tv-alu-help c a b mpg tree)))
(let ((alu-p (car alu-help))
(alu-g (cadr alu-help))
(alu-sum (cddr alu-help)))
(let ((alu-carry (f$t-carry c alu-p alu-g))
(out (f$shift-or-buf c alu-sum (nth (sub1 (length a)) a)
zero op0 op1 op2 op3)))
(cons (f$carry-out-help (nth 0 a) alu-carry zero op0 op1 op2 op3)
(cons (f$overflow-help (nth last-bit alu-sum)
(nth last-bit a)
(nth last-bit b)
zero op0 op1 op2 op3)
(cons (f$fast-zero out)
out)))))))))
;;; F$TV-ALU-HELP -- The tree-structured ALU function generator.
(defn f$tv-alu-help (c a b mpg tree)
(if (nlistp tree)
(f$alu-cell c (car a) (car b) mpg)
(let ((a-car (tfirstn a tree))
(b-car (tfirstn b tree))
(a-cdr (trestn a tree))
(b-cdr (trestn b tree)))
(let ((lhs (f$tv-alu-help c a-car b-car mpg (car tree))))
(let ((p-car (car lhs))
(g-car (cadr lhs))
(sum-car (cddr lhs)))
(let ((c-car (f$t-carry c p-car g-car)))
(let ((rhs (f$tv-alu-help c-car a-cdr b-cdr mpg (cdr tree))))
(let ((p-cdr (car rhs))
(g-cdr (cadr rhs))
(sum-cdr (cddr rhs)))
(cons (f-and p-car p-cdr)
(cons (f$t-carry g-car p-cdr g-cdr)
(append sum-car sum-cdr)))))))))))
(defn f$alu-cell (c a b mpg)
(let ((gbn (car mpg))
(gan (cadr mpg))
(ga (caddr mpg))
(pb (cadddr mpg))
(pan (caddddr mpg))
(pa (cadddddr mpg))
(m (caddddddr mpg)))
(let ((an (f-not a))
(bn (f-not b)))
(let ((p (f$p-cell a an b pa pan pb))
(g (f$g-cell a an bn ga gan gbn))
(mc (f-nand c m)))
(let ((z (f-equv3 mc p g)))
(list p g z))))))
(defn f$p-cell (a an b pa pan pb)
(f-nand3 (f-nand a pa)
(f-nand an pan)
(f-nand b pb)))
(defn f$g-cell (a an bn ga gan gbn)
(f-and3 (f-nand a ga)
(f-nand an gan)
(f-nand bn gbn)))
(defn f$t-carry (c prop gen)
(f-or (f-and c prop) gen))
;;; F$SHIFT-OR-BUF -- The shift unit.
(defn f$shift-or-buf (c a an zero op0 op1 op2 op3)
(let ((pass (car (f$shift-or-buf-cntl c an zero op0 op1 op2 op3)))
(si (cadr (f$shift-or-buf-cntl c an zero op0 op1 op2 op3))))
(fv-if pass a (fv-shift-right a si))))
(defn f$shift-or-buf-cntl (c an zero op0 op1 op2 op3)
(list (f-or3 (f-and op0 op1)
(f-nand (f-not op2) op3)
zero)
(f-or (f-and op0 an)
(f-and (f-and (f-not op0) (f-not op1))
c))))
(defn fv-shift-right (a si)
(if (nlistp a)
nil
(append (v-threefix (cdr a))
(list (threefix si)))))
;;; CARRY and OVERFLOW outputs.
(defn f$carry-out-help (a0 result zero op0 op1 op2 op3)
(let ((result- (f-not result)) (zero- (f-not zero))
(op0- (f-not op0)) (op1- (f-not op1))
(op2- (f-not op2)) (op3- (f-not op3)))
(let ((op0 (f-not op0-)) (op1 (f-not op1-))
(op2 (f-not op2-)) (op3 (f-not op3-)))
(f-and (f-nand3 (f-nand4 op3- (f-nand op0- op1-) op2- result)
(f-nand3 op3- op2 result-)
(f-nand4 op3 op2- (f-nand op0 op1) a0))
zero-))))
(defn f$overflow-help (rn an bn zero op0 op1 op2 op3)
(let ((an- (f-not an)) (zero- (f-not zero))
(op1- (f-not op1)) (op2- (f-not op2))
(op3- (f-not op3)))
(let ((an (f-not an-)) (zero (f-not zero-)) (op2 (f-not op2-)))
(f-if rn
(f-nor (f-nand (f-nor (f-nand3 op3-
(f-or3 op1- op2- (f-xor an bn))
(f-nand3 op1- op2 an-))
(f-nand (f-nand3 op1 op2- (f-xor an bn))
(f-nand3 op1- op2- an)))
zero-)
(f-nand3 (f-nand op2 an-)
(f-nand3 op0 op1- an)
(f-nand op2- an)))
(f-nor (f-nand (f-nor (f-nand3 op3-
(f-or3 op1- op2- (f-xor an bn))
(f-nand3 op1- op2 an-))
(f-nand (f-nand3 op1 op2- (f-xor an bn))
(f-nand3 op1- op2- an)))
zero-)
(f-not (f-nand3 (f-nand op2 an-)
(f-nand3 op0 op1- an)
(f-nand op2- an))))))))
;;; F$FAST-ZERO -- The zero detector.
(defn f$fast-zero (v)
(f-nor3 (tr-or-nor (firstn (sub1 (sub1 (length v))) v)
f
(make-tree (sub1 (sub1 (length v)))))
(nth (sub1 (sub1 (length v))) v)
(nth (sub1 (length v)) v)))
(defn tr-or-nor (a parity tree)
(if (nlistp tree)
(if parity (f-not (car a)) (f-buf (car a)))
(if (and (nlistp (car tree))
(nlistp (cdr tree)))
(if parity
(f-nor (car a) (cadr a))
(f-or (car a) (cadr a)))
(if parity
(f-nor (tr-or-nor (tfirstn a tree) (not parity) (car tree))
(tr-or-nor (trestn a tree) (not parity) (cdr tree)))
(f-nand (tr-or-nor (tfirstn a tree) (not parity) (car tree))
(tr-or-nor (trestn a tree) (not parity) (cdr tree)))))))
;;;++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
;;;
;;; MISCELLANEOUS DEFINITIONS
;;;
;;;++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
;;; F$EXTEND-IMMEDIATE -- The immediate/pass unit.
(defn f$extend-immediate (select-immediate immediate reg-data)
(fv-if select-immediate
(append immediate
(if (boolp (nth 8 immediate))
(make-list 23 (nth 8 immediate))
(make-list 23 (x))))
reg-data))
;;; F$DEC-PASS -- The decrement/pass unit is implemented by a special
;;; tree-based decrementer with fast carry-lookahead.
(defn f$dec-pass (c a)
(f$tv-dec-pass-ng (f-not c) a (make-tree (length a)) f))
(defn f$tv-dec-pass-ng (c a tree make-g)
(if (nlistp tree)
(if make-g
(list (car a) (f-equv (car a) c))
(list (f-equv (car a) c)))
(let ((lhs (f$tv-dec-pass-ng c
(tfirstn a tree)
(car tree)
t)))
(let ((rhs (f$tv-dec-pass-ng (f-or c (car lhs))
(trestn a tree)
(cdr tree)
make-g)))
(if make-g
(cons (f-or (car lhs) (car rhs))
(append (cdr lhs) (cdr rhs)))
(append (cdr lhs) rhs))))))
;;; F$UPDATE-FLAGS -- The new state of the FLAGS register.
(defn f$update-flags (flags set-flags cvzbv)
(list (f-if (z-set set-flags)
(zb cvzbv)
(z-flag flags))
(f-if (n-set set-flags)
(n cvzbv)
(n-flag flags))
(f-if (v-set set-flags)
(v cvzbv)
(v-flag flags))
(f-if (c-set set-flags)
(c cvzbv)
(c-flag flags))))
;;;++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
;;;
;;; CONTROL LOGIC
;;;
;;;++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
;;; F$NEXT-CONTROL-STATE -- The complete control logic.
(defn f$next-cntl-state (reset- dtack- hold- rw-
state i-reg flags pc-reg regs-address)
(let ((control-let (f$control-let i-reg flags regs-address))
(set-flags (set-flags i-reg))
(op-code (op-code i-reg))
(rn-a (rn-a i-reg))
(rn-b (rn-b i-reg)))
(let
((a-immediate-p (car control-let))
(store (cadr control-let))
(set-some-flags (caddr control-let))
(direct-a (cadddr control-let))
(direct-b (caddddr control-let))
(unary (cadddddr control-let))
(pre-dec-a (caddddddr control-let))
(pre-dec-b (cadddddddr control-let))
(c (caddddddddr control-let))
(all-t-regs-address (cadddddddddr control-let))
(side-effect-a (caddddddddddr control-let))
(side-effect-b (cadddddddddddr control-let)))
;; this forces an illegal state if reset- is asserted, thus sending the
;; machine to reset0.
(let ((decoded-state (f$decode-5 (fv-or
(make-list 5 (f-not reset-))
state))))
(let ((next-state
(f$next-state decoded-state store set-some-flags unary direct-a
direct-b side-effect-a side-effect-b
all-t-regs-address dtack- hold-)))
(f$cv next-state
rn-a rn-b op-code
pc-reg regs-address set-flags
store c a-immediate-p rw-
direct-a side-effect-a side-effect-b
pre-dec-a pre-dec-b))))))
;;; F$CONTROL-LET -- Summarizes conditions in the instruction word.
(defn f$control-let (i-reg flags regs-address)
(let ((a-immediate-p (a-immediate-p i-reg))
(mode-a (mode-a i-reg))
(rn-a (rn-a i-reg))
(mode-b (mode-b i-reg))
(rn-b (rn-b i-reg))
(set-flags (set-flags i-reg))
(store-cc (store-cc i-reg))
(op-code (op-code i-reg)))
(let
((a-immediate-p (id a-immediate-p)))
(let
((a-immediate-p- (f-not a-immediate-p))
(store (f$b-store-resultp store-cc flags))
(set-some-flags (f$set-some-flags set-flags))
(decode-reg-a-mode (f$decode-reg-mode mode-a))
(decode-reg-b-mode (f$decode-reg-mode mode-b)))
(let
((almost-direct-a (car decode-reg-a-mode))
(pre-dec-a (cadr decode-reg-a-mode))
(almost-side-effect-a (caddr decode-reg-a-mode))
(direct-b (car decode-reg-b-mode))
(pre-dec-b (cadr decode-reg-b-mode))
(side-effect-b (caddr decode-reg-b-mode))
(unary (f$unary-op-code-p op-code))
(c (id (c-flag flags)))
(all-t-regs-address (f$all-t-regs-address regs-address)))
(let
((side-effect-a (f-and a-immediate-p- almost-side-effect-a))
(direct-a (f-or a-immediate-p almost-direct-a)))
(list a-immediate-p store set-some-flags direct-a direct-b unary
pre-dec-a pre-dec-b c all-t-regs-address
side-effect-a side-effect-b)))))))
(defn f$b-store-resultp (store-cc flags)
(let ((s0 (car store-cc)) (s1 (cadr store-cc))
(s2 (caddr store-cc)) (s3 (cadddr store-cc))
(z (car flags)) (n (cadr flags)) (v (caddr flags)) (c (cadddr flags)))
(f-xor s0 (f$store-resultp-mux
s1 s2 s3
c v n z
(f-or c z) (f-xor n v) (f-or z (f-xor n v))))))
(defn f$store-resultp-mux (s0 s1 s2 d0 d1 d2 d3 d4 d5 d6)
(let ((s0- (f-not s0)) (s1- (f-not s1)) (s2- (f-not s2)))
(let ((x01 (f$ao2 s0- d0 s0 d1)) (x23 (f$ao2 s0- d2 s0 d3))
(x45 (f$ao2 s0- d4 s0 d5)) (x67 (f-nand s0- d6)))
(let ((x0123 (f$ao2 s1- x01 s1 x23)) (x4567 (f$ao2 s1- x45 s1 x67)))
(f$ao2 s2- x0123 s2 x4567)))))
(defn f$set-some-flags (set-flags)
(f-or4 (car set-flags)
(cadr set-flags)
(caddr set-flags)
(cadddr set-flags)))
(defn f$decode-reg-mode (m)
(let ((m0 (car m))
(m1 (cadr m)))
(list (f-nor m0 m1)
(f-nor m0 (f-not m1))
(id m1))))
(defn f$unary-op-code-p (op)
(let ((op0 (car op)) (op1 (cadr op)) (op2 (caddr op)) (op3 (cadddr op)))
(let ((op0- (f-not op0)) (op1- (f-not op1))
(op2- (f-not op2)) (op3- (f-not op3)))
(let ((s0 (f-nand op3- op1-)) (s1 (f-nand op2- op1-))
(s2 (f-nand3 op3 op1 op0-)) (s3 (f-nand3 op3 op2 op1)))
(f-nand4 s0 s1 s2 s3)))))
(defn f$all-t-regs-address (regs-address)
(f-and4 (car regs-address)
(cadr regs-address)
(caddr regs-address)
(cadddr regs-address)))
;;; F$DECODE-5 -- A 5-to-32 decoder.
(defn f$decode-5 (s)
(let ((s0 (car s)) (s1 (cadr s)) (s2 (caddr s)) (s3 (cadddr s))
(s4 (caddddr s)))
(let ((s0- (f-not s0)) (s1- (f-not s1)) (s2- (f-not s2)) (s3- (f-not s3))
(s4- (f-not s4)))
(let ((s0 (f-not s0-)) (s1 (f-not s1-)) (s2 (f-not s2-)) (s3 (f-not s3-))
(s4 (f-not s4-)))
(let ((l0 (f-nand s0- s1-)) (l1 (f-nand s0 s1-))
(l2 (f-nand s0- s1)) (l3 (f-nand s0 s1))
(h0 (f-nand3 s2- s3- s4-)) (h1 (f-nand3 s2 s3- s4-))
(h2 (f-nand3 s2- s3 s4-)) (h3 (f-nand3 s2 s3 s4-))
(h4 (f-nand3 s2- s3- s4)) (h5 (f-nand3 s2 s3- s4))
(h6 (f-nand3 s2- s3 s4)) (h7 (f-nand3 s2 s3 s4)))
(let ((x00 (f-nor l0 h0)) (x10 (f-nor l1 h0))
(x20 (f-nor l2 h0)) (x30 (f-nor l3 h0))
(x01 (f-nor l0 h1)) (x11 (f-nor l1 h1))
(x21 (f-nor l2 h1)) (x31 (f-nor l3 h1))
(x02 (f-nor l0 h2)) (x12 (f-nor l1 h2))
(x22 (f-nor l2 h2)) (x32 (f-nor l3 h2))
(x03 (f-nor l0 h3)) (x13 (f-nor l1 h3))
(x23 (f-nor l2 h3)) (x33 (f-nor l3 h3))
(x04 (f-nor l0 h4)) (x14 (f-nor l1 h4))
(x24 (f-nor l2 h4)) (x34 (f-nor l3 h4))
(x05 (f-nor l0 h5)) (x15 (f-nor l1 h5))
(x25 (f-nor l2 h5)) (x35 (f-nor l3 h5))
(x06 (f-nor l0 h6)) (x16 (f-nor l1 h6))
(x26 (f-nor l2 h6)) (x36 (f-nor l3 h6))
(x07 (f-nor l0 h7)) (x17 (f-nor l1 h7))
(x27 (f-nor l2 h7)) (x37 (f-nor l3 h7)))
(list x00 x10 x20 x30 x01 x11 x21 x31 x02 x12 x22 x32 x03 x13 x23
x33 x04 x14 x24 x34 x05 x15 x25 x35 x06 x16 x26 x36 x07 x17
x27 x37)))))))
;;; F$NEXT-STATE -- Computes the next state as a decoded, 32-bit vector. This
;;; function is synthesized from a tabular description of the FM9001 state
;;; machine.
(defn f$next-state (decoded-state store set-some-flags unary direct-a direct-b
side-effect-a side-effect-b
all-t-regs-address dtack- hold-)
(list (f-nand (f-and4 (f-nand all-t-regs-address
(nth 30 decoded-state))
(f-not (nth 25 decoded-state))
(f-not (nth 23 decoded-state))
(f-nand (f-not side-effect-b)
(nth 21 decoded-state)))
(f-and3 (f-nand (f-not dtack-)
(nth 19 decoded-state))
(f-nand (f-not (f-and side-effect-b unary))
(nth 7 decoded-state))
(f-nand4 (f-not side-effect-b) (f-not side-effect-a)
(f-not (f-or store set-some-flags))
(nth 4 decoded-state))))
(nth 0 decoded-state)
(f-and hold- (nth 1 decoded-state))
(f-nand (f-nand dtack- (nth 3 decoded-state))
(f-not (nth 2 decoded-state)))
(f-and (f-not dtack-) (nth 3 decoded-state))
(f-and4 (f-or direct-b unary) direct-a
(f-or store set-some-flags) (nth 4 decoded-state))
(f-and3 (f-not unary) direct-b (nth 5 decoded-state))
(f-nand6 (f-nand3 (f-not store) (f-not dtack-) (nth 15 decoded-state))
(f-nand5 (f-not store) unary (f-not direct-b) (f-not dtack-)
(nth 11 decoded-state))
(f-nand3 direct-b (f-not dtack-) (nth 11 decoded-state))
(f-not (nth 6 decoded-state))
(f-nand3 (f-not store) (f-not direct-b)
(nth 5 decoded-state))
(f-nand3 unary direct-b (nth 5 decoded-state)))
(f-and3 (f-not direct-a) (f-or store set-some-flags)
(nth 4 decoded-state))
(nth 8 decoded-state)
(nth 9 decoded-state)
(f-nand (f-nand dtack- (nth 11 decoded-state))
(f-not (nth 10 decoded-state)))
(f-nand (f-nand4 (f-not unary) (f-not direct-b)
(f-not dtack-) (nth 11 decoded-state))
(f-nand4 (f-not (f-or direct-b unary)) direct-a
(f-or store set-some-flags)
(nth 4 decoded-state)))
(nth 12 decoded-state)
(nth 13 decoded-state)
(f-nand (f-nand dtack- (nth 15 decoded-state))
(f-not (nth 14 decoded-state)))
(f-nand3 (f-nand3 store (f-not dtack-) (nth 15 decoded-state))
(f-nand5 store unary (f-not direct-b) (f-not dtack-)
(nth 11 decoded-state))
(f-nand3 store (f-not direct-b) (nth 5 decoded-state)))
(nth 16 decoded-state)
(nth 17 decoded-state)
(f-nand (f-nand dtack- (nth 19 decoded-state))
(f-not (nth 18 decoded-state)))
(f-and3 side-effect-a (f-not (f-or store set-some-flags))
(nth 4 decoded-state))
(nth 20 decoded-state)
(f-nand (f-nand side-effect-b (nth 21 decoded-state))
(f-nand4 side-effect-b (f-not side-effect-a)
(f-not (f-or store set-some-flags))
(nth 4 decoded-state)))
(f-nand (f-not (nth 22 decoded-state))
(f-nand (f-and side-effect-b unary) (nth 7 decoded-state)))
(f-nand (f-nand (f-not hold-) (nth 24 decoded-state))
(f-nand (f-not hold-) (nth 1 decoded-state)))
(f-and hold- (nth 24 decoded-state))
(vss)
(vss)
(f-nand3 (f-not (nth 31 decoded-state)) (f-not (nth 27 decoded-state))
(f-not (nth 26 decoded-state)))
(nth 28 decoded-state)
(f-nand (f-nand (f-not all-t-regs-address) (nth 30 decoded-state))
(f-not (nth 29 decoded-state)))
(vss)))
;;; F$CV -- Computes the 40-bit control vector. This function is generated
;;; largely automatically.
(defn f$cv (decoded-state rn-a rn-b op-code pc-reg regs-address set-flags
store c a-immediate-p rw- direct-a side-effect-a
side-effect-b pre-dec-a pre-dec-b)
(cons
(f-and (f-nand (f-not rw-) (nth 0 decoded-state))
(f-nor3 (nth 17 decoded-state) (nth 18 decoded-state)
(nth 19 decoded-state)))
(cons
(f-nor8 (nth 2 decoded-state) (nth 3 decoded-state) (nth 10 decoded-state)
(nth 11 decoded-state) (nth 14 decoded-state)
(nth 15 decoded-state) (nth 18 decoded-state)
(nth 19 decoded-state))
(cons
(f-not (nth 24 decoded-state))
(cons
(f-nand5 (f-nand store (nth 7 decoded-state))
(f-nand side-effect-a (nth 9 decoded-state))
(f-nand3 (f-not store) side-effect-b (nth 14 decoded-state))
(f-nand side-effect-b (nth 17 decoded-state))
(f-nor5 (nth 2 decoded-state) (nth 21 decoded-state)
(nth 23 decoded-state) (nth 28 decoded-state)
(nth 30 decoded-state)))
(cons
(f-nand (f-nand direct-a (nth 13 decoded-state))
(f-nor6 (nth 0 decoded-state) (nth 5 decoded-state)
(nth 8 decoded-state) (nth 11 decoded-state)
(nth 20 decoded-state) (nth 29 decoded-state)))
(cons
(f-nand (f-nor4 (nth 6 decoded-state) (nth 7 decoded-state)
(nth 10 decoded-state) (nth 12 decoded-state))
(f-nor4 (nth 15 decoded-state) (nth 16 decoded-state)
(nth 22 decoded-state) (nth 29 decoded-state)))
(cons
(f-or (nth 3 decoded-state) (nth 29 decoded-state))
(cons
(f-or (nth 16 decoded-state) (nth 28 decoded-state))
(cons
(f-nand (f-nor3 (nth 0 decoded-state) (nth 8 decoded-state)
(nth 12 decoded-state))
(f-nor (nth 16 decoded-state) (nth 29 decoded-state)))
(cons
(f-or3 (nth 0 decoded-state) (nth 24 decoded-state)
(nth 28 decoded-state))
(cons
(f-or (nth 24 decoded-state) (nth 28 decoded-state))
(cons
(f-or3 (nth 3 decoded-state) (nth 11 decoded-state)
(nth 15 decoded-state))
(cons
(f-nand (f-nand pre-dec-a (nth 8 decoded-state))
(f-nand pre-dec-b
(f-or (nth 12 decoded-state)
(nth 16 decoded-state))))
(cons
(f-and a-immediate-p
(f-or (nth 5 decoded-state) (nth 13 decoded-state)))
(cons
(f$carry-in-help
(cons
c
(cons
(f-or4 (nth 0 decoded-state) (nth 28 decoded-state)
(nth 29 decoded-state) (nth 30 decoded-state))
(f$select-op-code
(f-nor4
(nth 2 decoded-state)
(f-or (nth 9 decoded-state) (nth 21 decoded-state))
(f-or3 (nth 14 decoded-state) (nth 17 decoded-state)
(nth 23 decoded-state))
(f-or4 (nth 0 decoded-state) (nth 28 decoded-state)
(nth 29 decoded-state) (nth 30 decoded-state)))
(f-nand (f-nand (f-or (nth 9 decoded-state)
(nth 21 decoded-state))
pre-dec-a)
(f-nand (f-or3 (nth 14 decoded-state)
(nth 17 decoded-state)
(nth 23 decoded-state))
pre-dec-b))
op-code))))
(cons
(f-or4 (nth 0 decoded-state) (nth 28 decoded-state)
(nth 29 decoded-state) (nth 30 decoded-state))
(append
(f$encode-32
(nth 0 decoded-state) (nth 1 decoded-state)
(nth 2 decoded-state) (nth 3 decoded-state)
(nth 4 decoded-state) (nth 5 decoded-state)
(nth 6 decoded-state) (nth 7 decoded-state)
(nth 8 decoded-state) (nth 9 decoded-state)
(nth 10 decoded-state) (nth 11 decoded-state)
(nth 12 decoded-state) (nth 13 decoded-state)
(nth 14 decoded-state) (nth 15 decoded-state)
(nth 16 decoded-state) (nth 17 decoded-state)
(nth 18 decoded-state) (nth 19 decoded-state)
(nth 20 decoded-state) (nth 21 decoded-state)
(nth 22 decoded-state) (nth 23 decoded-state)
(nth 24 decoded-state) (nth 25 decoded-state)
(nth 26 decoded-state) (nth 27 decoded-state)
(nth 28 decoded-state) (nth 29 decoded-state)
(nth 30 decoded-state) (nth 31 decoded-state))
(append
(fv-if
(f-nor (nth 7 decoded-state) (nth 16 decoded-state))
(make-list 4 (threefix (nth 28 decoded-state)))
set-flags)
(append
(fv-if
(f-nand
(f-nor3 (nth 5 decoded-state) (nth 8 decoded-state)
(nth 9 decoded-state))
(f-nor3 (nth 13 decoded-state) (nth 20 decoded-state)
(nth 21 decoded-state)))
rn-a
(fv-if
(f-nand
(f-nor5 (nth 6 decoded-state) (nth 7 decoded-state)
(nth 10 decoded-state) (nth 12 decoded-state)
(nth 14 decoded-state))
(f-nor4 (nth 16 decoded-state) (nth 17 decoded-state)
(nth 22 decoded-state)
(nth 23 decoded-state)))
rn-b
(f$v-if-f-4 (f-or (nth 28 decoded-state)
(nth 29 decoded-state))
(fv-if (nth 30 decoded-state)
(f$v-inc4$v regs-address)
pc-reg))))
(append
(f$select-op-code
(f-nor4 (nth 2 decoded-state)
(f-or (nth 9 decoded-state)
(nth 21 decoded-state))
(f-or3 (nth 14 decoded-state)
(nth 17 decoded-state)
(nth 23 decoded-state))
(f-or4 (nth 0 decoded-state)
(nth 28 decoded-state)
(nth 29 decoded-state)
(nth 30 decoded-state)))
(f-nand (f-nand (f-or (nth 9 decoded-state)
(nth 21 decoded-state))
pre-dec-a)
(f-nand (f-or3 (nth 14 decoded-state)
(nth 17 decoded-state)
(nth 23 decoded-state))
pre-dec-b))
op-code)
(f$mpg
(cons
(f-or4 (nth 0 decoded-state)
(nth 28 decoded-state)
(nth 29 decoded-state)
(nth 30 decoded-state))
(cons
(f-or3 (nth 14 decoded-state)
(nth 17 decoded-state)
(nth 23 decoded-state))
(f$select-op-code
(f-nor4 (nth 2 decoded-state)
(f-or (nth 9 decoded-state)
(nth 21 decoded-state))
(f-or3 (nth 14 decoded-state)
(nth 17 decoded-state)
(nth 23 decoded-state))
(f-or4 (nth 0 decoded-state)
(nth 28 decoded-state)
(nth 29 decoded-state)
(nth 30 decoded-state)))
(f-nand
(f-nand (f-or (nth 9 decoded-state)
(nth 21 decoded-state))
pre-dec-a)
(f-nand (f-or3 (nth 14 decoded-state)
(nth 17 decoded-state)
(nth 23 decoded-state))
pre-dec-b))
op-code)))))))))))))))))))))))))
;;; Miscellaneous components of F$CV.
(defn f$v-if-f-4 (c a)
(list (f-and (f-not c) (car a))
(f-and (f-not c) (cadr a))
(f-and (f-not c) (caddr a))
(f-and (f-not c) (cadddr a))))
(defn f$v-inc4$v (a)
(let ((a0 (car a)) (a1 (cadr a)) (a2 (caddr a)) (a3 (cadddr a)))
(let ((a0n (f-not a0)) (a1n (f-not a1))
(a2n (f-not a2)) (a3n (f-not a3)))
(let ((c0 a0n) (c1 (f-nor a0n a1n)) (c2 (f-nor3 a0n a1n a2n)))
(list a0n
(f-xor a1n c0)
(f-equv a2n c1)
(f-equv a3n c2))))))
;;; ALU control signal decoding.
(defn f$select-op-code (select dec op)
(let ((op0 (car op))
(op1 (cadr op))
(op2 (caddr op))
(op3 (cadddr op)))
(list (f-nand select (f-not op0))
(f-and select op1)
(f-if select op2 dec)
(f-and select op3))))
(defn f$mpg (zsop)
(let ((zero (car zsop)) (swap (cadr zsop))
(op0 (caddr zsop)) (op1 (cadddr zsop))
(op2 (caddddr zsop)) (op3 (cadddddr zsop)))
(append (f$decode-gen zero swap op0 op1 op2 op3)
(append (f$decode-prop zero swap op0 op1 op2 op3)
(list (f$decode-mode op0 op1 op2 op3))))))
(defn f$decode-gen (zero swap op0 op1 op2 op3)
(let ((zero- (f-not zero)) (swap- (f-not swap))
(op0- (f-not op0)) (op1- (f-not op1))
(op2- (f-not op2)) (op3- (f-not op3)))
(let ((zero (f-not zero-)) (swap (f-not swap-))
(op0 (f-not op0-)) (op1 (f-not op1-))
(op2 (f-not op2-)) (op3 (f-not op3-)))
(list (f-nand3 (f-nand3 op0 op3 (f-xor op1 op2))
(f-nand3 op2 op3- (f-nand op1- swap-))
(f-nand3 op1 op2- op3-))
(f-nor (f-nand (f-nand4 op0 op1 op2- op3)
(f-nand3 op2 op3- (f-nand op1- swap-)))
zero)
(f-nor (f-nand3 (f-nand3 op0 op3 (f-xor op1 op2))
(f-nand3 op0 op1- op2)
(f-nand3 op1 op2- op3-))
zero)))))
(defn f$decode-prop (zero swap op0 op1 op2 op3)
(let ((zero- (f-not zero)) (swap- (f-not swap))
(op0- (f-not op0)) (op1- (f-not op1))
(op2- (f-not op2)) (op3- (f-not op3)))
(let ((zerop (f-not zero-)) (swap (f-not swap-))
(op0 (f-not op0-)) (op1 (f-not op1-))
(op2 (f-not op2-)) (op3 (f-not op3-)))
(list (f-nand3 (f-nand4 op0- op1- op2 op3)
(f-nand op1 op3-)
(f-nand3 op2- op3- swap))
(f-nor op2- (f-nor op3- (f-nor op0 op1-)))
(f-and (f-nand3 (f-nand op3 (f-equv op0 op1))
(f-nand op2- (f-nand swap op3-))
(f-nand4 op0 op1- op2 op3-))
zero-)))))
(defn f$decode-mode (op0 op1 op2 op3)
(f-nor (f-nor3 op0 op1 op2)
op3))
(defn f$carry-in-help (czop)
(let ((c (car czop)) (z (cadr czop))
(op0 (caddr czop)) (op1 (cadddr czop))
(op2 (caddddr czop)) (op3 (cadddddr czop)))
(let ((c- (f-not c)) (op0- (f-not op0))
(op1- (f-not op1)) (op2- (f-not op2))
(op3- (f-not op3)))
(let ((c (f-not c-))
(op0 (f-not op0-)) (op1 (f-not op1-))
(op2 (f-not op2-)) (op3 (f-not op3-)))
(f-or (f-nand3 (f-nand3 op1- op2- op3-)
(f-nand3 op0- op1- op2)
(f-nand3 op0 op1 op2))
(f-nand3 (f-nand op3 c)
(f-nand3 op0- op2- c)
(f-nand3 op0- op2 c-)))))))
;;; F$ENCODE-32 -- A 32-to-5 encoder, assuming a one-hot input vector, and
;;; assuming that inputs 26, 27 and 31 are never active.
(defn f$encode-32 (
s0 s1 s2 s3 s4 s5 s6 s7
s8 s9 s10 s11 s12 s13 s14 s15
s16 s17 s18 s19 s20 s21 s22 s23
s24 s25 s26 s27 s28 s29 s30 s31)
(let ((x0a (f-nor4 s1 s3 s5 s7))
(x0b (f-nor4 s9 s11 s13 s15))
(x0c (f-nor4 s17 s19 s21 s23))
(x0d (f-nor s25 s29))
(x1a (f-nor4 s2 s3 s6 s7))
(x1b (f-nor4 s10 s11 s14 s15))
(x1c (f-nor4 s18 s19 s22 s23))
(x1d (f-not s30))
(x2a (f-nor4 s4 s5 s6 s7))
(x2b (f-nor4 s12 s13 s14 s15))
(x2c (f-nor4 s20 s21 s22 s23))
(x2d (f-nor3 s28 s29 s30))
(x3a (f-nor4 s8 s9 s10 s11))
(x3b (f-nor4 s12 s13 s14 s15))
(x3c (f-nor s24 s25))
(x3d (f-nor3 s28 s29 s30))
(x4a (f-nor4 s16 s17 s18 s19))
(x4b (f-nor4 s20 s21 s22 s23))
(x4c (f-nor s24 s25))
(x4d (f-nor3 s28 s29 s30)))
(let ((x0 (f-nand4 x0a x0b x0c x0d))
(x1 (f-nand4 x1a x1b x1c x1d))
(x2 (f-nand4 x2a x2b x2c x2d))
(x3 (f-nand4 x3a x3b x3c x3d))
(x4 (f-nand4 x4a x4b x4c x4d)))
(list x0 x1 x2 x3 x4))))
;;;++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
;;;
;;; MEMORY MODEL
;;;
;;;++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
;;; This is a model of a generic memory for the FM9001. Besides the
;;; state component, the memory takes as input a STROBE (active low), a
;;; read/write line (low to write), and address and data lines.
;;;
;;; The state component consists of the memory contents, a memory control
;;; state (see below), a "clock" (see below), a "count" used for DTACK
;;; scheduling, a flag indicating that DTACK has been asserted, the last
;;; value of RW- and the last address and data inputs.
;;;
;;; Address lines, and data lines on a write, must be stable for one cycle
;;; before the strobe is activated, and one cycle after the strobe is
;;; released. On a write, the same setup/hold constraints also must be met
;;; by the low pulse on RW-.
;;;
;;; Memory control states:
;;;
;;; 0 -- The quiet state.
;;; 1 -- Read wait.
;;; 2 -- Write wait.
;;; x -- Error.
;;;
;;; The "clock" is an oracle that specifies the wait for DTACK. Whenever the
;;; STROBE is activated, then (CAR clock) is the number of memory delays for
;;; this memory operation, and the new "clock" becomes (CDR clock). For
;;; simulation purposes we normally set this to 0 to provide minimum delays
;;; since both the CAR and CDR of 0 are 0.
(defn next-memory-state (state strobe- rw- address data)
(let ((mem (car state))
(cntl (cadr state))
(clock (caddr state))
(count (cadddr state))
(dtack-asserted (caddddr state))
(last-rw- (cadddddr state))
(last-address (caddddddr state))
(last-data (cadddddddr state)))
(let ((rw-address-data
(list (threefix rw-)
(v-threefix address)
(if (boolp rw-)
(if rw-
(v-threefix last-data)
(v-threefix data))
(make-list (length data) (x))))))
(let
((reset (list* mem 0 clock 0 t rw-address-data))
(start-read (list* mem 1 (cdr clock)
(sub1 (car clock)) (zerop (car clock))
rw-address-data))
(start-write (list* mem 2 (cdr clock)
(sub1 (car clock)) (zerop (car clock))
rw-address-data))
(read-error (list* mem 3 (cdr clock)
(sub1 (car clock)) (zerop (car clock))
rw-address-data))
(write-error (list* (constant-ram mem (make-list 32 (x)))
3 (cdr clock)
(sub1 (car clock)) (zerop (car clock))
rw-address-data))
(reset-error (list* (constant-ram mem (make-list 32 (x)))
0 clock 0 t
rw-address-data))
(finish-write (list* (write-mem address mem data) 0 clock 0 t
rw-address-data))
(read-wait (list* mem 1 clock (sub1 count) (zerop count)
rw-address-data))
(write-wait (list* mem 2 clock (sub1 count) (zerop count)
rw-address-data))
(error-wait (list* mem 3 clock (sub1 count) (zerop count)
rw-address-data)))
(let ((bvp-equal-address (and (bvp address)
(bvp last-address)
(equal address last-address)))
(bvp-equal-data (and (bvp data)
(bvp last-data)
(equal data last-data))))
(if (and (boolp strobe-) (boolp rw-))
(case cntl
(0 (if strobe-
reset
(if rw-
(if (and last-rw- (boolp last-rw-))
(if bvp-equal-address
start-read
read-error)
write-error)
(if (and (not last-rw-) ;Subtle
bvp-equal-address
bvp-equal-data)
start-write
write-error))))
(1 (if strobe-
(if rw-
reset
reset-error)
(if rw-
(if bvp-equal-address
read-wait
read-error)
write-error)))
(2 (if strobe-
(if rw-
reset-error
(if (and bvp-equal-address
bvp-equal-data
(zerop count))
finish-write
reset-error))
(if rw-
write-error
(if (and bvp-equal-address
bvp-equal-data)
write-wait
write-error))))
(otherwise (if strobe-
(if rw-
reset
reset-error)
(if rw-
error-wait
write-error))))
reset-error))))))
(defn memory-value (state strobe- rw- address data)
(let ((mem (car state))
(cntl (cadr state))
(clock (caddr state))
(count (cadddr state))
(dtack-asserted (caddddr state))
(last-rw- (cadddddr state))
(last-address (caddddddr state))
(last-data (cadddddddr state)))
(let ((x-vector (make-list (length data) (x)))
(z-vector (make-list (length data) (z))))
(let ((unknown (cons (x) x-vector))
(default (cons (x) z-vector))
(read-wait (cons t x-vector))
(write-wait (cons t z-vector))
(dtack-0 (cons (if* (zerop (car clock)) f t)
(if* rw- x-vector z-vector)))
(dtack-read (cons f
(if* dtack-asserted
(read-mem address mem)
x-vector)))
(dtack-read-default (cons f x-vector))
(dtack-write-default (cons f z-vector)))
(let ((bvp-equal-address (and* (equal address last-address)
(and* (bvp address)
(bvp last-address)))))
(if* (and* (boolp strobe-) (boolp rw-))
(case cntl
(0 (if* strobe-
default
dtack-0))
(1 (if* strobe-
default
(if* rw-
(if* bvp-equal-address
(if* (zerop count)
dtack-read
read-wait)
(if* (zerop count)
dtack-read-default
read-wait))
(if* (zerop count)
dtack-write-default
write-wait))))
(2 (if* strobe-
default
(if* (zerop count)
dtack-write-default
write-wait)))
(otherwise (if* strobe-
default
(if* rw-
(if* (zerop count)
dtack-read-default
read-wait)
(if* (zerop count)
dtack-write-default
write-wait)))))
unknown))))))
;;; CONSTANT-RAM -- Sets all RAM cells to VALUE.
(defn constant-ram (mem value)
(if (ramp mem)
(ram value)
(if (nlistp mem)
mem
(cons (constant-ram (car mem) value)
(constant-ram (cdr mem) value)))))
;;;++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
;;;
;;; Four-valued vector functions.
;;;
;;;++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
;;; V-THREEFIX -- Normalize to a 4-valued vector. Also a vector buffer.
(defn v-threefix (v)
(if (nlistp v)
nil
(cons (threefix (car v))
(v-threefix (cdr v)))))
;;; FV-IF -- Vector multiplexor.
(defn fv-if (c a b)
(if (nlistp a)
nil
(cons (f-if c (car a) (car b))
(fv-if c (cdr a) (cdr b)))))
;;; FV-OR -- Vector OR.
(defn fv-or (a b)
(if (nlistp a)
nil
(cons (f-or (car a) (car b))
(fv-or (cdr a) (cdr b)))))
;;; FV-XOR -- Vector XOR.
(defn fv-xor (a b)
(if (nlistp a)
nil
(cons (f-xor (car a) (car b))
(fv-xor (cdr a) (cdr b)))))
;;; V-PULLUP -- Pullup vector.
(defn v-pullup (v)
(if (nlistp v)
nil
(cons (f-pullup (car v))
(v-pullup (cdr v)))))
;;; VFT-BUF -- Vector tristate buffer.
(defn vft-buf (c a)
(if (nlistp a)
nil
(cons (ft-buf c (car a))
(vft-buf c (cdr a)))))
;;; V-WIRE -- Vector "wire".
(defn v-wire (a b)
(if (nlistp a)
nil
(cons (ft-wire (car a) (car b))
(v-wire (cdr a) (cdr b)))))
;;;++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
;;;
;;; Four-valued gate-level functions.
;;;
;;;++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
(defn f$ao2 (a b c d) (f-nor (f-and a b) (f-and c d)))
(defn f-buf (a) (threefix a))
(defn f-nand (a b) (f-not (f-and a b)))
(defn f-nand3 (a b c) (f-not (f-and a (f-and b c))))
(defn f-nand4 (a b c d) (f-not (f-and a (f-and b (f-and c d)))))
(defn f-nand5 (a b c d e) (f-not (f-and a (f-and b (f-and c (f-and d e))))))
(defn f-nand6 (a b c d e g)
(f-not (f-and a (f-and b (f-and c (f-and d (f-and e g)))))))
(defn f-nand8 (a b c d e g h i)
(f-not
(f-and a (f-and b (f-and c (f-and d (f-and e (f-and g (f-and h i)))))))))
(defn f-and3 (a b c) (f-and a (f-and b c)))
(defn f-and4 (a b c d) (f-and a (f-and b (f-and c d))))
(defn f-and (a b)
(if (or (equal a f) (equal b f))
f
(if (and (equal a t) (equal b t))
t
(x))))
(defn f-nor (a b) (f-not (f-or a b)))
(defn f-nor3 (a b c) (f-not (f-or a (f-or b c))))
(defn f-nor4 (a b c d) (f-not (f-or a (f-or b (f-or c d)))))
(defn f-nor5 (a b c d e) (f-not (f-or a (f-or b (f-or c (f-or d e))))))
(defn f-nor6 (a b c d e g)
(f-not (f-or a (f-or b (f-or c (f-or d (f-or e g)))))))
(defn f-nor8 (a b c d e g h i)
(f-not
(f-or a (f-or b (f-or c (f-or d (f-or e (f-or g (f-or h i)))))))))
(defn f-or3 (a b c) (f-or a (f-or b c)))
(defn f-or4 (a b c d) (f-or a (f-or b (f-or c d))))
(defn f-or (a b)
(if (or (equal a t) (equal b t))
t
(if (and (equal a f) (equal b f))
f
(x))))
(defn f-equv3 (a b c) (f-equv a (f-xor b c)))
(defn f-equv (a b)
(if (equal a t)
(threefix b)
(if (equal a f)
(f-not b)
(x))))
(defn f-xor3 (a b c) (f-xor a (f-xor b c)))
(defn f-xor (a b)
(if (equal a t)
(f-not b)
(if (equal a f)
(threefix b)
(x))))
(defn f-if (c a b)
(if (equal c t)
(threefix a)
(if (equal c f)
(threefix b)
(x))))
(defn f-not (a)
(if (boolp a)
(not a)
(x)))
(defn ft-buf (c a)
(if (equal c t)
(threefix a)
(if (equal c f)
(z)
(x))))
(defn ft-wire (a b)
(if (equal a b)
(fourfix a)
(if (equal a (z))
(fourfix b)
(if (equal b (z))
(fourfix a)
(x)))))
(defn f-pullup (a)
(if (equal a (z))
t
(threefix a)))
;;; "Fix" functions.
(defn threefix (x)
(if (boolp x)
x
(x)))
(defn fourfix (x)
(if (fourp x)
x
(x)))
;;; BVP, BOOLP, THREEP, FOURP
(defn bvp (x)
(if (nlistp x)
(equal x nil)
(and (boolp (car x))
(bvp (cdr x)))))
(defn boolp (x)
(or (equal x t) (equal x f)))
(defn threep (x)
(or (equal x t) (equal x f) (equal x (x))))
(defn fourp (x)
(or (equal x t) (equal f x) (equal x (x)) (equal x (z))))
;;; X and Z
(add-shell x () xp ())
(add-shell z () zp ())
;;; ID -- The "renaming" gate.
(defn id (x) x)
;;; Power and ground
(defn vss () f)
(defn vdd () t)
;;;++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
;;;
;;; TREE FUNCTIONS
;;;
;;;++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
;;; TFIRSTN, TRESTN -- Divide a linear list based on a tree.
(defn tfirstn (list tree)
(firstn (tree-size (car tree)) list))
(defn trestn (list tree)
(restn (tree-size (car tree)) list))
;;; TREE-SIZE -- Number of leaves in a tree.
(defn tree-size (tree)
(if (nlistp tree)
1
(plus (tree-size (car tree))
(tree-size (cdr tree)))))
;;; TREE-HEIGHT
(defn tree-height (tree)
(if (nlistp tree)
1
(add1 (max (tree-height (car tree))
(tree-height (cdr tree))))))
;;; MAKE-TREE n -- Makes a tree of size N.
(defn make-tree (n)
(if (zerop n)
0
(if (equal n 1)
0
(cons (make-tree (quotient n 2))
(make-tree (difference n (quotient n 2)))))))
;;; These 3 lemmas are necessary to prove the admissibility of MAKE-TREE.
(prove-lemma quotient-lessp (rewrite)
(implies
(and (lessp 1 base)
(not (zerop n)))
(lessp (quotient n base)
n)))
(prove-lemma leq-lessp-difference (rewrite)
(implies
(and (leq x y)
(not (zerop z))
(not (zerop y)))
(equal (lessp (difference x z) y)
t))
;;Hint
((enable difference)))
(prove-lemma zerop-quotient (rewrite)
(equal (equal (quotient n m) 0)
(or (zerop n) (zerop m) (lessp n m))))
;;;++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
;;;
;;; *-CONNECTIVES
;;;
;;; These connectives are added to give us more control over case splitting.
;;;
;;;++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
(defn or* (a b) (if* a t (if* b t f)))
(defn and* (a b) (if* a (if* b t f) f))
(defn not* (a) (if* a f t))
(defn if* (a b c) (if a b c))
;;; Closes #. above.
)))