(define VDD 5.0)
(define VOH 4.5)
(define VIH 4.0)
(define VT  1.2)
(define VIL 1.0)
(define VOL 0.5)
(define GND 0.0)


;;; 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)
	   '(power-high power-low)
	   '((bias
	      ()
	      ((q        nmos-fet    out in  gnd)
	       (pull-up  resistor    vdd out))
	      ()
	      ((VT-typical (= (>> VT q) VT))
	       (k-typical (= (>> k q) 0.001))
	       (power-high-calc
		(= 0
		   (>> power-high)))
	       (power-low-calc
		(= (* (>> potential vdd)
		      (/ (>> potential vdd)
			 (+ (>> ron q) (>> resistance pull-up))))
		   (>> power-low)))
	       (divider			;voltage dividers need help
		(iff (> (>> potential in) (>> VT q))
		     (= (- (>> potential out)
			   (>> potential gnd))
			(* (/ (>> ron q)
			      (+ (>> resistance pull-up) (>> 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)))))
	   '())



;;; Here we define the digital idea of an "nand", but relate it to
;;; the static discipline.  It will be better to separate out the
;;; static discipline too.

(part-type 'digital-nand
	   '(in1 in2 out vdd mid gnd)
	   '()
	   '((digital () () ()
	      ((and1
		(iff (and (= 1 (>> potential in1))
			  (= 1 (>> potential in2)))
		     (= 0 (>> potential out))))
	       (and2
		(iff (> 2 (+ (>> potential in1)
			     (>> potential in2)))
		     (= 1 (>> potential out))))))
	     (else () () () ()))	;default model is empty.
	   '((input-low-spec1
	      (iff (= 0 (:> (potential in1) digital))
		   (and (<= GND (:> (potential in1) bias))
			(<= (:> (potential in1) bias) VIL)))
	      (digital bias))
	     (input-high-spec1
	      (iff (= 1 (:> (potential in1) digital))
		   (and (<= VIH (:> (potential in1) bias))
			(<= (:> (potential in1) bias) VDD)))
	      (digital bias))
	     (input-low-spec2
	      (iff (= 0 (:> (potential in2) digital))
		   (and (<= GND (:> (potential in2) bias))
			(<= (:> (potential in2) bias) VIL)))
	      (digital bias))
	     (input-high-spec2
	      (iff (= 1 (:> (potential in2) digital))
		   (and (<= VIH (:> (potential in2) bias))
			(<= (:> (potential in2) 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 bias model of the and

(part-type 'analog-nand
	   '(in1 in2 out vdd mid gnd)
	   '()
	   '((bias
	      ()
	      ((q1       nmos-fet    out in1 mid)
	       (q2       nmos-fet    mid in2 gnd)
	       (pull-up  resistor    vdd out))
	      ()
	      ((VT-typical1 (= (>> VT q1) VT))
	       (k-typical1 (= (>> k q1) 0.001))
	       (VT-typical2 (= (>> VT q2) VT))
	       (k-typical2 (= (>> k q2) 0.001))
	       (divider			;voltage dividers need help
		(iff (and (> (>> potential in1) (>> VT q1))
			  (> (>> potential in2) (>> VT q2)))
		     (= (- (>> potential out)
			   (>> potential gnd))
			(* (/ (+ (>> ron q1) (>> ron q2))
			      (+ (>> resistance pull-up) 
				 (>> ron q1) 
				 (>> ron q2)))
			   (- (>> potential vdd)
			      (>> potential gnd))))))))
	     (else () () () ()))	;default model is empty.
	   '())



;;; An nand-gate is an overlay of an analog-nand and a
;;; digital-nand

(part-type 'nand-gate
	   '(in1 in2 out vdd mid gnd)
	   '()
	   '((else () () () ()))	;default model is empty.
	   '()
	   '((analog analog-nand)
	     (logic digital-nand)))


	     
(part-type 'nand-test
	   '()
	   '()
	   '((any-model
	      (in1 in2 out vdd mid gnd)
	      ((power dc-voltage-source vdd gnd)
	       (sigin1 marginal-digital-source in1 gnd)
	       (sigin2 marginal-digital-source in2 gnd)
	       (nand nand-gate in1 in2 out vdd mid gnd))
	      ()
	      ((ground (= (>> potential gnd) GND))
	       (power  (= (>> potential vdd) VDD)))))
	   '())

#|
(define test (create-circuit 'foo 'nand-test '(digital bias)))
|#