1(* ===================================================================== *) 2(* 21 April 2018 - adapted to HOL 4 *) 3 4(* ===================================================================== *) 5(* 14 June 1989 - modified for HOL88 *) 6 7(* ===================================================================== *) 8(* Jeff Joyce, University of Cambridge, 1 November 1988 *) 9(* *) 10(* Derive results of executing individual microinstructions. *) 11 12 13open HolKernel boolLib bossLib Parse 14open proofManagerLib 15 16val _ = new_theory "tamarackProof1"; 17 18open arithmeticTheory stringTheory pairTheory prim_recTheory 19 20local 21 open tamarackTheory 22in 23end 24 25fun definition x y = SPEC_ALL (DB.fetch x y); 26 27val ADDn = definition "tamarack" "ADDn"; 28val Bits = definition "tamarack" "Bits"; 29val PWR = definition "tamarack" "PWR"; 30val GND = definition "tamarack" "GND"; 31val AND = definition "tamarack" "AND"; 32val OR = definition "tamarack" "OR"; 33val MUX = definition "tamarack" "MUX"; 34val BITS = definition "tamarack" "BITS"; 35val TNZ = definition "tamarack" "TNZ"; 36val HWC = definition "tamarack" "HWC"; 37val ADDER = definition "tamarack" "ADDER"; 38val ALU = definition "tamarack" "ALU"; 39val DEL = definition "tamarack" "DEL"; 40val REG = definition "tamarack" "REG"; 41val MEM = definition "tamarack" "MEM"; 42val CheckCntls = definition "tamarack" "CheckCntls"; 43val DataPath = definition "tamarack" "DataPath"; 44val Cntls = definition "tamarack" "Cntls"; 45val NextMpc = definition "tamarack" "NextMpc"; 46val Microcode = definition "tamarack" "Microcode"; 47val ROM = definition "tamarack" "ROM"; 48val Decoder = definition "tamarack" "Decoder"; 49val MpcUnit = definition "tamarack" "MpcUnit"; 50val CntlUnit = definition "tamarack" "CntlUnit"; 51val Tamarack = definition "tamarack" "Tamarack"; 52 53val LESS_MOD_THM = DB.fetch "arithmetic" "LESS_MOD"; 54val LESS_LESS_MONO = DECIDE ``!m n p q. (m < p) /\ (n < q) ==> ((m + n) < (p + q))``; 55val MOD_LESS_THM = DB.fetch "arithmetic" "MOD_LESS"; 56 57val MATCH_GOAL_TAC : thm_tactic = fn impthm => fn (asl,tm):goal => 58 let 59 val match = ((PART_MATCH (snd o dest_imp)) impthm) tm 60 in 61 ([(asl,fst (dest_imp (concl match)))],fn [th] => MP match th) 62 end handle HOL_ERR _ => failwith "MATCH_GOAL_TAC"; 63 64val PAIR_EQ_THM = store_thm ( 65 "PAIR_EQ_THM", 66 ``!a:'a. !b:'b. !c:'a. !d:'b. ((a,b) = (c,d)) = ((a = c) /\ (b = d))``, 67 REPEAT STRIP_TAC THEN 68 EQ_TAC THENL 69 [DISCH_THEN 70 (fn thm => 71 REWRITE_TAC [ 72 PURE_REWRITE_RULE [FST,SND] 73 (CONJ 74 (AP_TERM ``FST:('a # 'b)->'a`` thm) 75 (AP_TERM ``SND:('a # 'b)->'b`` thm))]), 76 DISCH_TAC THEN 77 ASM_REWRITE_TAC []]); 78 79fun not_eq_CONV tm = 80 if not (is_eq tm) then failwith "not_eq_CONV" else 81 let 82 val [n,m] = map numSyntax.int_of_term [rand (rator tm),rand tm] in 83 if m = n then failwith "not_eq_CONV" else 84 TAC_PROOF (([],``^tm = F``), 85 CONV_TAC (REDEPTH_CONV numLib.num_CONV) THEN 86 REWRITE_TAC [INV_SUC_EQ,numTheory.NOT_SUC]) 87 end; 88 89(* The two steps could take quite a long time ! *) 90 91val thlist1 = map 92 (fn n => 93 (REWRITE_RULE [] 94 (CONV_RULE (ONCE_DEPTH_CONV not_eq_CONV) 95 (REWRITE_RULE [] 96 (SPEC (numSyntax.term_of_int n) (GEN ``n:num`` Microcode)))))) 97 [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15]; 98 99val Microcode_THMS = map 100 ((REWRITE_RULE []) o 101 (CONV_RULE (ONCE_DEPTH_CONV stringLib.string_EQ_CONV)) o 102 (PURE_ONCE_REWRITE_RULE [Cntls,NextMpc])) 103 thlist1; 104 105val EXP_2_4 = 106 PURE_REWRITE_RULE [MULT_CLAUSES, ADD_CLAUSES] 107 (PURE_REWRITE_RULE [numLib.num_CONV ``1``, EXP] 108 ((REDEPTH_CONV numLib.num_CONV) ``2 EXP 4``)); 109 110(* The following tactics correspond to the sequence of steps which take 111 place when a microinstruction is executed: tac1 - produce microcode 112 ROM output; tac2 - generate next mpc state; tac3 - generate next data 113 path state. The last step, tac4, is used to simplify the mpc state. *) 114 115 116val tac1 = 117 PURE_REWRITE_TAC [Tamarack, CntlUnit, ROM] THEN 118 REPEAT STRIP_TAC THEN 119 IMP_RES_THEN (MP_TAC o (SPEC ``t:time``)) (fst (EQ_IMP_RULE Decoder)) THEN 120 PURE_ASM_REWRITE_TAC [] THEN 121 SUBST_TAC Microcode_THMS THEN 122 DISCH_THEN (STRIP_ASSUME_TAC o (PURE_REWRITE_RULE [PAIR_EQ_THM])); 123 124val tac2 = 125 IMP_RES_THEN MP_TAC (fst (EQ_IMP_RULE MpcUnit)) THEN 126 PURE_ONCE_REWRITE_TAC [AND,OR,MUX,HWC,ADDER,DEL] THEN 127 DISCH_THEN ((REPEAT_TCL CHOOSE_THEN) (fn thm => REWRITE_TAC [thm])) THEN 128 ASM_REWRITE_TAC []; 129 130val tac3 = 131 IMP_RES_THEN MP_TAC (fst (EQ_IMP_RULE DataPath)) THEN 132 PURE_ONCE_REWRITE_TAC [CheckCntls,MEM,REG,BITS,TNZ,ALU,PWR,GND] THEN 133 DISCH_THEN ((REPEAT_TCL CHOOSE_THEN) MP_TAC) THEN 134 DISCH_THEN (MP_TAC o LIST_CONJ o (map (SPEC ``t:time``)) o CONJUNCTS) THEN 135 ASM_REWRITE_TAC [PAIR_EQ_THM] THEN 136 DISCH_THEN 137 (fn thm => MP_TAC (REWRITE_RULE [CONJUNCT1 thm] (CONJUNCT2 thm))) THEN 138 STRIP_TAC THEN 139 ASM_REWRITE_TAC []; 140 141val tac4 = 142 REWRITE_TAC [ADDn] THEN 143 SUBST1_TAC EXP_2_4 THEN 144 CONV_TAC (REDEPTH_CONV numLib.num_CONV) THEN 145 PURE_REWRITE_TAC [ADD_CLAUSES] THEN 146 MATCH_GOAL_TAC LESS_MOD_THM THEN 147 REWRITE_TAC [LESS_MONO_EQ,LESS_0]; 148 149set_goal ([], 150 ``!n mpc mem mar pc acc ir arg buf. 151 Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) 152 ==> 153 !t. 154 (mpc t = 0) ==> 155 ((mpc (t+1),mem (t+1),mar (t+1),pc (t+1),acc (t+1)) = 156 (1,mem t,pc t,pc t,acc t))``); 157 158expandf (tac1 THEN tac2 THEN tac3); 159expandf tac4; 160 161val MPC_0_THM = save_thm ("MPC_0_THM",top_thm ()); 162val _ = drop(); 163 164set_goal ([], 165 ``!n mpc mem mar pc acc ir arg buf. 166 Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) 167 ==> 168 !t. 169 (mpc t = 1) ==> 170 ((mpc (t+1),mem (t+1),pc (t+1),acc (t+1),ir (t+1)) = 171 (2,mem t,pc t,acc t,mem t (Bits (0,n) (mar t))))``); 172 173expandf (tac1 THEN tac2 THEN tac3); 174expandf tac4; 175 176val MPC_1_THM = save_thm ("MPC_1_THM",top_thm()); 177 178set_goal ([], 179 ``!n mpc mem mar pc acc ir arg buf. 180 Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) 181 ==> 182 !t. 183 (mpc t = 2) ==> 184 ((mpc (t+1),mem (t+1),mar (t+1),pc (t+1),acc (t+1),ir (t+1)) = 185 ((Bits (n,3) (ir t)) + 3,mem t,ir t,pc t,acc t,ir t))``); 186 187expandf (tac1 THEN tac2 THEN tac3); 188 189val th1 = prove (``!n. 0 < (2 EXP n)``, 190 GEN_TAC >> 191 MP_TAC (SPECL [``n:num``, ``1``] ZERO_LESS_EXP) >> 192 SIMP_TAC arith_ss [] 193); 194 195val th2 = TAC_PROOF (([],``3 < (2 EXP 3)``), 196 CONV_TAC (REDEPTH_CONV numLib.num_CONV) THEN 197 PURE_REWRITE_TAC [numLib.num_CONV ``1``,EXP] THEN 198 PURE_REWRITE_TAC [MULT_CLAUSES,ADD_CLAUSES] THEN 199 REWRITE_TAC [LESS_MONO_EQ,LESS_0]); 200 201expandf (PURE_REWRITE_TAC [ADDn,Bits] THEN 202 MATCH_GOAL_TAC LESS_MOD_THM THEN 203 SUBST1_TAC (DEPTH_CONV numLib.num_CONV ``2 EXP 4``) THEN 204 PURE_REWRITE_TAC [EXP,MULT_CLAUSES,ADD_CLAUSES] THEN 205 SUBST1_TAC (SYM (numLib.num_CONV ``2``)) THEN 206 ASSUME_TAC 207 (SPEC ``(((ir:bus) t) DIV (2 EXP n))`` 208 (MATCH_MP MOD_LESS_THM (SPEC ``3`` th1))) THEN 209 ASSUME_TAC th2 THEN 210 PURE_ONCE_REWRITE_TAC [ADD_SYM] THEN 211 IMP_RES_TAC LESS_LESS_MONO); 212 213val MPC_2_THM = save_thm ("MPC_2_THM",top_thm()); 214 215set_goal ([], 216 ``!n mpc mem mar pc acc ir arg buf. 217 Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) 218 ==> 219 !t. 220 (mpc t = 3) ==> 221 ((mpc (t+1),mem (t+1),pc (t+1),acc (t+1),ir (t+1)) = 222 (((if ((acc t) = 0) then 4 else 10),mem t,pc t,acc t,ir t)))``); 223 224expandf (tac1 THEN tac2 THEN tac3); 225expandf (BOOL_CASES_TAC ``(acc:bus) t = 0`` THEN 226 tac4); 227 228val MPC_3_THM = save_thm ("MPC_3_THM",top_thm()); 229val _ = drop(); 230 231set_goal ([], 232 ``!n mpc mem mar pc acc ir arg buf. 233 Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) 234 ==> 235 !t. 236 (mpc t = 4) ==> 237 ((mpc (t+1),mem (t+1),pc (t+1),acc (t+1)) = 238 (0,mem t,ir t,acc t))``); 239 240expandf (tac1 THEN tac2 THEN tac3); 241expandf tac4; 242 243val MPC_4_THM = save_thm ("MPC_4_THM",top_thm()); 244val _ = drop(); 245 246set_goal ([], 247 ``!n mpc mem mar pc acc ir arg buf. 248 Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) 249 ==> 250 !t. 251 (mpc t = 5) ==> 252 ((mpc (t+1),mem (t+1),mar (t+1),pc (t+1),acc (t+1),arg (t+1)) = 253 (12,mem t,mar t,pc t,acc t,acc t))``); 254 255expandf (tac1 THEN tac2 THEN tac3); 256expandf tac4; 257 258val MPC_5_THM = save_thm ("MPC_5_THM",top_thm()); 259val _ = drop(); 260 261set_goal ([], 262 ``!n mpc mem mar pc acc ir arg buf. 263 Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) 264 ==> 265 !t. 266 (mpc t = 6) ==> 267 ((mpc (t+1),mem (t+1),mar (t+1),pc (t+1),acc (t+1),arg (t+1)) = 268 (13,mem t,mar t,pc t,acc t,acc t))``); 269 270expandf (tac1 THEN tac2 THEN tac3); 271expandf tac4; 272 273val MPC_6_THM = save_thm ("MPC_6_THM",top_thm()); 274val _ = drop(); 275 276set_goal ([], 277 ``!n mpc mem mar pc acc ir arg buf. 278 Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) 279 ==> 280 !t. 281 (mpc t = 7) ==> 282 ((mpc (t+1),mem (t+1),pc (t+1),acc (t+1)) = 283 (10,mem t,pc t,mem t (Bits (0,n) (mar t))))``); 284 285expandf (tac1 THEN tac2 THEN tac3); 286expandf tac4; 287 288val MPC_7_THM = save_thm ("MPC_7_THM",top_thm()); 289val _ = drop(); 290 291set_goal ([], 292 ``!n mpc mem mar pc acc ir arg buf. 293 Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) 294 ==> 295 !t. 296 (mpc t = 8) ==> 297 ((mpc (t+1),mem (t+1),pc (t+1),acc (t+1)) = 298 (10,Update (mem t,Bits (0,n) (mar t),acc t),pc t,acc t))``); 299 300expandf (tac1 THEN tac2 THEN tac3); 301expandf tac4; 302 303val MPC_8_THM = save_thm ("MPC_8_THM",top_thm ()); 304val _ = drop(); 305 306set_goal ([], 307 ``!n mpc mem mar pc acc ir arg buf. 308 Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) 309 ==> 310 !t. 311 (mpc t = 9) ==> 312 ((mpc (t+1),mem (t+1),pc (t+1),acc (t+1)) = 313 (10,mem t,pc t,acc t))``); 314 315expandf (tac1 THEN tac2 THEN tac3); 316expandf tac4; 317 318val MPC_9_THM = save_thm ("MPC_9_THM",top_thm ()); 319val _ = drop(); 320 321set_goal ([], 322 ``!n mpc mem mar pc acc ir arg buf. 323 Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) 324 ==> 325 !t. 326 (mpc t = 10) ==> 327 ((mpc (t+1),mem (t+1),pc (t+1),acc (t+1),buf (t+1)) = 328 (11,mem t,pc t,acc t,INCn (n+3) (pc t)))``); 329 330expandf (tac1 THEN tac2 THEN tac3); 331expandf tac4; 332 333val MPC_10_THM = save_thm ("MPC_10_THM",top_thm ()); 334val _ = drop(); 335 336set_goal ([], 337 ``!n mpc mem mar pc acc ir arg buf. 338 Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) 339 ==> 340 !t. 341 (mpc t = 11) ==> 342 ((mpc (t+1),mem (t+1),pc (t+1),acc (t+1)) = 343 (0,mem t,buf t,acc t))``); 344 345expandf (tac1 THEN tac2 THEN tac3); 346expandf tac4; 347 348val MPC_11_THM = save_thm ("MPC_11_THM",top_thm()); 349val _ = drop(); 350 351set_goal ([], 352 ``!n mpc mem mar pc acc ir arg buf. 353 Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) 354 ==> 355 !t. 356 (mpc t = 12) ==> 357 ((mpc (t+1),mem (t+1),pc (t+1),acc (t+1),buf (t+1)) = 358 (14,mem t,pc t,acc t, 359 ADDn (n+3) (arg t,mem t (Bits (0,n) (mar t)))))``); 360 361expandf (tac1 THEN tac2 THEN tac3); 362expandf tac4; 363 364val MPC_12_THM = save_thm ("MPC_12_THM",top_thm()); 365val _ = drop(); 366 367set_goal ([], 368 ``!n mpc mem mar pc acc ir arg buf. 369 Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) 370 ==> 371 !t. 372 (mpc t = 13) ==> 373 ((mpc (t+1),mem (t+1),pc (t+1),acc (t+1),buf (t+1)) = 374 (14,mem t,pc t,acc t, 375 SUBn (n+3) (arg t,mem t (Bits (0,n) (mar t)))))``); 376 377expandf (tac1 THEN tac2 THEN tac3); 378expandf tac4; 379 380val MPC_13_THM = save_thm ("MPC_13_THM",top_thm()); 381val _ = drop(); 382 383set_goal ([], 384 ``!n mpc mem mar pc acc ir arg buf. 385 Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) 386 ==> 387 !t. 388 (mpc t = 14) ==> 389 ((mpc (t+1),mem (t+1),pc (t+1),acc (t+1)) = 390 (10,mem t,pc t,buf t))``); 391 392expandf (tac1 THEN tac2 THEN tac3); 393expandf tac4; 394 395val MPC_14_THM = save_thm ("MPC_14_THM",top_thm()); 396val _ = drop(); 397 398val _ = export_theory (); 399