1% PROOF : Transistor Implementation of a Counter % 2% FILE : clock.ml % 3% % 4% DESCRIPTION : Defines predicates for a very simple version of % 5% two phase non-overlapping clocking and derives % 6% theorems about the clock behaviour. The theory % 7% also uses the temporal abstraction theory to derive % 8% two major theorems for temporal abstraction on any % 9% of the four phases of the clock. % 10% % 11% These definitions of a two phase non-overlapping % 12% clock are taken from I. Dhingra's paper, "Formal % 13% Validation of an Integrated Circuit Design Style", % 14% Hardware Verification Workshop, University of % 15% Calgary, January 1987. % 16% % 17% AUTHOR : J.Joyce % 18% DATE : 31 March 1987 % 19 20new_theory `clock`;; 21 22loadt `misc`;; 23loadt `types`;; 24 25new_parent `da`;; 26new_parent `mos`;; 27new_parent `tempabs`;; 28 29let Shift = new_definition ( 30 `Shift`, 31 "Shift (phi1:^wire) (phi2:^wire) = !t. phi2 (t+2) = phi1 t");; 32 33let Invert = new_definition ( 34 `Invert`, 35 "Invert (phi:^wire) (phibar:^wire) = !t. phibar t = Not (phi t)");; 36 37let Cycle1 = new_definition ( 38 `Cycle1`, 39 "Cycle1 (phi:^wire) (t:^time) = 40 (phi t = Hi) /\ (phi (t+1) = Lo) /\ 41 (phi (t+2) = Lo) /\ (phi (t+3) = Lo)");; 42 43let Cycle = new_definition ( 44 `Cycle`, 45 "Cycle (phi:^wire) = 46 ((!t. phi (t+4) = phi t) /\ 47 (Cycle1 phi 0 \/ 48 Cycle1 phi 1 \/ Cycle1 phi 2 \/ Cycle1 phi 3))");; 49 50let Clock = new_definition ( 51 `Clock`, 52 "Clock (phi1:^wire,phi1bar:^wire,phi2:^wire,phi2bar:^wire) = 53 Cycle phi1 /\ Shift phi1 phi2 /\ 54 Invert phi1 phi1bar /\ Invert phi2 phi2bar");; 55 56let isHi = new_definition (`isHi`,"isHi phi t = (phi t = Hi)");; 57 58let Not = definition `mos` `Not`;; 59let Inf = definition `tempabs` `Inf`;; 60let val_not_eq_ax = axiom `mos` `val_not_eq_ax`;; 61 62let DA = theorem `da` `DA`;; 63let Next_ADD1 = theorem `tempabs` `Next_ADD1`;; 64let Next_INCREASE = theorem `tempabs` `Next_INCREASE`;; 65let Next_IDENTITY = theorem `tempabs` `Next_IDENTITY`;; 66let TimeOf_TRUE = theorem `tempabs` `TimeOf_TRUE`;; 67let TimeOf_Next = theorem `tempabs` `TimeOf_Next`;; 68 69let DISJ_ASSOC = TAC_PROOF ( 70 ([],"!t1 t2 t3. t1 \/ t2 \/ t3 = (t1 \/ t2) \/ t3"), 71 REPEAT GEN_TAC THEN 72 BOOL_CASES_TAC "t1" THEN REWRITE_TAC [] ORELSE 73 BOOL_CASES_TAC "t2" THEN REWRITE_TAC [] ORELSE 74 BOOL_CASES_TAC "t3" THEN REWRITE_TAC []);; 75 76% lemma1 = [Cycle phi] |- !t. phi(SUC(SUC(SUC(SUC t)))) = phi t % 77let lemma1 = SUC_FORM_RULE (CONJUNCT1 (UNDISCH (fst (EQ_IMP_RULE Cycle))));; 78 79let lemma2 = 80 PURE_REWRITE_RULE [lemma1] 81 (SUC_FORM_RULE 82 (PURE_REWRITE_RULE [Cycle1] 83 (CONJUNCT2 (UNDISCH (fst (EQ_IMP_RULE Cycle))))));; 84 85let lemma3 = TAC_PROOF ( 86 ([],"!phi. Cycle phi ==> !t. (Cycle1 phi (t+4) = Cycle1 phi t)"), 87 REPEAT STRIP_TAC THEN 88 PURE_REWRITE_TAC [Cycle1] THEN 89 PURE_REWRITE_TAC [SYM (SPECL ["t";"4";"m"] ADD_ASSOC)] THEN 90 PURE_REWRITE_TAC [SPECL ["4";"m"] ADD_SYM] THEN 91 PURE_REWRITE_TAC [ADD_ASSOC] THEN 92 REWRITE_TAC [CONJUNCT1 (UNDISCH (fst (EQ_IMP_RULE Cycle)))]);; 93 94let th1 = TAC_PROOF ( 95 ([],"0 < 4"), 96 SUC_FORM_TAC THEN 97 ASSUME_TAC (SPEC "0" LESS_0) THEN 98 REPEAT (FIRST [FIRST_ASSUM ACCEPT_TAC;IMP_RES_TAC LESS_SUC]));; 99 100let th2 = TAC_PROOF ( 101 ([],"!m. m < 4 ==> ((m = 0) \/ (m = 1) \/ (m = 2) \/ (m = 3))"), 102 let thm = 103 GEN_ALL (SYM 104 (SUBS [SPECL ["m = n";"m < n"] DISJ_SYM] (SPEC_ALL LESS_THM))) 105 in 106 REPEAT STRIP_TAC THEN 107 PURE_REWRITE_TAC [DISJ_ASSOC] THEN 108 PURE_REWRITE_TAC 109 [GEN_ALL (REWRITE_RULE [NOT_LESS_0] (SPECL ["m";"0"] thm))] THEN 110 PURE_REWRITE_TAC [thm;SYM (num_CONV "1")] THEN 111 PURE_REWRITE_TAC [thm;SYM (num_CONV "2")] THEN 112 PURE_REWRITE_TAC [thm;SYM (num_CONV "3")] THEN 113 ASM_REWRITE_TAC [SYM (num_CONV "4")]);; 114 115% th3 = |- !m n p. (m + n) + p = (m + p) + n % 116let th3 = 117 GEN_ALL 118 ((SUBS [SPECL ["n";"p"] ADD_SYM] (SYM (SPEC_ALL ADD_ASSOC))) 119 TRANS (SPECL ["m";"p";"n"] ADD_ASSOC));; 120 121let Cycle1_ALWAYS = prove_thm ( 122 `Cycle1_ALWAYS`, 123 "!phi. 124 Cycle phi 125 ==> 126 !t. 127 Cycle1 phi t \/ 128 Cycle1 phi (t+1) \/ 129 Cycle1 phi (t+2) \/ 130 Cycle1 phi (t+3)", 131 GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN 132 STRIP_ASSUME_TAC 133 (MP (SPECL ["t";"4"] DA) 134 (NOT_EQ_SYM (MATCH_MP LESS_NOT_EQ th1))) THEN 135 SUBST1_TAC (ASSUME "t = (q * 4) + r") THEN 136 SPEC_TAC ("q:num","q':num") THEN 137 INDUCT_TAC THENL 138 [PURE_REWRITE_TAC [MULT_CLAUSES;ADD_CLAUSES] THEN 139 PURE_REWRITE_TAC [Cycle1] THEN 140 SUC_FORM_TAC THEN 141 IMP_RES_TAC th2 THENL 142 (map (\tm. SUBST1_TAC (ASSUME "r = ^tm")) ["0";"1";"2";"3"]) THEN 143 SUC_FORM_TAC THEN 144 PURE_REWRITE_TAC [lemma1] THEN 145 IMP_RES_TAC (DISCH_ALL lemma2) THEN 146 ASM_REWRITE_TAC []; % 16 cases % 147 PURE_REWRITE_TAC [MULT_CLAUSES] THEN 148 PURE_REWRITE_TAC [SPECL ["m";"4";"n"] th3] THEN 149 IMP_RES_THEN (\thm. ASM_REWRITE_TAC [thm]) lemma3]);; 150 151let th1 = 152 REWRITE_RULE 153 [lemma1;ASSUME "phi t = Hi";val_not_eq_ax] 154 (SUC_FORM_RULE 155 (PURE_REWRITE_RULE [Cycle1] 156 (SPEC_ALL (UNDISCH_ALL (SPEC_ALL Cycle1_ALWAYS)))));; 157 158let isHi_Cycle1_ALWAYS = prove_thm ( 159 `isHi_Cycle1_ALWAYS`, 160 "!phi t. (Cycle phi /\ isHi phi t) ==> Cycle1 phi t", 161 PURE_REWRITE_TAC [isHi;Cycle1] THEN 162 REPEAT GEN_TAC THEN DISCH_THEN STRIP_ASSUME_TAC THEN 163 SUC_FORM_TAC THEN 164 ASM_REWRITE_TAC [th1]);; 165 166let num_CONVs = map num_CONV ["1";"2";"3";"4"];; 167let th1 = SUC_FORM_RULE (PURE_REWRITE_RULE [Cycle1] Cycle1_ALWAYS);; 168 169let Cycle_Inf = prove_thm ( 170 `Cycle_Inf`, 171 "!phi. Cycle phi ==> Inf (isHi phi)", 172 PURE_REWRITE_TAC [Inf;isHi;GREATER] THEN 173 REPEAT STRIP_TAC THEN 174 ASSUME_TAC (SPEC "t" LESS_SUC_REFL) THEN 175 IMP_RES_TAC LESS_SUC THEN 176 IMP_RES_TAC LESS_SUC THEN 177 IMP_RES_TAC LESS_SUC THEN 178 IMP_RES_TAC (hd (IMP_CANON th1)) THENL 179 (map EXISTS_TAC ["t+4";"t+1";"t+2";"t+3"]) THEN 180 ASM_REWRITE_TAC (num_CONVs @ [ADD_CLAUSES;lemma1]));; 181 182let TimeOf_isHi_TRUE = prove_thm ( 183 `TimeOf_isHi_TRUE`, 184 "!phi. Cycle phi ==> !n. (isHi phi) (TimeOf (isHi phi) n)", 185 GEN_TAC THEN DISCH_TAC THEN 186 IMP_RES_TAC Cycle_Inf THEN IMP_RES_TAC TimeOf_TRUE);; 187 188let TimeOf_isHi_Next = prove_thm ( 189 `TimeOf_isHi_Next`, 190 "!phi. 191 Cycle phi ==> 192 !n. Next (TimeOf (isHi phi) n,TimeOf (isHi phi) (n+1)) (isHi phi)", 193 REPEAT STRIP_TAC THEN 194 IMP_RES_TAC Cycle_Inf THEN IMP_RES_TAC TimeOf_Next);; 195 196% th1 = .. |- phi(SUC(SUC(SUC(SUC t)))) = Hi % 197let th1 = SUBS [SYM (SPEC "t" lemma1)] (ASSUME "phi t = Hi");; 198let th2 = TAC_PROOF ( 199 ([],"!phi t. (phi t = Lo) ==> ~(phi t = Hi)"), 200 REPEAT GEN_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC [val_not_eq_ax]);; 201let th3 = 202 SUC_FORM_RULE 203 (PURE_REWRITE_RULE [isHi] (SPEC "isHi phi" Next_ADD1));; 204let th4 = 205 SUC_FORM_RULE 206 (PURE_REWRITE_RULE [isHi] (SPEC "isHi phi" Next_INCREASE));; 207 208let isHi_Next_plus4 = prove_thm ( 209 `isHi_Next_plus4`, 210 "!phi t. (Cycle phi /\ isHi phi t) ==> Next (t,t+4) (isHi phi)", 211 REPEAT STRIP_TAC THEN 212 SUC_FORM_TAC THEN 213 IMP_RES_TAC 214 (SUC_FORM_RULE (PURE_REWRITE_RULE [Cycle1] isHi_Cycle1_ALWAYS)) THEN 215 ASSUME_TAC th1 THEN 216 IMP_RES_TAC th2 THEN 217 IMP_RES_TAC th3 THEN 218 IMP_RES_TAC th4 THEN 219 IMP_RES_TAC th4 THEN 220 IMP_RES_TAC th4);; 221 222let TimeOf_isHi_Next_plus4 = prove_thm ( 223 `TimeOf_isHi_Next_plus4`, 224 "!phi. 225 Cycle phi ==> 226 !n. Next (TimeOf (isHi phi) n,(TimeOf (isHi phi) n)+4) (isHi phi)", 227 REPEAT STRIP_TAC THEN 228 ASSUME_TAC 229 (SPEC "n" (MATCH_MP TimeOf_isHi_TRUE (ASSUME "Cycle phi"))) THEN 230 IMP_RES_TAC isHi_Next_plus4);; 231 232let TimeOf_isHi_plus4 = prove_thm ( 233 `TimeOf_isHi_plus4`, 234 "!phi. 235 Cycle phi ==> 236 !n. (TimeOf (isHi phi) (n+1) = (TimeOf (isHi phi) n)+4)", 237 REPEAT STRIP_TAC THEN 238 ASSUME_TAC 239 (SPEC "n" (MATCH_MP TimeOf_isHi_Next (ASSUME "Cycle phi"))) THEN 240 ASSUME_TAC 241 (SPEC "n" 242 (MATCH_MP TimeOf_isHi_Next_plus4 (ASSUME "Cycle phi"))) THEN 243 IMP_RES_TAC Next_IDENTITY);; 244 245let th1 = 246 SUC_FORM_RULE 247 (PURE_REWRITE_RULE [Cycle1] (ASSUME "Cycle1 phi1 t"));; 248let th2 = 249 SUC_FORM_RULE 250 (SUBS (CONJUNCTS th1) 251 (SPEC "t" 252 (CONJUNCT1 253 (PURE_REWRITE_RULE [Cycle] (ASSUME "Cycle phi1")))));; 254let th3 = PURE_REWRITE_RULE [Invert] (ASSUME "Invert phi1 phi1bar");; 255let th4 = PURE_REWRITE_RULE [Invert] (ASSUME "Invert phi2 phi2bar");; 256let th5 = 257 SUC_FORM_RULE 258 (PURE_REWRITE_RULE [Shift] (ASSUME "Shift phi1 phi2"));; 259 260let ClockSignals = prove_thm ( 261 `ClockSignals`, 262 "!phi1 phi1bar phi2 phi2bar t. 263 (Clock (phi1,phi1bar,phi2,phi2bar) /\ (isHi phi1 t)) 264 ==> 265 (phi1 t = Hi) /\ (phi1 (t+1) = Lo) /\ 266 (phi1 (t+2) = Lo) /\ (phi1 (t+3) = Lo) /\ 267 (phi1 (t+4) = Hi) /\ 268 (phi1bar (t+1) = Hi) /\ (phi1bar (t+2) = Hi) /\ 269 (phi1bar (t+3) = Hi) /\ (phi1bar (t+4) = Lo) /\ 270 (phi2 (t+2) = Hi) /\ (phi2 (t+3) = Lo) /\ 271 (phi2 (t+4) = Lo) /\ 272 (phi2bar (t+3) = Hi) /\ (phi2bar (t+4) = Hi)", 273 PURE_REWRITE_TAC [Clock] THEN 274 REPEAT GEN_TAC THEN DISCH_THEN STRIP_ASSUME_TAC THEN 275 IMP_RES_TAC isHi_Cycle1_ALWAYS THEN 276 SUC_FORM_TAC THEN 277 REWRITE_TAC [th1;th2;th3;th4;th5;Not;val_not_eq_ax]);; 278% 279|- !phi1 phi1bar phi2 phi2bar. 280 Clock(phi1,phi1bar,phi2,phi2bar) ==> Cycle phi1 281% 282let Clock_Cycle = save_thm ( 283 `Clock_Cycle`, 284 GEN_ALL (DISCH_ALL (CONJUNCT1 (UNDISCH (fst (EQ_IMP_RULE Clock))))));; 285 286close_theory ();; 287