1% PROOF : Transistor Implementation of a Counter % 2% FILE : gates.ml % 3% % 4% DESCRIPTION : Defines CMOS implementations of basic gates used % 5% in the increment unit circuit and derives boolean % 6% behaviours. % 7% % 8% AUTHOR : J.Joyce % 9% DATE : 31 March 1987 % 10 11new_theory `gates`;; 12 13loadt `misc`;; 14loadt `types`;; 15 16new_parent `dataabs`;; 17 18let inv = new_definition (`inv`,"inv i = ~i");; 19let nand = new_definition (`nand`,"nand (i1,i2) = ~(i1 /\ i2)");; 20let and = new_definition (`and`,"and (i1,i2) = (i1 /\ i2)");; 21let xor = new_definition (`xor`,"xor (i1,i2) = (i1 /\ ~i2) \/ (~i1 /\ i2)");; 22 23let INV_IMP = new_definition ( 24 `INV_IMP`, 25 "INV_IMP (i:^wire,o:^wire) = 26 ?w1 w2 w3 w4. 27 Vdd (w1) /\ 28 Ptran (i,w1,w2) /\ 29 Join (w2,w3,o) /\ 30 Ntran (i,w4,w3) /\ 31 Gnd (w4)");; 32 33let NAND_IMP = new_definition ( 34 `NAND_IMP`, 35 "NAND_IMP (i1:^wire,i2:^wire,o:^wire) = 36 ?w1 w2 w3 w4 w5 w6 w7. 37 Vdd (w1) /\ 38 Ptran (i1,w1,w2) /\ 39 Ptran (i2,w1,w3) /\ 40 Join (w2,w3,w4) /\ 41 Join (w4,w5,o) /\ 42 Ntran (i1,w6,w5) /\ 43 Ntran (i2,w7,w6) /\ 44 Gnd (w7)");; 45 46let AND_IMP = new_definition ( 47 `AND_IMP`, 48 "AND_IMP (i1:^wire,i2:^wire,o:^wire) = 49 ?w. NAND_IMP (i1,i2,w) /\ INV_IMP (w,o)");; 50 51let XOR_IMP = new_definition ( 52 `XOR_IMP`, 53 "XOR_IMP (i1:^wire,i2:^wire,o:^wire) = 54 ?w1 w2 w3. 55 NAND_IMP (i1,i2,w1) /\ 56 NAND_IMP (i1,w1,w2) /\ 57 NAND_IMP (i2,w1,w3) /\ 58 NAND_IMP (w2,w3,o)");; 59 60let val_not_eq_ax = axiom `mos` `val_not_eq_ax`;; 61 62let U = definition `mos` `U`;; 63let Not = definition `mos` `Not`;; 64let Vdd = definition `mos` `Vdd`;; 65let Gnd = definition `mos` `Gnd`;; 66let Ptran = definition `mos` `Ptran`;; 67let Ntran = definition `mos` `Ntran`;; 68let Join = definition `mos` `Join`;; 69let Def = definition `dataabs` `Def`;; 70let BoolAbs_THM = theorem `dataabs` `BoolAbs_THM`;; 71let Def_DISJ_CASES = theorem `dataabs` `Def_DISJ_CASES`;; 72 73let INV_CORRECT = prove_thm ( 74 `INV_CORRECT`, 75 "!i o. 76 INV_IMP (i,o) 77 ==> 78 !t. 79 Def (i t) ==> 80 Def (o t) /\ (BoolAbs (o t) = inv (BoolAbs (i t)))", 81 let th1 = EXPANDF [Vdd;Gnd;Ptran;Ntran;Join] INV_IMP 82 in 83 PURE_REWRITE_TAC [th1] THEN 84 REPEAT STRIP_TAC THEN 85 PURE_REWRITE_TAC [Def] THEN 86 IMP_RES_TAC Def_DISJ_CASES THEN 87 ASM_REWRITE_TAC [val_not_eq_ax;U;BoolAbs_THM;inv]);; 88 89let NAND_CORRECT = prove_thm ( 90 `NAND_CORRECT`, 91 "!i1 i2 o. 92 NAND_IMP (i1,i2,o) 93 ==> 94 !t. 95 Def (i1 t) /\ Def (i2 t) ==> 96 Def (o t) /\ 97 (BoolAbs (o t) = nand (BoolAbs (i1 t),BoolAbs (i2 t)))", 98 let th1 = EXPANDF [Vdd;Gnd;Ptran;Ntran;Join] NAND_IMP 99 in 100 PURE_REWRITE_TAC [th1] THEN 101 REPEAT STRIP_TAC THEN 102 PURE_REWRITE_TAC [Def] THEN 103 IMP_RES_TAC Def_DISJ_CASES THEN 104 ASM_REWRITE_TAC [val_not_eq_ax;U;BoolAbs_THM;nand]);; 105 106let AND_CORRECT = prove_thm ( 107 `AND_CORRECT`, 108 "!i1 i2 o. 109 AND_IMP (i1,i2,o) 110 ==> 111 !t. 112 Def (i1 t) /\ Def (i2 t) ==> 113 Def (o t) /\ 114 (BoolAbs (o t) = and (BoolAbs (i1 t),BoolAbs (i2 t)))", 115 PURE_REWRITE_TAC [AND_IMP] THEN 116 REPEAT STRIP_TAC THEN 117 IMP_RES_TAC NAND_CORRECT THEN 118 RES_TAC THEN 119 IMP_RES_TAC INV_CORRECT THEN 120 RES_TAC THEN 121 ASM_REWRITE_TAC [nand;inv;and]);; 122 123let XOR_CORRECT = prove_thm ( 124 `XOR_CORRECT`, 125 "!i1 i2 o. 126 XOR_IMP (i1,i2,o) 127 ==> 128 !t. 129 Def (i1 t) /\ Def (i2 t) ==> 130 Def (o t) /\ 131 (BoolAbs (o t) = xor (BoolAbs (i1 t),BoolAbs (i2 t)))", 132 PURE_REWRITE_TAC [XOR_IMP] THEN 133 REPEAT STRIP_TAC THEN 134 IMP_RES_TAC NAND_CORRECT THEN 135 RES_TAC THEN 136 ASM_REWRITE_TAC [] THEN 137 BOOL_CASES_TAC "BoolAbs (i1 t)" THEN 138 BOOL_CASES_TAC "BoolAbs (i2 t)" THEN 139 REWRITE_TAC [nand;xor]);; 140 141close_theory ();; 142