;;;  Copyright (C) 1990-1994 Computational Logic, Inc.  All Rights
;;;  Reserved.  See the file LICENSE in this directory for the
;;;  complete license agreement.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; 
;;;     DUAL-EVAL-SPEC.EVENTS
;;;    
;;;    Bishop C. Brock & Warren A. Hunt, Jr.
;;;    
;;;    This file contains an almost minimal set of events necessary to define
;;;    the DUAL-EVAL interpreter.  The definitions are presented in a
;;;    top-down fashion.  Many of the definitions required by the functions
;;;    defined here appear in the file "rtl-level-spec.events", in
;;;    particular, the primitive functional definitions appear there.
;;;    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 '(

;;;++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
;;;
;;;    DUAL-EVAL and related multi-cycle interpreters.
;;;
;;;++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

;;;   SIMULATE -- Runs DUAL-EVAL over time.

(defn simulate (fn inputs state netlist)
  (if (nlistp inputs)
      nil
    (let ((value (dual-eval 0 fn (car inputs) state netlist))
	  (new-state (dual-eval 2 fn (car inputs) state netlist)))
      (cons (list value new-state)
	    (simulate fn (cdr inputs) new-state netlist)))))

;;;  SIMULATE-DUAL-EVAL-2 -- Returns the final state after a number of
;;;  simulation steps. 

(defn simulate-dual-eval-2 (module inputs state netlist n)
  (if (zerop n)
      state
    (simulate-dual-eval-2
     module
     (cdr inputs)
     (dual-eval 2 module (car inputs) state netlist)
     netlist
     (sub1 n))))

;;;  The DUAL-EVAL interpreter.

(defn dual-eval (flag x0 x1 x2 netlist)
  (case flag

    ;;  New value of a form.

    (0 (let ((fn x0)
	     (args x1)
	     (state x2))
	 (if (primp fn)
	     (dual-apply-value fn args state)
	
	   (let ((module (lookup-module fn netlist)))
	     (if (listp module)
		 (let ((inputs  (module-inputs module))
		       (outputs (module-outputs module))
		       (occurrences (module-occurrences module))
		       (statenames (module-statenames module)))
		   (collect-value
		    outputs
		    (dual-eval 1
			       occurrences
			       (pairlist inputs args)
			       (pairstates statenames state)
			       (delete-module fn netlist))))
	       f)))))

    ;;  Create the new bindings of a body.

    (1 (let ((body x0)
	     (bindings x1)
	     (state-bindings x2))
	 
	 (if (listp body)
	     (let ((occurrence (car body)))
	       (let ((occ-name (occ-name occurrence))
		     (outputs (occ-outputs occurrence))
		     (fn (occ-function occurrence))
		     (inputs (occ-inputs occurrence)))
		 (dual-eval
		  1
		  (cdr body)
		  (append
		   (pairlist outputs
			     (dual-eval 0
					fn
					(collect-value inputs bindings)
					(value occ-name state-bindings)
					netlist))
		   bindings)
		  state-bindings
		  netlist)))
	   bindings)))

    ;;  New state of a form.

    (2 (let ((fn x0)
	     (args x1)
	     (state x2))
	 (if (primp fn)
	     (dual-apply-state fn args state)
	
	   (let ((module (lookup-module fn netlist)))
	     (if (listp module)
		 (let ((inputs  (module-inputs module))
		       (outputs (module-outputs module))
		       (occurrences (module-occurrences module))
		       (statenames (module-statenames module)))
		   (collect-states
		    statenames
		    (dual-eval 3
			       occurrences
			       (dual-eval 1
					  occurrences
					  (pairlist inputs args)
					  (pairstates statenames state)
					  (delete-module fn netlist))
			       (pairstates statenames state)
			       (delete-module fn netlist))))
	       f)))))
    
    ;;  New state of a body.

    (3 (let ((body x0)
	     (bindings x1)
	     (state-bindings x2))
	 
	 (if (listp body)
	     (let ((occurrence (car body)))
	       (let ((occ-name (occ-name occurrence))
		     (outputs (occ-outputs occurrence))
		     (fn (occ-function occurrence))
		     (inputs (occ-inputs occurrence)))
		 (cons
		  (cons occ-name
			(dual-eval 2
				   fn
				   (collect-value inputs bindings)
				   (value occ-name state-bindings)
				   netlist))
		  (dual-eval 3
			     (cdr body)
			     bindings
			     state-bindings
			     netlist))))
	   nil)))

    (otherwise f))

  ((ord-lessp (cons (add1 (count netlist)) (count x0)))))

;;;   Module and Occurrence Destructors

(defn module-name        (module) (car module))
(defn module-inputs      (module) (cadr module))
(defn module-outputs     (module) (caddr module))
(defn module-occurrences (module) (cadddr module))
(defn module-statenames  (module) (caddddr module))
(defn module-annotation  (module) (cadddddr module))


(defn occ-name       (occurrence) (car occurrence))
(defn occ-outputs    (occurrence) (cadr occurrence))
(defn occ-function   (occurrence) (caddr occurrence))
(defn occ-inputs     (occurrence) (cadddr occurrence))
(defn occ-annotation (occurrence) (caddddr occurrence))

;;;++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
;;;
;;;    Evaluation
;;;
;;;++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

