;;; Reference voltages

(define VDD 5.0)
(define VOH 4.0)
(define VIH 3.0)
(define VT  1.0)
(define VIL 0.75)
(define VOL 0.5)
(define GND 0.0)


;;; We could have defined the inverter to have a digital model as well
;;; as an analog model.  This works.  However it is nice to separate
;;; concerns (see next page).
#|
(part-type 'nmos-inverter
	   '(in out vdd gnd)
	   '()
	   '((bias
	      ()
	      ((q    nmos-fet    out in  gnd)
	       (rpu  resistor    vdd out))
	      ()
	      ((VT-typical (= (>> VT q) VT))
	       (divider			;voltage dividers need help
		(= (- (>> potential out)
		      (>> potential gnd))
		   (* (/ (>> ron q)
			 (+ (>> resistance rpu) (>> ron q)))
		      (- (>> potential vdd)
			 (>> potential gnd)))))))
	     (digital () () ()
	      ((inv1
		(iff (= 0 (>> potential in))
		     (= 1 (>> potential out))))
	       (inv2
		(iff (= 1 (>> potential in))
		     (= 0 (>> potential out))))))
	     (else () () () ()))
	   '((input-low-spec
	      (iff (= 0 (:> (potential in) digital))
		   (and (<= GND (:> (potential in) bias))
			(<= (:> (potential in) bias) VIL)))
	      (digital bias))
	     (input-high-spec
	      (iff (= 1 (:> (potential in) digital))
		   (and (<= VIH (:> (potential in) bias))
			(<= (:> (potential in) bias) VDD)))
	      (digital bias))

	     (output-low-spec
	      (iff (= 0 (:> (potential out) digital))
		   (and (<= GND (:> (potential out) bias))
			(<= (:> (potential out) bias) VOL)))
	      (digital bias))
	     (output-high-spec
	      (iff (= 1 (:> (potential out) digital))
		   (and (<= VOH (:> (potential out) bias))
			(<= (:> (potential out) bias) VDD)))
	      (digital bias))))
|#

;;; Here we define the digital idea of an inverter, but relate it to
;;; the static discipline.  It will be better to separate out the
;;; static discipline too.

(part-type 'inverter
	   '(in out vdd gnd)
	   '()
	   '((digital () () ()
	      ((inv1
		(iff (= 0 (>> potential in))
		     (= 1 (>> potential out))))
	       (inv2
		(iff (= 1 (>> potential in))
		     (= 0 (>> potential out))))))
	     (else () () () ()))	;default model is empty.
	   '((input-low-spec
	      (iff (= 0 (:> (potential in) digital))
		   (and (<= GND (:> (potential in) bias))
			(<= (:> (potential in) bias) VIL)))
	      (digital bias))
	     (input-high-spec
	      (iff (= 1 (:> (potential in) digital))
		   (and (<= VIH (:> (potential in) bias))
			(<= (:> (potential in) bias) VDD)))
	      (digital bias))

	     (output-low-spec
	      (iff (= 0 (:> (potential out) digital))
		   (and (<= GND (:> (potential out) bias))
			(<= (:> (potential out) bias) VOL)))
	      (digital bias))
	     (output-high-spec
	      (iff (= 1 (:> (potential out) digital))
		   (and (<= VOH (:> (potential out) bias))
			(<= (:> (potential out) bias) VDD)))
	      (digital bias))))

;;; Here we define an nmos amplifier

(part-type 'nmos-amplifier
	   '(in out vdd gnd)
	   '()
	   '((bias
	      ()
	      ((q    nmos-fet    out in  gnd)
	       (rpu  resistor    vdd out))
	      ()
	      ((VT-typical (= (>> VT q) VT))
	       (divider			;voltage dividers need help
		(= (- (>> potential out)
		      (>> potential gnd))
		   (* (/ (>> ron q)
			 (+ (>> resistance rpu) (>> ron q)))
		      (- (>> potential vdd)
			 (>> potential gnd)))))))
	     (else () () () ()))	;default model is empty.
	   '())


;;; An nmos-inverter is an overlay of an analog amplifier and a
;;; digital inverter

(part-type 'nmos-inverter
	   '(in out vdd gnd)
	   '()
	   '((else () () () ()))	;default model is empty.
	   '()
	   '((analog nmos-amplifier)
	     (logic inverter)))

(part-type 'marginal-digital-source
	   '(out gnd)
	   '()
	   '((bias
	      ()
	      ()
	      (voltage)
	      ((kvl
		(= (>> voltage)
		   (- (>> potential out)
		      (>> potential gnd))))
	       (kcl
		(= (>> current out)
		   (- (>> current gnd))))))
	     (digital
	      ()
	      ()
	      ()
	      ((state
		(try
		 (high (= 1 (>> potential out)))
		 (low  (= 0 (>> potential out))))))))
	   '((lo
	      (iff (= 0 (:> (potential out) digital))
		   (= (:> (voltage) bias) VIL))
	      (digital bias))
	     (hi
	      (iff (= 1 (:> (potential out) digital))
		   (= (:> (voltage) bias) VIH))
	      (digital bias))))
	     
