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