1% PROOF : Transistor Implementation of a Counter % 2% FILE : muxn.ml % 3% % 4% DESCRIPTION : Defines a CMOS Mux and uses this to construct a % 5% n-bit Mux. Only the control line is abstracted % 6% to a boolean signal. % 7% % 8% AUTHOR : J.Joyce % 9% DATE : 31 March 1987 % 10 11new_theory `muxn`;; 12 13loadt `misc`;; 14loadt `types`;; 15 16new_parent `gates`;; 17 18let mux = new_definition (`mux`,"mux (cntl,i1:*,i2:*) = cntl => i1 | i2");; 19 20let CMUX_IMP = new_definition ( 21 `CMUX_IMP`, 22 "CMUX_IMP (cntl:^wire,cntlbar:^wire,i1:^wire,i2:^wire,o:^wire) = 23 ?w1 w2 w3 w4 w5 w6. 24 Ptran (cntlbar,i1,w1) /\ 25 Ntran (cntl,i1,w2) /\ 26 Join (w1,w2,w3) /\ 27 Join (w3,w4,o) /\ 28 Join (w5,w6,w4) /\ 29 Ptran (cntl,i2,w5) /\ 30 Ntran (cntlbar,i2,w6)");; 31 32let CMUXn_IMP = new_definition ( 33 `CMUXn_IMP`, 34 "CMUXn_IMP n (cntl:^wire,cntlbar:^wire,i1:^bus,i2:^bus,o:^bus) = 35 !m. m <= n ==> 36 CMUX_IMP 37 (cntl,cntlbar,DEST_BUS i1 m,DEST_BUS i2 m,DEST_BUS o m)");; 38 39let MUXn_IMP = new_definition ( 40 `MUXn_IMP`, 41 "MUXn_IMP n (cntl:^wire,i1:^bus,i2:^bus,o:^bus) = 42 ?cntlbar. 43 INV_IMP (cntl,cntlbar) /\ CMUXn_IMP n (cntl,cntlbar,i1,i2,o)");; 44 45let U = definition `mos` `U`;; 46let Vdd = definition `mos` `Vdd`;; 47let Gnd = definition `mos` `Gnd`;; 48let Ptran = definition `mos` `Ptran`;; 49let Ntran = definition `mos` `Ntran`;; 50let Join = definition `mos` `Join`;; 51let Not = definition `mos` `Not`;; 52let Def = definition `dataabs` `Def`;; 53let DEST_BUS = definition `dataabs` `DEST_BUS`;; 54let INV_IMP = definition `gates` `INV_IMP`;; 55 56let val_not_eq_ax = axiom `mos` `val_not_eq_ax`;; 57 58let Def_DISJ_CASES = theorem `dataabs` `Def_DISJ_CASES`;; 59let BoolAbs_THM = theorem `dataabs` `BoolAbs_THM`;; 60let isBus_THM = theorem `dataabs` `isBus_THM`;; 61 62let lemma1 = TAC_PROOF (( 63 [], 64 "(!t1:*. !t2:*. (((t1 = t2) => t1 | t1) = t1)) /\ 65 (!t1:*. !t2:*. (((t1 = t2) => t2 | t2) = t2)) /\ 66 (!t1:*. !t2:*. (((t1 = t2) => t1 | t2) = t2)) /\ 67 (!t1:*. !t2:*. (((t1 = t2) => t2 | t1) = t1))"), 68 let thm = SYM (CONJUNCT2(CONJUNCT2(CONJUNCT2 (SPEC_ALL EQ_CLAUSES)))) 69 in 70 REPEAT STRIP_TAC THEN 71 DISJ_CASES_TAC (SPEC "t1 = t2" EXCLUDED_MIDDLE) THEN 72 IMP_RES_TAC thm THEN 73 ASM_REWRITE_TAC []);; 74 75let CMUX_CORRECT = prove_thm ( 76 `CMUX_CORRECT`, 77 "!cntl cntlbar i1 i2 o. 78 CMUX_IMP (cntl,cntlbar,i1,i2,o) 79 ==> 80 !t. 81 Def (cntl t) /\ (cntlbar t = Not (cntl t)) 82 ==> 83 (o t = mux (BoolAbs (cntl t),i1 t,i2 t))", 84 PURE_REWRITE_TAC [EXPANDF [Ptran;Ntran;Join] CMUX_IMP] THEN 85 REPEAT STRIP_TAC THEN 86 IMP_RES_TAC Def_DISJ_CASES THEN 87 ASM_REWRITE_TAC [Not;mux;U;val_not_eq_ax;BoolAbs_THM;lemma1]);; 88 89let CMUXn_CORRECT = prove_thm ( 90 `CMUXn_CORRECT`, 91 "!n cntl cntlbar i1 i2 o. 92 CMUXn_IMP n (cntl,cntlbar,i1,i2,o) /\ 93 isBus n i1 /\ 94 isBus n i2 /\ 95 isBus n o 96 ==> 97 !t. 98 Def (cntl t) /\ (cntlbar t = Not (cntl t)) 99 ==> 100 (o t = mux (BoolAbs (cntl t),i1 t,i2 t))", 101 PURE_REWRITE_TAC [CMUXn_IMP;mux] THEN 102 REPEAT STRIP_TAC THEN 103 COND_CASES_TAC THEN 104 IMP_RES_TAC isBus_THM THEN 105 ASM_REWRITE_TAC [] THEN 106 REPEAT STRIP_TAC THEN 107 RES_TAC THEN 108 HOL_IMP_RES_THEN 109 (ASSUME_TAC o BETA_RULE o PURE_REWRITE_RULE [DEST_BUS]) 110 CMUX_CORRECT THEN 111 RES_TAC THEN 112 ASM_REWRITE_TAC [mux]);; 113 114let th1 = TAC_PROOF ( 115 ([],"!i o. INV_IMP (i,o) ==> !t. Def (i t) ==> (o t = Not (i t))"), 116 PURE_REWRITE_TAC [EXPANDF [Vdd;Gnd;Ptran;Ntran;Join] INV_IMP] THEN 117 REPEAT STRIP_TAC THEN 118 IMP_RES_TAC Def_DISJ_CASES THEN 119 ASM_REWRITE_TAC [Not;U;val_not_eq_ax]);; 120 121let MUXn_CORRECT = prove_thm ( 122 `MUXn_CORRECT`, 123 "!n cntl i1 i2 o. 124 MUXn_IMP n (cntl,i1,i2,o) /\ 125 isBus n i1 /\ 126 isBus n i2 /\ 127 isBus n o 128 ==> 129 !t. Def (cntl t) ==> (o t = mux (BoolAbs (cntl t),i1 t,i2 t))", 130 PURE_REWRITE_TAC [MUXn_IMP] THEN 131 REPEAT STRIP_TAC THEN 132 IMP_RES_TAC th1 THEN 133 IMP_RES_TAC CMUXn_CORRECT THEN 134 RES_TAC);; 135 136close_theory ();; 137