1% PROOF		: Transistor Implementation of a Counter		%
2% FILE		: mos.ml						%
3%									%
4% DESCRIPTION	: Defines MOS primitives based on a four-valued		%
5%		  logic where Zz and Er represent low impedence		%
6%		  (or floating) and undefined/unknown respectively.	%
7%		  Not is a negation function in the four-valued		%
8%		  logic and U is the least upper bound function.	%
9%									%
10%		  The MOS primitives were originally motivated by	%
11%		  models used by Inder Dhingra described in "Formal	%
12%		  Validation of an Integrated Circuit Design Style",	%
13%		  Hardware Verification Workshop, University of		%
14%		  Calgary, January 1987, however, the transistor	%
15%		  models differ slightly.				%
16%									%
17% AUTHOR	: J.Joyce						%
18% DATE		: 31 March 1987						%
19
20new_theory `mos`;;
21
22loadt `misc`;;
23loadt `types`;;
24
25new_constant (`Er`,":^val");;
26new_constant (`Hi`,":^val");;
27new_constant (`Lo`,":^val");;
28new_constant (`Zz`,":^val");;
29
30let val_not_eq_ax = new_axiom (
31	`val_not_eq_ax`,
32	"((Er = Hi) = F) /\ ((Er = Lo) = F) /\ ((Er = Zz) = F) /\
33	  ((Hi = Er) = F) /\ ((Hi = Lo) = F) /\ ((Hi = Zz) = F) /\
34	  ((Lo = Er) = F) /\ ((Lo = Hi) = F) /\ ((Lo = Zz) = F) /\
35	  ((Zz = Er) = F) /\ ((Zz = Hi) = F) /\ ((Zz = Lo) = F)");;
36
37let Not = new_definition (
38	`Not`,
39	"Not v = (v = Hi) => Lo | ((v = Lo) => Hi | Er)");;
40
41let U = new_infix_definition (
42	`U`,
43	"U (x:^val) (y:^val) =
44	  ((x = y) => x |
45	    (x = Zz) => y | (y = Zz) => x | Er)");;
46
47let Vdd = new_definition (`Vdd`,"Vdd (o:^wire) = !t. o (t) = Hi");;
48
49let Gnd = new_definition (`Gnd`,"Gnd (o:^wire) = !t. o (t) = Lo");;
50
51let Ptran = new_definition (
52	`Ptran`,
53	"Ptran (g:^wire,i:^wire,o:^wire) =
54	  !t. o t = (g t = Lo) => i t | ((g t = Hi) => Zz | Er)");;
55
56let Ntran = new_definition (
57	`Ntran`,
58	"Ntran (g:^wire,i:^wire,o:^wire) =
59	  !t. o t = (g t = Hi) => i t | ((g t = Lo) => Zz | Er)");;
60
61let Join = new_definition (
62	`Join`,
63	"Join (i1:^wire,i2:^wire,o:^wire) = !t. o t = (i1 t U i2 t)");;
64
65let Cap = new_definition (
66	`Cap`,
67	"Cap (i:^wire,o:^wire) = !t. o t = (~(i t = Zz)) => i t | i (t-1)");;
68
69close_theory ();;
70