1% PROOF : Transistor Implementation of a Counter % 2% FILE : count.ml % 3% % 4% DESCRIPTION : Top-level implementation of the counter with three % 5% different correctness statements. % 6% % 7% AUTHOR : J.Joyce % 8% DATE : 1 April 1987 % 9 10new_theory `count`;; 11 12loadt `misc`;; 13loadt `types`;; 14 15new_parent `regn`;; 16new_parent `muxn`;; 17new_parent `incn`;; 18 19let COUNT_IMP = new_definition ( 20 `COUNT_IMP`, 21 "COUNT_IMP n (phiA:^wire,reset:^wire,in:^bus,out:^bus) = 22 ?phiAbar phiB phiBbar b1 b2. 23 Clock (phiA,phiAbar,phiB,phiBbar) /\ 24 REGn_IMP n (phiA,phiB,b1,out) /\ 25 MUXn_IMP n (reset,in,b2,b1) /\ 26 INCn_IMP n (out,b2) /\ 27 isBus n b1 /\ 28 isBus n b2");; 29 30let when = definition `tempabs` `when`;; 31let mux = definition `muxn` `mux`;; 32 33let BoolAbs_THM = theorem `dataabs` `BoolAbs_THM`;; 34let REGn_CORRECT = theorem `regn` `REGn_CORRECT`;; 35let MUXn_CORRECT = theorem `muxn` `MUXn_CORRECT`;; 36let INCn_CORRECT = theorem `incn` `INCn_CORRECT`;; 37 38let LESS_OR_EQ_ADD = TAC_PROOF( 39 ([],"!m n. m <= n = (?p. p + m = n)"), 40 REPEAT GEN_TAC THEN 41 EQ_TAC THENL 42 [PURE_REWRITE_TAC [LESS_OR_EQ] THEN 43 REPEAT STRIP_TAC THENL 44 [IMP_RES_TAC LESS_ADD; 45 EXISTS_TAC "0" THEN ASM_REWRITE_TAC [ADD_CLAUSES]]; 46 REPEAT STRIP_TAC THEN 47 FIRST_ASSUM (SUBST1_TAC o SYM) THEN 48 SUBST1_TAC (SPECL ["p";"m"] ADD_SYM) THEN 49 REWRITE_TAC [LESS_EQ_ADD]]);; 50 51 52% =========================================== % 53% Basic Behaviour disregarding initialization % 54 55let COUNT_CORRECT1 = prove_thm ( 56 `COUNT_CORRECT1`, 57 "!n clk reset inp out. 58 COUNT_IMP n (clk,reset,inp,out) /\ 59 isBus n inp /\ 60 isBus n out 61 ==> 62 !t. 63 Def ((reset when (isHi clk)) t) /\ 64 Defn n ((inp when (isHi clk)) t) /\ 65 (((reset when (isHi clk)) t = Hi) \/ 66 (Defn n ((out when (isHi clk)) t))) 67 ==> 68 Defn n ((out when (isHi clk)) (t+1)) /\ 69 (WordVal n (WordAbs ((out when (isHi clk)) (t+1))) = 70 (BoolAbs ((reset when (isHi clk)) t) => 71 (WordVal n (WordAbs ((inp when (isHi clk)) t))) | 72 (((WordVal n (WordAbs ((out when (isHi clk)) t))) + 1) 73 MOD (2 EXP (SUC n)))))", 74 let REGn_thm = (BETA_RULE (PURE_REWRITE_RULE [when] REGn_CORRECT)) 75 in 76 PURE_REWRITE_TAC [COUNT_IMP;when] THEN 77 BETA_TAC THEN 78 REPEAT STRIP_TAC THEN 79 IMP_RES_TAC REGn_thm THEN 80 IMP_RES_TAC MUXn_CORRECT THEN 81 IMP_RES_TAC INCn_CORRECT THEN 82 ASM_REWRITE_TAC [mux] THENL 83 [ASM_REWRITE_TAC [BoolAbs_THM]; 84 ASM_REWRITE_TAC [BoolAbs_THM]; 85 COND_CASES_TAC THEN ASM_REWRITE_TAC [BoolAbs_THM]; 86 COND_CASES_TAC THEN ASM_REWRITE_TAC [BoolAbs_THM]]);; 87 88% ================================================== % 89% Behaviour plus proper initialization at some point % 90 91let th1 = CONJUNCT1 (CONJUNCT2 (CONJUNCT2 ADD_CLAUSES));; 92let th2 = (DEPTH_CONV (REWRITE_CONV th1)) "((SUC p) + sysinit)";; 93let th3 = SYM (TRANS th2 ((REWRITE_CONV ADD1) (rhs (concl th2))));; 94 95let COUNT_CORRECT2 = prove_thm ( 96 `COUNT_CORRECT2`, 97 "!n clk reset inp out. 98 COUNT_IMP n (clk,reset,inp,out) /\ 99 isBus n inp /\ 100 isBus n out /\ 101 (!t. Def ((reset when (isHi clk)) t)) /\ 102 (!t. Defn n ((inp when (isHi clk)) t)) 103 ==> 104 !sysinit. 105 ((reset when (isHi clk)) sysinit = Hi) 106 ==> 107 !t. sysinit <= t ==> 108 Defn n ((out when (isHi clk)) (t+1)) /\ 109 (WordVal n (WordAbs ((out when (isHi clk)) (t+1))) = 110 (BoolAbs ((reset when (isHi clk)) t) => 111 (WordVal n (WordAbs ((inp when (isHi clk)) t))) | 112 (((WordVal n (WordAbs ((out when (isHi clk)) t))) + 1) 113 MOD (2 EXP (SUC n)))))", 114 PURE_REWRITE_TAC [LESS_OR_EQ_ADD] THEN 115 REPEAT GEN_TAC THEN STRIP_TAC THEN 116 GEN_TAC THEN STRIP_TAC THEN GEN_TAC THEN 117 DISCH_THEN (STRIP_THM_THEN (SUBST1_TAC o SYM)) THEN 118 SPEC_TAC ("p","p") THEN 119 INDUCT_TAC THENL 120 [PURE_REWRITE_TAC [ADD_CLAUSES] THEN 121 ASSUM_LIST (MAP_EVERY 122 (\thm. if (is_forall (concl thm)) 123 then (ASSUME_TAC (SPEC "sysinit" thm)) else ALL_TAC)) THEN 124 IMP_RES_TAC COUNT_CORRECT1 THEN 125 RES_TAC THEN 126 ASM_REWRITE_TAC []; 127 ASSUM_LIST (MAP_EVERY 128 (\thm. if (is_forall (concl thm)) 129 then (ASSUME_TAC (SPEC "(SUC p) + sysinit" thm)) 130 else ALL_TAC)) THEN 131 ASSUM_LIST (MAP_EVERY 132 (\thm. if (is_conj (concl thm)) 133 then (ASSUME_TAC (SUBS [th3] (CONJUNCT1 thm))) 134 else ALL_TAC)) THEN 135 IMP_RES_TAC COUNT_CORRECT1 THEN 136 RES_TAC THEN 137 ASM_REWRITE_TAC []]);; 138 139% ========================================================== % 140% Similar to COUNT_CORRECT2 but weaker assumptions on inputs % 141 142let COUNT_CORRECT3 = prove_thm ( 143 `COUNT_CORRECT3`, 144 "!n clk reset inp out. 145 COUNT_IMP n (clk,reset,inp,out) /\ 146 isBus n inp /\ 147 isBus n out 148 ==> 149 !sysinit. 150 (!t. sysinit <= t ==> Def ((reset when (isHi clk)) t)) /\ 151 (!t. sysinit <= t ==> Defn n ((inp when (isHi clk)) t)) /\ 152 ((reset when (isHi clk)) sysinit = Hi) 153 ==> 154 !t. sysinit <= t ==> 155 Defn n ((out when (isHi clk)) (t+1)) /\ 156 (WordVal n (WordAbs ((out when (isHi clk)) (t+1))) = 157 (BoolAbs ((reset when (isHi clk)) t) => 158 (WordVal n (WordAbs ((inp when (isHi clk)) t))) | 159 (((WordVal n (WordAbs ((out when (isHi clk)) t))) + 1) 160 MOD (2 EXP (SUC n)))))", 161 REPEAT GEN_TAC THEN STRIP_TAC THEN 162 GEN_TAC THEN STRIP_TAC THEN GEN_TAC THEN 163 PURE_REWRITE_TAC [LESS_OR_EQ_ADD] THEN 164 DISCH_THEN (STRIP_THM_THEN (SUBST1_TAC o SYM)) THEN 165 SPEC_TAC ("p","p") THEN 166 INDUCT_TAC THENL 167 [PURE_REWRITE_TAC [ADD_CLAUSES] THEN 168 ASSUME_TAC (SPEC "sysinit" LESS_EQ_REFL) THEN 169 RES_TAC THEN 170 IMP_RES_TAC COUNT_CORRECT1 THEN 171 RES_TAC THEN 172 ASM_REWRITE_TAC []; 173 ASSUME_TAC 174 (SUBS [SPECL ["sysinit";"SUC p"] ADD_SYM] 175 (SPECL ["sysinit";"SUC p"] LESS_EQ_ADD)) THEN 176 RES_TAC THEN 177 ASSUM_LIST (MAP_EVERY 178 (\thm. if (is_conj (concl thm)) 179 then (ASSUME_TAC (SUBS [th3] (CONJUNCT1 thm))) 180 else ALL_TAC)) THEN 181 IMP_RES_TAC COUNT_CORRECT1 THEN 182 RES_TAC THEN 183 ASM_REWRITE_TAC []]);; 184 185close_theory ();; 186