;;; Reference voltages

(define VDD 5.0)
(define VOH 4.5)
(define VIH 4.0)
(define VT  2.0)
(define VIL 1.5)
(define VOL 1.0)
(define GND 0.0)

(define RON 300)

;;; 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) VDD)

(assume-value test '(ron q ni bias) RON)


(propagate (constraint-network test))


;;; Student understands that the limit on rpu is determined by the low
;;; output voltage when the inverter is on.  So student turns inverter
;;; on by raising the input.

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

(propagate (constraint-network test))

;;; Since the input was made high, the output is now low.

(the-value test '(potential out digital))
; ((potential out digital) = 0)
;   (set by (=rhs:inv2 ni digital))
;     (because ((v:lhs:rhs:inv2 ni digital) ()))
;Value: 0



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

(propagate (constraint-network test))
; (Contradiction! #[uninterned-symbol 23 TP117])

(explain (car (cn-contradictions (constraint-network test))))
;(TP117 contradiction found by (<=rhs:rhs:output-low-spec ni) (TP67 TP116 TP70))
;(TP67 and-a2:rhs:output-low-spec set by (and:rhs:output-low-spec ni) (TP65))
;(TP116 (potential out bias) = 1.875 set by (-lhs:divider ni bias) (TP115 TP43))
;(TP70 (v:rhs:rhs:rhs:output-low-spec ni) = 1. set by (c:rhs:rhs:rhs:output-low-spec ni) ())
;(TP65 iff:output-low-spec set by (=lhs:output-low-spec ni) (TP66 TP86))
;(TP115 (=divider ni bias) = 1.875 set by (*rhs:divider ni bias) (TP114 TP81))
;(TP43 (potential gnd bias) = 0. set by (v:rhs:ground bias) ())
;(TP66 (v:lhs:lhs:output-low-spec ni) = 0 set by (c:lhs:lhs:output-low-spec ni) ())
;(TP86 (potential out digital) = 0 set by (=rhs:inv2 ni digital) (TP13 TP11))
;(TP114 (v:0:rhs:divider ni bias) = 3/8 set by (/0:rhs:divider ni bias) (TP83 TP113))
;(TP81 (v:1:rhs:divider ni bias) = 5. set by (-1:rhs:divider ni bias) (TP44 TP43))
;(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 TP85))
;(TP83 (ron q ni bias) = 300 set by assumption (TP84))
;(TP113 (v:1:0:rhs:divider ni bias) = 800 set by (+1:0:rhs:divider ni bias) (TP111 TP83))
;(TP44 (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) ())
;(TP85 (potential in digital) = 1 set by (=R:0:state sigin digital) (TP5 TP4))
;(TP111 (resistance rpu ni bias) = 500 set by assumption (TP112))
;(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

(support test (car (cn-contradictions (constraint-network test))))
;Value 24: ((high state sigin digital) (resistance rpu ni bias) (ron q ni bias))

(the-value test '(potential out bias))
; ((potential out bias) = 1.875)
;   (set by (-lhs:divider ni bias))
;     (because ((=divider ni bias) (potential gnd bias)))
;Value: 1.875