(defn dual-apply-value (fn args state)
  (let ((input-names (primp2 fn 'inputs))
	(state-names (primp2 fn 'states))
	(module-outs (primp2 fn 'results)))
    (let ((alist (append (pairlist input-names args)
			 (pairstates state-names state))))
      (eval$ t module-outs alist))))

(defn dual-apply-state (fn args state)
  (let ((input-names (primp2 fn 'inputs))
	(state-names (primp2 fn 'states))
	(new-states  (primp2 fn 'new-states)))
    (let ((alist (append (pairlist input-names args)
			 (pairstates state-names state))))
      (eval$ t new-states alist))))

(defn primp2 (fn name)
  (cdr (primp-lookup fn name)))

(defn primp-lookup (fn name)
  (lookup-module name (cdr (primp fn))))

(defn primp (fn)
  (lookup-module fn (primp-database)))

;;;++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
;;;
;;;    Netlist accessors
;;;
;;;++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

;;  To prove the admissibility of DUAL-EVAL.

(prove-lemma delete-module-lookup-module-count (rewrite)
  (implies
   (lookup-module name netlist)
   (lessp (count (delete-module name netlist))
	  (count netlist)))
  ;;Hint
  ((enable lookup-module delete-module)))

(defn lookup-module (name netlist)
  (if (nlistp netlist)
      f
    (if (and (listp (car netlist))
	     (equal (caar netlist) name))
	(car netlist)
      (lookup-module name (cdr netlist)))))

(defn delete-module (name netlist)
  (if (nlistp netlist)
      netlist
    (if (and (listp (car netlist))
	     (equal (caar netlist) name))
	(cdr netlist)
      (cons (car netlist) (delete-module name (cdr netlist))))))

;;;++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
;;;
;;;    ALIST access and creation.
;;;
;;;++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

;;;   PAIRSTATES and COLLECT-STATES

(defn pairstates (statenames state)
  (if (or (listp statenames)
	  (equal statenames nil))
      (pairlist statenames state)
    (list (cons statenames state))))

(defn collect-states (statenames state-bindings)
  (if (or (listp statenames)
	  (equal statenames nil))
      (collect-value statenames state-bindings)
    (value statenames state-bindings)))


;;;  VALUE and COLLECT-VALUE

(defn collect-value (args alist)
  (if (nlistp args)
      nil
    (cons (value (car args) alist)
	  (collect-value (cdr args) alist))))

(defn value (name alist)
  (if (nlistp alist)
      0
    (if (listp (car alist))
	(if (equal (caar alist) name)
	    (cdar alist)
	  (value name (cdr alist)))
      (value name (cdr alist)))))

;;;++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
;;;
;;;    PRIMITIVE-DATABASE
;;;
;;;    This is the entire primitive database, as stored in the file
;;;    "primp-database.lisp".  We have included the entire database
;;;    here for completeness, even though DUAL-EVAL only uses a small
;;;    portion of the fields of the database.
;;;
;;;++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

(eval `
(defn primp-database () ',common-lisp-primp-database))

;;;  The database.

(defconstant
  common-lisp-primp-database
  `((ao2
     (delays        ((263 737) (83 392)))
     (drives        10)
     (input-types   boolp boolp boolp boolp)
     (inputs        a b c d)
     (loadings      1 1 1 1)
     (lsi-name      . ao2)
     (out-depends   (a b c d))
     (output-types  boolp)
     (outputs       z)
     (results       . ,(cons-up '((f-nor (f-and a b) (f-and c d)))))

     (gates         . 2)
     (primitives    . 1)
     (transistors   . 8))


    (ao4
     (delays        ((260 895) (82 311)))
     (drives        10)
     (input-types   boolp boolp boolp boolp)
     (inputs        a b c d)
     (loadings      1 1 1 1)
     (lsi-name      . ao4)
     (out-depends   (a b c d))
     (output-types  boolp)
     (outputs       z)
     (results       . ,(cons-up '((f-nand (f-or a b) (f-or c d)))))

     (gates         . 2)
     (primitives    . 1)
     (transistors   . 8))


    (ao6
     (delays        ((260 745) (82 202)))
     (drives        10)
     (input-types   boolp boolp boolp)
     (inputs        a b c)
     (loadings      1 1 1)
     (lsi-name      . ao6)
     (out-depends   (a b c))
     (output-types  boolp)
     (outputs       z)
     (results       . ,(cons-up '((f-nor (f-and a b) c))))

     (gates         . 2)
     (primitives    . 1)
     (transistors   . 6))


    (ao7
     (delays        ((261 486) (83 293)))
     (drives        10)
     (input-types   boolp boolp boolp)
     (inputs        a b c)
     (loadings      1 1 1)
     (lsi-name      . ao7)
     (out-depends   (a b c))
     (output-types  boolp)
     (outputs       z)
     (results       . ,(cons-up '((f-nand (f-or a b) c))))

     (gates         . 2)
     (primitives    . 1)
     (transistors   . 6))

    (b-and
     (delays        ((144 422) (54 707)))
     (drives        10)
     (input-types   boolp boolp)
     (inputs        a b)
     (loadings      1 1)
     (lsi-name      . an2)
     (out-depends   (a b))
     (output-types  boolp)
     (outputs       z)
     (results       . ,(cons-up '((f-and a b))))

     (gates         . 2)
     (primitives    . 1)
     (transistors   . 6))


    (b-and3
     (delays        ((146 663) (58 809)))
     (drives        10)
     (input-types   boolp boolp boolp)
     (inputs        a b c)
     (loadings      1 1 1)
     (lsi-name      . an3)
     (out-depends   (a b c))
     (output-types  boolp)
     (outputs       z)
     (results       . ,(cons-up '((f-and3 a b c))))

     (gates         . 2)
     (primitives    . 1)
     (transistors   . 8))


    (b-and4
     (delays        ((149 934) (60 870)))
     (drives        10)
     (input-types   boolp boolp boolp boolp)
     (inputs        a b c d)
     (loadings      1 1 1 1)
     (lsi-name      . an4)
     (out-depends   (a b c d))
     (output-types  boolp)
     (outputs       z)
     (results       . ,(cons-up '((f-and4 a b c d))))

     (gates         . 3)
     (primitives    . 1)
     (transistors   . 10))


    (b-equv
     (delays        ((145 742) (67 973)))
     (drives        10)
     (input-types   boolp boolp)
     (inputs        a b)
     (loadings      1 2)
     (lsi-name      . en)
     (out-depends   (a b))
     (output-types  boolp)
     (outputs       z)
     (results       . ,(cons-up '((f-equv a b))))

     (gates         . 3)
     (primitives    . 1)
     (transistors   . 12))


    (b-equv3
     (delays        ((151 1806) (79 1580)))
     (drives        10)
     (input-types   boolp boolp boolp)
     (inputs        a b c)
     (loadings      1 3 2)
     (lsi-name      . en3)
     (out-depends   (a b c))
     (output-types  boolp)
     (outputs       z)
     (results       . ,(cons-up '((f-equv3 a b c))))

     (gates         . 7)
     (primitives    . 1)
     (transistors   . 22))


    (b-if
     (delays        ((70 775) (60 1040)))
     (drives        10)
     (input-types   boolp boolp boolp)
     (inputs        s a b)
     (loadings      2 1 1)
     (lsi-name      . (mux21h b a s))	; Note input reordering
     (out-depends   (a b s))
     (output-types  boolp)
     (outputs       z)
     (results       . ,(cons-up '((f-if s a b))))

     (gates         . 4)
     (primitives    . 1)
     (transistors   . 12))


    (b-nand
     (delays        ((141 420) (82 161)))
     (drives        10)
     (input-types   boolp boolp)
     (inputs        a b)
     (loadings      1 1)
     (lsi-name      . nd2)
     (out-depends   (a b))
     (output-types  boolp)
     (outputs       z)
     (results       . ,(cons-up '((f-nand a b))))

     (gates         . 1)
     (primitives    . 1)
     (transistors   . 4))


    (b-nand3
     (delays        ((142 537) (109 322)))
     (drives        10)
     (input-types   boolp boolp boolp)
     (inputs        a b c)
     (loadings      1 1 1)
     (lsi-name      . nd3)
     (out-depends   (a b c))
     (output-types  boolp)
     (outputs       z)
     (results       . ,(cons-up '((f-nand3 a b c))))

     (gates         . 2)
     (primitives    . 1)
     (transistors   . 6))


    (b-nand4
     (delays        ((144 588) (144 418)))
     (drives        10)
     (input-types   boolp boolp boolp boolp)
     (inputs        a b c d)
     (loadings      1 1 1 1)
     (lsi-name      . nd4)
     (out-depends   (a b c d))
     (output-types  boolp)
     (outputs       z)
     (results       . ,(cons-up '((f-nand4 a b c d))))

     (gates         . 2)
     (primitives    . 1)
     (transistors   . 8))


    (b-nand5
     (delays        ((144 1002) (59 1120)))
     (drives        10)
     (input-types   boolp boolp boolp boolp boolp)
     (inputs        a b c d e)
     (loadings      1 1 1 1 1)
     (lsi-name      . nd5)
     (out-depends   (a b c d e))
     (output-types  boolp)
     (outputs       z)
     (results       . ,(cons-up '((f-nand5 a b c d e))))

     (gates         . 4)
     (primitives    . 1)
     (transistors   . 16))


    (b-nand6
     (delays        ((144 982) (59 1090)))
     (drives        10)
     (input-types   boolp boolp boolp boolp boolp boolp)
     (inputs        a b c d e g)
     (loadings      1 1 1 1 1 1)
     (lsi-name      . nd6)
     (out-depends   (a b c d e g))
     (output-types  boolp)
     (outputs       z)
     (results       . ,(cons-up '((f-nand6 a b c d e g))))

     (gates         . 5)
     (primitives    . 1)
     (transistors   . 18))


    (b-nand8
     (delays        ((144 1042) (60 1360)))
     (drives        10)
     (input-types   boolp boolp boolp boolp boolp boolp boolp boolp)
     (inputs        a b c d e g h i)
     (loadings      1 1 1 1 1 1 1 1)
     (lsi-name      . nd8)
     (out-depends   (a b c d e g h i))
     (output-types  boolp)
     (outputs       z)
     (results       . ,(cons-up '((f-nand8 a b c d e g h i))))

     (gates         . 6)
     (primitives    . 1)
     (transistors   . 22))


    (b-nbuf
     (delays        ((142 447) (57 213))
		    ((143 302) (52 366)))
     (drives        9 10)
     (input-types   boolp)
     (inputs        a)
     (loadings      1)
     (lsi-name      . ivda)
     (out-depends   (a) (a))
     (output-types  boolp boolp)
     (outputs       y z)
     (results       . ,(cons-up '((f-not a) (f-buf a))))

     (gates         . 1)
     (primitives    . 1)
     (transistors   . 4))


    (b-nor
     (delays        ((260 460) (59 170)))
     (drives        10)
     (input-types   boolp boolp)
     (inputs        a b)
     (loadings      1 1)
     (lsi-name      . nr2)
     (out-depends   (a b))
     (output-types  boolp)
     (outputs       z)
     (results       . ,(cons-up '((f-nor a b))))

     (gates         . 1)
     (primitives    . 1)
     (transistors   . 4))


    (b-nor3
     (delays        ((384 798) (59 224)))
     (drives        10)
     (input-types   boolp boolp boolp)
     (inputs        a b c)
     (loadings      1 1 1)
     (lsi-name      . nr3)
     (out-depends   (a b c))
     (output-types  boolp)
     (outputs       z)
     (results       . ,(cons-up '((f-nor3 a b c))))

     (gates         . 2)
     (primitives    . 1)
     (transistors   . 6))


    (b-nor4
     (delays        ((510 1072) (59 225)))
     (drives        10)
     (input-types   boolp boolp boolp boolp)
     (inputs        a b c d)
     (loadings      1 1 1 1)
     (lsi-name      . nr4)
     (out-depends   (a b c d))
     (output-types  boolp)
     (outputs       z)
     (results       . ,(cons-up '((f-nor4 a b c d))))

     (gates         . 2)
     (primitives    . 1)
     (transistors   . 8))


    (b-nor5
     (delays        ((145 1493) (55 767)))
     (drives        10)
     (input-types   boolp boolp boolp boolp boolp)
     (inputs        a b c d e)
     (loadings      1 1 1 1 1)
     (lsi-name      . nr5)
     (out-depends   (a b c d e))
     (output-types  boolp)
     (outputs       z)
     (results       . ,(cons-up '((f-nor5 a b c d e))))

     (gates         . 4)
     (primitives    . 1)
     (transistors   . 16))


    (b-nor6
     (delays        ((146 1593) (55 807)))
     (drives        10)
     (input-types   boolp boolp boolp boolp boolp boolp)
     (inputs        a b c d e g)
     (loadings      1 1 1 1 1 1)
     (lsi-name      . nr6)
     (out-depends   (a b c d e g))
     (output-types  boolp)
     (outputs       z)
     (results       . ,(cons-up '((f-nor6 a b c d e g))))

     (gates         . 5)
     (primitives    . 1)
     (transistors   . 18))


    (b-nor8
     (delays        ((146 1853) (54 767)))
     (drives        10)
     (input-types   boolp boolp boolp boolp boolp boolp boolp boolp)
     (inputs        a b c d e g h i)
     (loadings      1 1 1 1 1 1 1 1)
     (lsi-name      . nr8)
     (out-depends   (a b c d e g h i))
     (output-types  boolp)
     (outputs       z)
     (results       . ,(cons-up '((f-nor8 a b c d e g h i))))

     (gates         . 6)
     (primitives    . 1)
     (transistors   . 22))


    (b-not
     (delays        ((70 235) (57 198)))
     (drives        10)       
     (input-types   boolp)
     (inputs        a)
     (loadings      2)
     (lsi-name      . iva)
     (out-depends   (a))
     (output-types  boolp)
     (outputs       z)
     (results       . ,(cons-up '((f-not a))))

     (gates         . 1)
     (primitives    . 1)
     (transistors   . 3))


    (b-not-b4ip
     (delays        ((17 333) (12 124)))
     (drives        128)       
     (input-types   boolp)
     (inputs        a)
     (loadings      8)
     (lsi-name      . b4ip)
     (out-depends   (a))
     (output-types  boolp)
     (outputs       z)
     (results       . ,(cons-up '((f-not a))))

     (gates         . 4)
     (primitives    . 1)
     (transistors   . 12))


    (b-not-ivap
     (delays        ((38 208) (35 126)))
     (drives        20)       
     (input-types   boolp)
     (inputs        a)
     (loadings      3)
     (lsi-name      . ivap)
     (out-depends   (a))
     (output-types  boolp)
     (outputs       z)
     (results       . ,(cons-up '((f-not a))))

     (gates         . 2)
     (primitives    . 1)
     (transistors   . 6))


    (b-or
     (delays        ((143 332) (58 819)))
     (drives        10)
     (input-types   boolp boolp)
     (inputs        a b)
     (loadings      1 1)
     (lsi-name      . or2)
     (out-depends   (a b))
     (output-types  boolp)
     (outputs       z)
     (results       . ,(cons-up '((f-or a b))))

     (gates         . 2)
     (primitives    . 1)
     (transistors   . 6))


    (b-or3
     (delays        ((144 422) (70 1185)))
     (drives        10)
     (input-types   boolp boolp boolp)
     (inputs        a b c)
     (loadings      1 1 1)
     (lsi-name      . or3)
     (out-depends   (a b c))
     (output-types  boolp)
     (outputs       z)
     (results       . ,(cons-up '((f-or3 a b c))))

     (gates         . 2)
     (primitives    . 1)
     (transistors   . 8))


    (b-or4
     (delays        ((143 352) (78 1329)))
     (drives        10)
     (input-types   boolp boolp boolp boolp)
     (inputs        a b c d)
     (loadings      1 1 1 1)
     (lsi-name      . or4)
     (out-depends   (a b c d))
     (output-types  boolp)
     (outputs       z)
     (results       . ,(cons-up '((f-or4 a b c d))))

     (gates         . 3)
     (primitives    . 1)
     (transistors   . 10))


    (b-xor
     (delays        ((145 742) (67 973)))
     (drives        10)
     (input-types   boolp boolp)
     (inputs        a b)
     (loadings      1 2)
     (lsi-name      . eo)
     (out-depends   (a b))
     (output-types  boolp)
     (outputs       z)
     (results       . ,(cons-up '((f-xor a b))))

     (gates         . 3)
     (primitives    . 1)
     (transistors   . 12))


    (b-xor3
     (delays        ((151 1806) (79 1580)))
     (drives        10)
     (input-types   boolp boolp boolp)
     (inputs        a b c)
     (loadings      1 3 2)
     (lsi-name      . eo3)
     (out-depends   (a b c))
     (output-types  boolp)
     (outputs       z)
     (results       . ,(cons-up '((f-xor3 a b c))))

     (gates         . 7)
     (primitives    . 1)
     (transistors   . 22))


    (del2
     (delays        ((70 2035) (38 2199)))
     (drives        10)       
     (input-types   boolp)
     (inputs        a)
     (loadings      1)
     (lsi-name      . del2)
     (out-depends   (a))
     (output-types  boolp)
     (outputs       z)
     (results       . ,(cons-up '((f-buf a))))

     (gates         . 4)
     (primitives    . 1)
     (transistors   . 16))


    (del4
     (delays        ((73 4017) (38 4179)))
     (drives        10)       
     (input-types   boolp)
     (inputs        a)
     (loadings      1)
     (lsi-name      . del4)
     (out-depends   (a))
     (output-types  boolp)
     (outputs       z)
     (results       . ,(cons-up '((f-buf a))))

     (gates         . 7)
     (primitives    . 1)
     (transistors   . 28))


    (del10
     (delays        ((60 10530) (49 10424)))
     (drives        10)       
     (input-types   boolp)
     (inputs        a)
     (loadings      1)
     (lsi-name      . del10)
     (out-depends   (a))
     (output-types  boolp)
     (outputs       z)
     (results       . ,(cons-up '((f-buf a))))

     (gates         . 19)
     (primitives    . 1)
     (transistors   . 76))



    (procmon				
     ;; Delay slopes are from MUX21H.  LSI flyer says delay through OR's is
     ;; at least twice the delay through the inverters, so intercepts are
     ;; approximately:    2*(30-IV's + ND2 + EN + MUX21H) ~= 25000.
     ;; (30*IV + NR2 + 90*(NR3+IVAP) + EN + MUX21H gives a much larger number.)
     (delays        ((70 25000) (60 25000)))
     (drives        10)
     (input-types   parametric parametric parametric parametric)
     (inputs        a e s n)
     (loadings      2 2 2 1)
     (lsi-name      . procmon)
     (out-depends   (a e s n))
     (output-types  parametric)
     (outputs       z)
     (results       . (cons (f-if s
				  (f-if e
					(f-if a '*1*false '*1*false)
					a)
				  n)
			    'nil))

     (gates         . 100)
     (primitives    . 1)
     (transistors   . 400))

    (dp-ram-16x32
     ;; delays: Slopes are one fourth of ND2 (b-nand) slopes.
     ;;         Intercepts came from LSI flyer.
     (delays        . ,(make-list 32
				  :initial-element
				  '((35 7500) (21 7500))))
     (drives        . ,(make-list 32 :initial-element 2))
     (input-types   boolp boolp boolp boolp
		    boolp boolp boolp boolp
		    level
		    boolp boolp boolp boolp boolp boolp boolp boolp
		    boolp boolp boolp boolp boolp boolp boolp boolp
		    boolp boolp boolp boolp boolp boolp boolp boolp
		    boolp boolp boolp boolp boolp boolp boolp boolp)
     (inputs        ,@dp-ram-16x32-inputs)
     (loadings      2 2 2 2
		    2 2 2 2
		    4
		    1 1 1 1 1 1 1 1  
		    1 1 1 1 1 1 1 1  
		    1 1 1 1 1 1 1 1  
		    1 1 1 1 1 1 1 1)
     (lsi-name      . cmrb100a)
     (new-states    . (dual-port-ram-state
		       '32 '4
		       ,(cons-up dp-ram-16x32-inputs)
		       state))
     (output-types  boolp boolp boolp boolp boolp boolp boolp boolp
		    boolp boolp boolp boolp boolp boolp boolp boolp
		    boolp boolp boolp boolp boolp boolp boolp boolp
		    boolp boolp boolp boolp boolp boolp boolp boolp)
     (out-depends   . ,(make-list
			32
			:initial-element
			'(read-a0 read-a1 read-a2 read-a3)))
     (outputs       o0  o1  o2  o3  o4  o5  o6  o7
		    o8  o9  o10 o11 o12 o13 o14 o15
		    o16 o17 o18 o19 o20 o21 o22 o23
		    o24 o25 o26 o27 o28 o29 o30 o31)
     (results       . (dual-port-ram-value
		       '32 '4
		       ,(cons-up dp-ram-16x32-inputs)
		       state))
     (state-types   . (addressed-state 4 (ram ',(make-list 32 :initial-element
							   'boolp))))
     (states        . state)

     (gates         . 2368)
     (primitives    . 1)
     (transistors   . 9472))  ; Estimate: 4 * 2368


    (fd1
     (delays        ((147 1024) (55 1288))
		    ((145 1432) (53 1447)))
     (drives        10 10)
     (input-types   boolp clk)
     (inputs        d cp)
     (loadings      1 1)
     (lsi-name      . fd1)
     (new-states    . (f-buf d))
     (out-depends   () ())
     (output-types  boolp boolp)
     (outputs       q qn)
     (results       . ,(cons-up '((f-buf state) (f-not state))))
     (state-types   . boolp)
     (states        . state)
                  
     (gates         . 7)
     (primitives    . 1)
     (transistors   . 26))


    (fd1s
     (delays        ((147 1024) (55 1288))
		    ((145 1432) (53 1447)))
     (drives        10 10)
     (input-types   boolp clk boolp boolp)
     (inputs        d cp ti te)
     (loadings      1 1 1 2)
     (lsi-name      . fd1s)
     (new-states    . (f-if te ti d))
     (out-depends   () ())
     (output-types  boolp boolp)
     (outputs       q qn)
     (results       . ,(cons-up '((f-buf state) (f-not state))))
     (state-types   . boolp)
     (states        . state)
                  
     (gates         . 9)
     (primitives    . 1)
     (transistors   . 34))


    (fd1sp
     (delays        ((68 1084) (34 1327))
		    ((65 1712) (32 1596)))
     (drives        16 16)
     (input-types   boolp clk boolp boolp)
     (inputs        d cp ti te)
     (loadings      1 1 1 2)
     (lsi-name      . fd1sp)
     (new-states    . (f-if te ti d))
     (out-depends   () ())
     (output-types  boolp boolp)
     (outputs       q qn)
     (results       . ,(cons-up '((f-buf state) (f-not state))))
     (state-types   . boolp)
     (states        . state)
                  
     (gates         . 10)
     (primitives    . 1)
     (transistors   . 38))


    (fd1slp
     (delays        ((70 1085) (45  982))
		    ((67 1493) (35 1568)))
     (drives        12 12)
     (input-types   boolp clk boolp boolp boolp)
     (inputs        d cp ld ti te)
     (loadings      1 1 2 1 2)
     (lsi-name      . fd1slp)
     (new-states    . (f-if te ti (f-if ld d state)))
     (out-depends   () ())
     (output-types  boolp boolp)
     (outputs       q qn)
     (results       . ,(cons-up '((f-buf state) (f-not state))))
     (state-types   . boolp)
     (states        . state)

     (gates         . 12)
     (primitives    . 1)
     (transistors   . 40))


    (id
     (delays        a)
     (drives        a)
     (input-types   free)
     (inputs        a)
     (loadings      0)
     (lsi-name      . id)
     (out-depends   (a))
     (output-types  (a))
     (outputs       z)
     (results       . (cons a 'nil))

     (gates         . 0)
     (primitives    . 0)
     (transistors   . 0))


    (mem-32x32
     ;; Delays are arbitrary.  Slopes are 10 times NAND slopes.
     (delays        . ,(make-list 33
				  :initial-element
				  '((1410 20000) (820 20000))))
     (drives        . ,(make-list 33 :initial-element 10))

     (input-types   boolp boolp

                    boolp boolp boolp boolp boolp boolp boolp boolp
		    boolp boolp boolp boolp boolp boolp boolp boolp
		    boolp boolp boolp boolp boolp boolp boolp boolp
		    boolp boolp boolp boolp boolp boolp boolp boolp
		    
		    boolp boolp boolp boolp boolp boolp boolp boolp
		    boolp boolp boolp boolp boolp boolp boolp boolp
		    boolp boolp boolp boolp boolp boolp boolp boolp
		    boolp boolp boolp boolp boolp boolp boolp boolp)

     (inputs        ,@mem-32x32-inputs)

     (loadings      1 1

		    1 1 1 1 1 1 1 1  
		    1 1 1 1 1 1 1 1  
		    1 1 1 1 1 1 1 1  
		    1 1 1 1 1 1 1 1

		    1 1 1 1 1 1 1 1  
		    1 1 1 1 1 1 1 1  
		    1 1 1 1 1 1 1 1  
		    1 1 1 1 1 1 1 1)

     ;; The LSI-name is arbitrary.  This is a model of a memory system, NOT an
     ;; actual LSI macrocell.  The LSI-NAME is specified here because the
     ;; primitive-database predicate requires it.
     (lsi-name      . mem-32x32)

     (new-states    . (mem-state
		       ,(cons-up mem-32x32-inputs)
		       state))

     (out-depends   . ,(make-list
			33
			:initial-element
			'(rw- strobe-
			  a0  a1  a2  a3  a4  a5  a6  a7
			  a8  a9  a10 a11 a12 a13 a14 a15
			  a16 a17 a18 a19 a20 a21 a22 a23
			  a24 a25 a26 a27 a28 a29 a30 a31)))

     (output-types  boolp
		    tri-state tri-state tri-state tri-state
		    tri-state tri-state tri-state tri-state
		    tri-state tri-state tri-state tri-state
		    tri-state tri-state tri-state tri-state
		    tri-state tri-state tri-state tri-state
		    tri-state tri-state tri-state tri-state
		    tri-state tri-state tri-state tri-state
		    tri-state tri-state tri-state tri-state)

     (outputs       dtack-
		    o0  o1  o2  o3  o4  o5  o6  o7
		    o8  o9  o10 o11 o12 o13 o14 o15
		    o16 o17 o18 o19 o20 o21 o22 o23
		    o24 o25 o26 o27 o28 o29 o30 o31)

     (results       . (mem-value
		       ,(cons-up mem-32x32-inputs)
		       state))

     (state-types   . ((addressed-state 32 (ram ',(make-list 32
							     :initial-element
							     'boolp)))
		       numberp number-listp numberp boolp boolp
		       ,(make-list 32 :initial-element 'boolp)
		       ,(make-list 32 :initial-element 'boolp)))

     (states        . state)

     (gates         . 0)
     (primitives    . 1)
     (transistors   . 0))



    ;; (ram-enable-circuit
    ;;  (clk test-regfile- disable-regfile- we)
    ;;  (z)
    ;;  ((g0 (clk-10)       del10    (clk))
    ;;   (g1 (test-regfile) b-not    (test-regfile-))
    ;;   (g2 (gate-clk)     b-or     (clk-10 test-regfile))
    ;;   (g3 (z)            b-nand3p (we disable-regfile- gate-clk)))
    ;;  nil)
    ;;
    ;; NOTE: B-NAND3P is not in the primp-database.

    ;; MODULE RAM-ENABLE-CIRCUIT;
    ;; INPUTS CLK,TEST-REGFILE-,DISABLE-REGFILE-,WE;
    ;; OUTPUTS Z;
    ;; LEVEL FUNCTION;
    ;; DEFINE
    ;; G0 (CLK-10)       = DEL10 (CLK);
    ;; G1 (TEST-REGFILE) = IVA   (TEST-REGFILE-);
    ;; G2 (GATE-CLK)     = OR2   (CLK-10,TEST-REGFILE);
    ;; G3 (Z)            = ND3P  (WE,DISABLE-REGFILE-,GATE-CLK);
    ;; END MODULE;

    ;; loadings:  CLK              1
    ;;            TEST-REGFILE-    2
    ;;            CLK-10           1
    ;;            TEST-REGFILE     1
    ;;            WE               2
    ;;            DISABLE-REGFILE- 2
    ;;            GATE-CLK         2
    ;;
    ;; delays:  (slope*load) + intercept + input-delay
    ;;  CLK-10
    ;;    primp delay: ((60 10530) (49 10424))
    ;;    low-to-high: (60 * 1) + 10530 + CLK = 10590 + CLK
    ;;    high-to-low: (49 * 1) + 10424 + CLK = 10473 + CLK
    ;;  TEST-REGFILE
    ;;    primp delay: ((70 235) (57 198))
    ;;    low-to-high: (70 * 1) + 235 + TEST-REGFILE- = 305 + TEST-REGFILE-
    ;;    high-to-low: (57 * 1) + 198 + TEST-REGFILE- = 255 + TEST-REGFILE-
    ;;  GATE-CLK
    ;;    primp delay: ((143 332) (58 819))
    ;;    low-to-high:   (143 * 2) + 332 + max(CLK-10,TEST-REGFILE)
    ;;                 = 618             + max(CLK-10,TEST-REGFILE)
    ;;    high-to-low:   ( 58 * 2) + 819 + max(CLK-10,TEST-REGFILE)
    ;;                 = 935             + max(CLK-10,TEST-REGFILE)
    ;;    range:         [618 .. 935] + max(CLK-10,TEST-REGFILE)
    ;;                 =       [  618 .. 935]
    ;;                   + max([10473..10590]+CLK, [255..305]+TEST-REGFILE-)
    ;;                le [11091 .. 11525] + max(CLK, TEST-REGFILE-)
    ;;  Z
    ;;    primp delay: ((68 552) (54 311))
    ;;    low-to-high:   (slope*load) + intercept + input-delay
    ;;                 = (68   * 0)   + 552       + max(WE, DISABLE-REGFILE-,
    ;;                                                  GATE-CLK)
    ;;                 le 552 + max(WE, DISABLE-REGFILE-,
    ;;                             [11091..11525]+max(CLK,TEST-REGFILE-))
    ;;                 le 552 + [11091..11525] + max(CLK, TEST-REGFILE-,
    ;;                                               DISABLE-REGFILE-, WE)
    ;;                 = [11643..12077] + max(...)
    ;;                 average 11860
    ;;    high-to-low:   (slope*load) + intercept + input-delay
    ;;                 = (54   * 0)   + 311       + max(WE, DISABLE-REGFILE-,
    ;;                                                  GATE-CLK)
    ;;                 le 311 + max(WE, DISABLE-REGFILE-,
    ;;                              [11091..11525]+max(CLK,TEST-REGFILE-))
    ;;                 le 311  + [11091..11525] + max(CLK, TEST-REGFILE-,
    ;;                                                DISABLE-REGFILE-, WE)
    ;;                 = [11402..11836] + max(...)
    ;;                 average 11619

    (ram-enable-circuit
     (delays        ((68 12000) (54 12000)))
     (drives        10)
     (input-types   clk boolp boolp boolp)
     (inputs        clk test-regfile- disable-regfile- we)
     (loadings      1 2 2 2)
     (lsi-name      . ram-enable-circuit)
     (out-depends   (clk test-regfile- disable-regfile- we))
     (output-types  level)
     (outputs       z)
     (results       . ,(cons-up '((f-nand disable-regfile- we))))

     (gates         . 24)
     (primitives    . 1)
     (transistors   . 97))


    (t-buf
     (delays        ((146 313) (57 728)))
     (drives        10)
     (input-types   boolp boolp)
     (inputs        e a)
     (loadings      2 2)
     (lsi-name      . (bts4 a e))	; Note input reordering
     (out-depends   (a e))
     (output-types  tri-state)
     (outputs       z)
     (results       . ,(cons-up '((ft-buf e a))))

     (gates         . 3)
     (primitives    . 1)
     (transistors   . 12))


    (t-wire
     (delays        (or  a b))
     (drives        (min a b))
     (input-types   tri-state tri-state)
     (inputs        a b)
     (loadings      1 1)
     (lsi-name      . t-wire)
     (out-depends   (a b))
     (output-types  tri-state)
     (outputs       z)
     (results       . ,(cons-up '((ft-wire a b))))

     (gates         . 0)
     (primitives    . 0)
     (transistors   . 0))


    (pullup
     (delays        a)
     (drives        a)
     (input-types   tri-state)
     (inputs        a)
     (loadings      1)
     (lsi-name      . pullup)
     (out-depends   (a))
     (output-types  boolp)
     (outputs       z)
     (results       . ,(cons-up '((f-pullup a))))

     (gates         . 0)
     (primitives    . 0)
     (transistors   . 0))


    ;;  Delay information may not be correct for the pads.


    ;; Note: (1) zi delay (second one) is from LSI ttl input buffer TLCHT.
    ;;           (See pages 4-39 and 4-27 of LSI book.)
    ;;       (2) po delay (third one) has ND2 (b-nand) slopes, and 
    ;;           intercepts are ND2 intercepts plus output ZI intercepts.
    ;;           (See drawings on pages 4-40 and 4-27 of LSI book.)

    (ttl-bidirect
     (delays        (((61 ps-pf) 1633) ((41 ps-pf) 2253))
		    (( 43         633) (20          638))
		    ((141        1053) (82          799)))
     (drives        (8 mA) 10 10)
     (input-types   ttl-tri-state boolp boolp parametric)
     (inputs        io a en pi)
     (loadings      (3 pf) 1 1 1)
     (lsi-name      . bd8trp)
     (out-depends   (en a) (en a io) (en a io pi))
     (output-types  ttl-tri-state boolp parametric)
     (outputs       io zi po)
     (results       . ,(cons-up
			'((ft-buf (f-not en) a) 
			  (f-buf (ft-wire io (ft-buf (f-not en) a)))
			  (f-nand (ft-wire io (ft-buf (f-not en) a))
				  pi))))

     (gates         . 0)
     (pads          . 1)
     (primitives    . 1)
     (transistors   . 0))


    (ttl-clk-input
     (delays        ((  4 1225) (  4 1152))
		    ((202 1050) (117  741)))
     (drives        400 10)
     (input-types   ttl parametric)
     (inputs        a pi)
     (loadings      (3 pf) 1)
     (lsi-name      . drvt8)
     (out-depends   (a) (a pi))
     (output-types  clk parametric)
     (outputs       z po)
     (results       . ,(cons-up '((f-buf a) (f-nand a pi))))

     (gates         . 0)
     (pads          . 2)
     (primitives    . 1)
     (transistors   . 0))


    ;; Note: po delay (second one) has ND2 (b-nand) slopes, and 
    ;;       intercepts are ND2 intercepts plus output Z intercepts.
    ;;       (See drawings on page 4-27 of LSI book.)

    (ttl-input
     (delays        (( 43  633) (20 638))
		    ((141 1053) (82 799)))
     (drives        10 10)
     (input-types   ttl parametric)
     (inputs        a pi)
     (loadings      (3 pf) 1)
     (lsi-name      . tlcht)
     (out-depends   (a) (a pi))
     (output-types  boolp parametric)
     (outputs       z po)
     (results       . ,(cons-up '((f-buf a) (f-nand a pi))))

     (gates         . 0)
     (pads          . 1)
     (primitives    . 1)
     (transistors   . 0))


    (ttl-output
     (delays        (((61 ps-pf) 812) ((42 ps-pf) 1155)))
     (drives        (8 mA))
     (input-types   boolp)
     (inputs        a)
     (loadings      5)
     (lsi-name      . b8rp)
     (out-depends   (a))
     (output-types  ttl)
     (outputs       z)
     (results       . (cons (f-buf a) 'nil))

     (gates         . 0)
     (pads          . 1)
     (primitives    . 1)
     (transistors   . 0))


    (ttl-output-parametric
     (delays        (((64 ps-pf) 737) ((42 ps-pf) 1125)))
     (drives        (4 mA))
     (input-types   parametric)
     (inputs        a)
     (loadings      3)
     (lsi-name      . b4)	
     (out-depends   (a))
     (output-types  ttl)
     (outputs       z)
     (results       . (cons (f-buf a) 'nil))

     (gates         . 0)
     (pads          . 1)
     (primitives    . 1)
     (transistors   . 0))


    (ttl-output-fast
     (delays        (((36 ps-pf) 991) ((24 ps-pf) 1488)))
     (drives        (8 mA))
     (input-types   boolp)
     (inputs        a)
     (loadings      3)
     (lsi-name      . b8)
     (out-depends   (a))
     (output-types  ttl)
     (outputs       z)
     (results       . (cons (f-buf a) 'nil))

     (gates         . 0)
     (pads          . 1)
     (primitives    . 1)
     (transistors   . 0))


    (ttl-tri-output
     (delays        (((61 ps-pf) 1602) ((41 ps-pf) 2233)))
     (drives        (8 mA))
     (input-types   boolp boolp)
     (inputs        a en)
     (loadings      1 1)
     (lsi-name      . bt8rp)
     (out-depends   (a en))
     (output-types  ttl-tri-state)
     (outputs       z)
     (results       . (cons (ft-buf (f-not en) a) 'nil))

     (gates         . 0)
     (pads          . 1)
     (primitives    . 1)
     (transistors   . 0))


    (ttl-tri-output-fast
     (delays        (((36 ps-pf) 1581) ((24 ps-pf) 2198)))
     (drives        (8 mA))
     (input-types   boolp boolp)
     (inputs        a en)
     (loadings      1 1)
     (lsi-name      . bt8)
     (out-depends   (a en))
     (output-types  ttl-tri-state)
     (outputs       z)
     (results       . (cons (ft-buf (f-not en) a) 'nil))

     (gates         . 0)
     (pads          . 1)
     (primitives    . 1)
     (transistors   . 0))


    (vdd
     (delays        ((0 0) (0 0)))
     (drives        50)
     (input-types   )
     (inputs        )
     (loadings      )
     (lsi-name      . vdd)
     (out-depends   ())
     (output-types  boolp)
     (outputs       z)
     (results       . (cons '*1*true 'nil))

     (gates         . 0)
     (primitives    . 1)
     (transistors   . 0))


    (vdd-parametric
     (delays        ((0 0) (0 0)))
     (drives        50)
     (input-types   )
     (inputs        )
     (loadings      )
     (lsi-name      . vdd)
     (out-depends   ())
     (output-types  parametric)
     (outputs       z)
     (results       . (cons '*1*true 'nil))

     (gates         . 0)
     (primitives    . 1)
     (transistors   . 0))
                     

    (vss
     (delays        ((0 0) (0 0)))
     (drives        50)
     (input-types   )
     (inputs        )
     (loadings      )
     (lsi-name      . vss)
     (out-depends   ())
     (output-types  boolp)
     (outputs       z)
     (results       . (cons '*1*false 'nil))

     (gates         . 0)
     (primitives    . 1)
     (transistors   . 0))

    ))

;;;  Abbreviations

(defconstant dp-ram-16x32-inputs
  '(read-a0 read-a1 read-a2 read-a3
	    write-b0 write-b1 write-b2 write-b3
	    wen
	    d0  d1  d2  d3  d4  d5  d6  d7
	    d8  d9  d10 d11 d12 d13 d14 d15
	    d16 d17 d18 d19 d20 d21 d22 d23
	    d24 d25 d26 d27 d28 d29 d30 d31))

(defconstant mem-32x32-inputs
  '(rw- strobe-

	a0  a1  a2  a3  a4  a5  a6  a7
	a8  a9  a10 a11 a12 a13 a14 a15
	a16 a17 a18 a19 a20 a21 a22 a23
	a24 a25 a26 a27 a28 a29 a30 a31

	d0  d1  d2  d3  d4  d5  d6  d7
	d8  d9  d10 d11 d12 d13 d14 d15
	d16 d17 d18 d19 d20 d21 d22 d23
	d24 d25 d26 d27 d28 d29 d30 d31
	))

;;;  CONS-UP builds a quoted expression suitable for EVAL$.

(defun cons-up (list)
  (cond
   ((null list) ''NIL)
   (t `(CONS ,(car list) ,(cons-up (cdr list))))))

;;;  Closes the #. above.

)))