(part-type 'inverter-test
	   '()
	   '()
	   '((any-model
	      (in out vdd gnd)
	      ((power dc-voltage-source vdd gnd)
	       (sigin marginal-digital-source in gnd)
	       (ni nmos-inverter in out vdd gnd))
	      ()
	      ((ground (= (>> potential gnd) GND))
	       (power  (= (>> potential vdd) VDD)))))
	   '())

(define test
  (create-circuit 'T 'inverter-test '(digital bias)))

(assume-value test '(strength power) 5)

(propagate (constraint-network test))

(node-assume! (referent test '(high state sigin digital)))

(propagate (constraint-network test))

(the-value test '(potential out sigin digital))
; ((potential in digital) = 1)
;   (set by (=R:0:state sigin digital))
;     (because ((v:lhs:R:0:state sigin digital) ()))
;Value: 1


(the-value test '(potential out sigin bias))
; ((potential in bias) = 3.)
;   (set by (-rhs:kvl sigin bias))
;     (because ((voltage sigin bias) (potential gnd bias)))
;Value: 3.

(explain (connector-assignment (referent test '(potential out sigin bias))))
;(TP86 (potential in bias) = 3. set by (-rhs:kvl sigin bias) (TP85 TP43))
;(TP85 (voltage sigin bias) = 3. set by (=rhs:hi sigin) (TP53 TP51))
;(TP43 (potential gnd bias) = 0. set by (v:rhs:ground ni bias) ())
;(TP53 (v:rhs:rhs:hi sigin) = 3. set by (c:rhs:rhs:hi sigin) ())
;(TP51 iff:hi set by (=lhs:hi sigin) (TP52 TP83))
;(TP52 (v:lhs:lhs:hi sigin) = 1 set by (c:lhs:lhs:hi sigin) ())
;(TP83 (potential in digital) = 1 set by (=R:0:state sigin digital) (TP5 TP4))
;(TP5 (v:lhs:R:0:state sigin digital) = 1 set by (c:lhs:R:0:state sigin digital) ())
;(TP4 T:0:state PREMISE)
;Value: QED

(assume-value test '(ron q ni bias) 300)

(propagate (constraint-network test))

(assume-value test '(resistance rpu ni bias) 500)

(propagate (constraint-network test))
; (Contradiction! #[uninterned-symbol 49 TP100])

(explain (car (cn-contradictions (constraint-network test))))
;(TP100 contradiction found by (<=rhs:rhs:output-low-spec ni) (TP68 TP99 TP71))
;(TP68 and-a2:rhs:output-low-spec set by (and:rhs:output-low-spec ni) (TP66))
;(TP99 (potential out bias) = 1.875 set by (-lhs:divider ni bias) (TP98 TP44))
;(TP71 (v:rhs:rhs:rhs:output-low-spec ni) = .5 set by (c:rhs:rhs:rhs:output-low-spec ni) ())
;(TP66 iff:output-low-spec set by (=lhs:output-low-spec ni) (TP67 TP85))
;(TP98 (=divider ni bias) = 1.875 set by (*rhs:divider ni bias) (TP97 TP82))
;(TP44 (potential gnd bias) = 0. set by (v:rhs:ground bias) ())
;(TP67 (v:lhs:lhs:output-low-spec ni) = 0 set by (c:lhs:lhs:output-low-spec ni) ())
;(TP85 (potential out digital) = 0 set by (=rhs:inv2 ni digital) (TP13 TP11))
;(TP97 (v:0:rhs:divider ni bias) = 3/8 set by (/0:rhs:divider ni bias) (TP92 TP96))
;(TP82 (v:1:rhs:divider ni bias) = 5. set by (-1:rhs:divider ni bias) (TP45 TP44))
;(TP13 (v:lhs:rhs:inv2 ni digital) = 0 set by (c:lhs:rhs:inv2 ni digital) ())
;(TP11 iff:inv2 set by (=lhs:inv2 ni digital) (TP12 TP84))
;(TP92 (ron q ni bias) = 300 set by assumption (TP93))
;(TP96 (v:1:0:rhs:divider ni bias) = 800 set by (+1:0:rhs:divider ni bias) (TP94 TP92))
;(TP45 (potential vdd bias) = 5. set by (v:rhs:power bias) ())
;(TP12 (v:lhs:lhs:inv2 ni digital) = 1 set by (c:lhs:lhs:inv2 ni digital) ())
;(TP84 (potential in digital) = 1 set by (=R:0:state sigin digital) (TP5 TP4))
;(TP94 (resistance rpu ni bias) = 500 set by assumption (TP95))
;(TP5 (v:lhs:R:0:state sigin digital) = 1 set by (c:lhs:R:0:state sigin digital) ())
;(TP4 T:0:state PREMISE)
;Value: QED

(retract-assumed-value test '(resistance rpu ni bias))

(assume-value test '(resistance rpu ni bias) 6800.)

(propagate (constraint-network test))

(the-value test '(current drain q ni bias))
; ((current drain q ni bias) = 7.04225352112676e-4)
;   (set by (kcl-terminal out ni bias))
;     (because ((current out ni bias) (current t2 rpu ni bias)))
;Value: 7.04225352112676e-4


(the-value test '(potential out bias))
; ((potential out bias) = .2112676056338028)
;   (set by (-lhs:divider ni bias))
;     (because ((=divider ni bias) (potential gnd bias)))
;Value: .2112676056338028

(node-in? (referent test '(cutoff operation q ni bias)))
;Value: ()

(node-in? (referent test '(amplifying operation q ni bias)))
;Value: ()

(node-in? (referent test '(switched-on operation q ni bias)))
;Value: ()

(node-in? (referent test '(on operation q ni bias)))
;Value 39: ((*CONSTRAINT* and:R:3:operation) #[uninterned-symbol 40 TP39] #[uninterned-symbol 41 TP38])

(explain (referent test '(on operation q ni bias)))
;(TP37 T:3:operation set by (and:R:3:operation q ni bias) (TP39 TP38))
;(TP39 and-a1:R:3:operation set by (<lhs:R:3:operation q ni bias) (TP40 TP89))
;(TP38 and-a2:R:3:operation set by (=rhs:R:3:operation q ni bias) (TP122 TP132))
;(TP40 (v:lhs:lhs:R:3:operation q ni bias) = 0 set by (c:lhs:lhs:R:3:operation q ni bias) ())
;(TP89 (ve q ni bias) = 2. set by (-rhs:vedef q ni bias) (TP88 TP42))
;(TP122 (vds q ni bias) = .2112676056338028 set by (-rhs:kvl-ds q ni bias) (TP120 TP44))
;(TP132 (v:rhs:rhs:R:3:operation q ni bias) = .21126760563380279 set by (*rhs:rhs:R:3:operation q ni bias) (TP92 TP128))
;(TP88 (vgs q ni bias) = 3. set by (-rhs:kvl-gs q ni bias) (TP87 TP44))
;(TP42 (VT q ni bias) = 1 set by (v:rhs:VT-typical q ni bias) ())
;(TP120 (potential out bias) = .2112676056338028 set by (-lhs:divider ni bias) (TP119 TP44))
;(TP44 (potential gnd bias) = 0. set by (v:rhs:ground bias) ())
;(TP92 (ron q ni bias) = 300 set by assumption (TP93))
;(TP128 (current drain q ni bias) = 7.04225352112676e-4 set by (kcl-terminal out ni bias) (TP47 TP127))
;(TP87 (potential in bias) = 3. set by (-rhs:kvl sigin bias) (TP86 TP44))
;(TP119 (=divider ni bias) = .2112676056338028 set by (*rhs:divider ni bias) (TP118 TP82))
;(TP47 (current out ni bias) = 0 set by (kcl-node out bias) ())
;(TP127 (current t2 rpu ni bias) = -7.04225352112676e-4 set by (-rhs:kcl rpu ni bias) (TP123))
;(TP86 (voltage sigin bias) = 3. set by (=rhs:hi sigin) (TP53 TP51))
;(TP118 (v:0:rhs:divider ni bias) = .04225352112676056 set by (/0:rhs:divider ni bias) (TP92 TP117))
;(TP82 (v:1:rhs:divider ni bias) = 5. set by (-1:rhs:divider ni bias) (TP45 TP44))
;(TP123 (current t1 rpu ni bias) = 7.04225352112676e-4 set by (*rhs:ohm rpu ni bias) (TP121 TP115))
;(TP53 (v:rhs:rhs:hi sigin) = 3. set by (c:rhs:rhs:hi sigin) ())
;(TP51 iff:hi set by (=lhs:hi sigin) (TP52 TP84))
;(TP117 (v:1:0:rhs:divider ni bias) = 7100. set by (+1:0:rhs:divider ni bias) (TP115 TP92))
;(TP45 (potential vdd bias) = 5. set by (v:rhs:power bias) ())
;(TP121 (voltage rpu ni bias) = 4.788732394366197 set by (-rhs:kvl rpu ni bias) (TP45 TP120))
;(TP115 (resistance rpu ni bias) = 6800. set by assumption (TP116))
;(TP52 (v:lhs:lhs:hi sigin) = 1 set by (c:lhs:lhs:hi sigin) ())
;(TP84 (potential in digital) = 1 set by (=R:0:state sigin digital) (TP5 TP4))
;(TP5 (v:lhs:R:0:state sigin digital) = 1 set by (c:lhs:R:0:state sigin digital) ())
;(TP4 T:0:state PREMISE)
;Value: QED