1(* ===================================================================== *) 2(* April 2018 - Updated to HOL 4, Ramana Kumar, Thomas Tuerk *) 3 4(* ===================================================================== *) 5(* 14 June 1989 - modified for HOL88 *) 6(* *) 7(* ===================================================================== *) 8(* Jeff Joyce, University of Cambridge, 1 November 1988 *) 9(* *) 10(* Specify register-transfer level implementation and functional *) 11(* behaviour of a very simple microprocessor. *) 12 13open HolKernel boolLib bossLib Parse 14 15open arithmeticTheory stringTheory 16 17val _ = new_theory "tamarack"; 18 19(* ----------------------------- *) 20(* - Definitions - *) 21(* ----------------------------- *) 22 23val _ = type_abbrev ("time",``:num``); 24val _ = type_abbrev ("wire",``:time->bool``); 25val _ = type_abbrev ("bus",``:time->num``); 26val _ = type_abbrev ("mem",``:time->num->num``); 27 28val INCn_def = Define `INCn n a = (a + 1) MOD (2 EXP n)`; 29val SUBn_def = Define `SUBn n (a,b) = (a + b) MOD (2 EXP n)`; 30val ADDn_def = Define `ADDn n (a,b) = (a + b) MOD (2 EXP n)`; 31 32val Bits_def = Define `Bits (n,m) w = ((w DIV (2 EXP n)) MOD (2 EXP m))`; 33 34val Update_def = Define `Update (s:'a->'b,x,y) = (x =+ y) s`; 35 36val PWR_def = Define `PWR (w:wire) = !t. w t = T`; 37 38val GND_def = Define `GND (w:wire) = !t. w t = F`; 39 40val AND_def = Define `AND (a:wire,b:wire,out:wire) = !t. out t = a t /\ b t`; 41 42val OR_def = Define `OR (a:wire,b:wire,out:wire) = !t. out t = a t \/ b t`; 43 44val MUX_def = Define `MUX (cntl:wire,a:bus,b:bus,out:bus) = 45 !t. out t = (if cntl t then b t else a t)`; 46 47val BITS_def = Define `BITS (n,m) (inp:bus,out:bus) = !t. out t = Bits (n,m) (inp t)`; 48 49val TNZ_def = Define `TNZ (inp:bus,flag:wire) = !t. flag t = ~(inp t = 0)`; 50 51val HWC_def = Define `HWC c (b:bus) = !t. b t = c`; 52 53val ADDER_def = Define `ADDER n (a:bus,b:bus,out:bus) = !t. out t = ADDn n (a t,b t)`; 54 55val ALU_def = Define `ALU n (f0:wire,f1:wire,a:bus,b:bus,out:bus) = 56 !t. 57 ?w. 58 out t = 59 (if ((f0 t,f1 t) = (T,T)) then w else 60 if ((f0 t,f1 t) = (F,T)) then INCn n (b t) else 61 if ((f0 t,f1 t) = (F,F)) then ADDn n (a t,b t) else 62 SUBn n (a t,b t))`; 63 64val DEL_def = Define `DEL (inp:bus,out:bus) = !t. out (t+1) = inp t`; 65 66val REG_def = Define `REG ((w:wire,r:wire,inp:bus,bus:bus,out:bus),P) = 67 !t. 68 ((out (t+1) = (if w t then inp t else out t)) /\ 69 (P t ==> r t ==> (bus t = out t)))`; 70 71val MEM_def = Define `MEM n ((w:wire,r:wire,addr:bus,bus:bus),(P,mem:mem)) = 72 !t. 73 (mem (t+1) = (if w t then Update (mem t,addr t,bus t) else mem t)) /\ 74 (P t ==> r t ==> (bus t = mem t (addr t)))`; 75 76val CheckCntls_def = Define `CheckCntls (rmem,rpc,racc,rir,rbuf,P) = 77 !t. 78 P t = 79 (if (rmem t) then (~(rpc t \/ racc t \/ rir t \/ rbuf t)) else 80 (if (rpc t) then (~(racc t \/ rir t \/ rbuf t)) else 81 (if (racc t) then (~(rir t \/ rbuf t)) else 82 (if (rir t) then (~(rbuf t)) else T))))`; 83 84val DataPath_def = Define `DataPath n ( 85 (wmem,rmem,wmar,wpc,rpc,wacc,racc,wir,rir,warg,alu0,alu1,rbuf, 86 zeroflag,opcode), 87 (mem,mar,pc,acc,ir,arg,buf)) = 88 ?P bus addr alu pwr gnd. 89 CheckCntls (rmem,rpc,racc,rir,rbuf,P) /\ 90 MEM n ((wmem,rmem,addr,bus),(P,mem)) /\ 91 REG ((wmar,gnd,bus,bus,mar),P) /\ 92 BITS (0,n) (mar,addr) /\ 93 REG ((wpc,rpc,bus,bus,pc),P) /\ 94 REG ((wacc,racc,bus,bus,acc),P) /\ 95 TNZ (acc,zeroflag) /\ 96 REG ((wir,rir,bus,bus,ir),P) /\ 97 BITS (n,3) (ir,opcode) /\ 98 REG ((warg,gnd,bus,bus,arg),P) /\ 99 ALU (n+3) (alu0,alu1,arg,bus,alu) /\ 100 REG ((pwr,rbuf,alu,bus,buf),P) /\ 101 PWR pwr /\ 102 GND gnd`; 103 104val Cntls_def = Define ` 105 Cntls (tok1,tok2) = 106 ((tok2 = "wmem"), 107 (tok1 = "rmem"), 108 (tok2 = "wmar"), 109 (tok2 = "wpc"), 110 (tok1 = "rpc"), 111 (tok2 = "wacc"), 112 (tok1 = "racc"), 113 (tok2 = "wir"), 114 (tok1 = "rir"), 115 (tok2 = "warg"), 116 (tok2 = "sub"), 117 (tok2 = "inc"), 118 (tok1 = "rbuf"))`; 119 120val NextMpc_def = Define `NextMpc (tok,addr:num) = 121 if (tok = "jop") then ((T,F),addr) else 122 if (tok = "jnz") then ((F,T),addr) else 123 if (tok = "jmp") then ((T,T),addr) else 124 ((F,F),addr)`; 125 126val Microcode_def = Define ` 127 (Microcode 0 = (Cntls ("rpc","wmar"), NextMpc ("inc",0)) ) /\ 128 (Microcode 1 = (Cntls ("rmem","wir"), NextMpc ("inc",0)) ) /\ 129 (Microcode 2 = (Cntls ("rir","wmar"), NextMpc ("jop",0)) ) /\ 130 (Microcode 3 = (Cntls ("none","none"), NextMpc ("jnz",10))) /\ (* JZR *) 131 (Microcode 4 = (Cntls ("rir","wpc"), NextMpc ("jmp",0)) ) /\ (* JMP *) 132 (Microcode 5 = (Cntls ("racc","warg"), NextMpc ("jmp",12))) /\ (* ADD *) 133 (Microcode 6 = (Cntls ("racc","warg"), NextMpc ("jmp",13))) /\ (* SUB *) 134 (Microcode 7 = (Cntls ("rmem","wacc"), NextMpc ("jmp",10))) /\ (* LD *) 135 (Microcode 8 = (Cntls ("racc","wmem"), NextMpc ("jmp",10))) /\ (* ST *) 136 (Microcode 9 = (Cntls ("none","none"), NextMpc ("inc",0)) ) /\ (* NOP *) 137 (Microcode 10 = (Cntls ("rpc","inc"), NextMpc ("inc",0)) ) /\ (* NOP *) 138 (Microcode 11 = (Cntls ("rbuf","wpc"), NextMpc ("jmp",0)) ) /\ 139 (Microcode 12 = (Cntls ("rmem","add"), NextMpc ("jmp",14))) /\ 140 (Microcode 13 = (Cntls ("rmem","sub"), NextMpc ("inc",0)) ) /\ 141 (Microcode 14 = (Cntls ("rbuf","wacc"), NextMpc ("jmp",10))) /\ 142 (Microcode _ = (Cntls ("none","none"), NextMpc ("jmp",0)))`; 143 144 145val miw_ty = ty_antiq (hd (tl (snd (dest_type (type_of ``Microcode``))))); 146 147val ROM_def = Define ` 148 ROM contents (addr:bus,data:time->^miw_ty) = 149 !t. data t = contents (addr t)`; 150 151val Decoder_def = Define 152 `Decoder ( 153 miw:time->^miw_ty,test0,test1,addr, 154 wmem,rmem,wmar,wpc,rpc,wacc,racc,wir,rir,warg,alu0,alu1,rbuf) = 155 !t. 156 ((wmem t,rmem t,wmar t,wpc t,rpc t,wacc t, 157 racc t,wir t,rir t,warg t,alu0 t,alu1 t,rbuf t), 158 ((test0 t,test1 t),addr t)) = 159 miw t`; 160 161val MpcUnit_def = Define 162 `MpcUnit (test0,test1,zeroflag,opcode,addr,mpc) = 163 ?w1 w2 const0 const1 const3 b1 b2 b3 b4 b5. 164 AND (test1,zeroflag,w1) /\ 165 OR (test0,w1,w2) /\ 166 MUX (test1,opcode,addr,b1) /\ 167 MUX (w2,mpc,b1,b2) /\ 168 HWC 0 const0 /\ 169 HWC 3 const3 /\ 170 MUX (test1,const3,const0,b3) /\ 171 HWC 1 const1 /\ 172 MUX (w2,const1,b3,b4) /\ 173 ADDER 4 (b2,b4,b5) /\ 174 DEL (b5,mpc)`; 175 176val CntlUnit_def = Define 177 `CntlUnit ( 178 (zeroflag,opcode, 179 wmem,rmem,wmar,wpc,rpc,wacc,racc,wir,rir,warg,alu0,alu1,rbuf), 180 mpc) = 181 ?miw test0 test1 addr. 182 ROM Microcode (mpc,miw) /\ 183 Decoder ( 184 miw,test0,test1,addr, 185 wmem,rmem,wmar,wpc,rpc,wacc,racc,wir,rir,warg,alu0,alu1,rbuf) /\ 186 MpcUnit (test0,test1,zeroflag,opcode,addr,mpc)`; 187 188val Tamarack_def = Define 189 `Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) = 190 ?zeroflag opcode 191 wmem rmem wmar wpc rpc wacc racc wir rir warg alu0 alu1 rbuf. 192 CntlUnit ( 193 (zeroflag,opcode, 194 wmem,rmem,wmar,wpc,rpc,wacc,racc,wir,rir,warg,alu0,alu1,rbuf), 195 (mpc)) /\ 196 DataPath n ( 197 (wmem,rmem,wmar,wpc,rpc,wacc,racc,wir,rir,warg,alu0,alu1,rbuf, 198 zeroflag,opcode), 199 (mem,mar,pc,acc,ir,arg,buf))`; 200 201val Inst_def = Define `Inst n (mem:num->num,pc) = mem (pc MOD (2 EXP n))`; 202 203val Opc_def = Define `Opc n inst = ((inst DIV (2 EXP n)) MOD (2 EXP 3))`; 204 205val Addr_def = Define `Addr n inst = (inst MOD (2 EXP n))`; 206 207val NextState_def = Define ` 208 NextState n (mem,pc,acc) = 209 let inst = Inst n (mem,pc) in 210 let opc = Opc n inst in 211 let addr = Addr n inst in 212 (if (opc = 0) then (mem,(if (acc = 0) then inst else (INCn (n+3) pc)),acc) else 213 if (opc = 1) then (mem,inst,acc) else 214 if (opc = 2) then (mem,(INCn (n+3) pc),(ADDn (n+3) (acc,mem addr))) else 215 if (opc = 3) then (mem,(INCn (n+3) pc),(SUBn (n+3) (acc,mem addr))) else 216 if (opc = 4) then (mem,(INCn (n+3) pc),mem addr) else 217 if (opc = 5) then (Update (mem,addr,acc),(INCn (n+3) pc),acc) else 218 (mem,(INCn (n+3) pc),acc))`; 219 220val Behaviour_def = Define 221 `Behaviour n (mem,pc,acc) = 222 !t. 223 (mem (t+1),pc (t+1),acc (t+1)) = 224 NextState n (mem t,pc t,acc t)`; 225 226val MicroCycles_def = Define 227 `MicroCycles n (mem,pc,acc) = 228 let opc = Opc n (Inst n (mem,pc)) in 229 (if (opc = 0) then (if (acc = 0) then 5 else 6) else 230 if (opc = 1) then 4 else 231 if (opc = 2) then 8 else 232 if (opc = 3) then 8 else 233 if (opc = 4) then 6 else 234 if (opc = 5) then 6 else 235 if (opc = 6) then 6 else 236 5)`; 237 238val REV_TimeOfCycle_def = Define ` 239 (REV_TimeOfCycle 0 n mem pc acc = 0) /\ 240 (REV_TimeOfCycle (SUC t) n mem pc acc = 241 let prev = (REV_TimeOfCycle t n mem pc acc) in 242 (prev + (MicroCycles n (mem prev,pc prev,acc prev))))`; 243 244val TimeOfCycle_def = Define ` 245 TimeOfCycle n (mem,pc,acc) t = REV_TimeOfCycle t n mem pc acc`; 246 247 248 249(* --------------------------- *) 250(* - Proofs 1 - *) 251(* --------------------------- *) 252 253(* Evaluation theorem. 254 One can first evaluate via e.g. 255 256 LIST_CONJ (map (CONV_RULE (RHS_CONV EVAL)) (BODY_CONJUNCTS Microcode_def)) 257 258 and then copy the result, massage it a bit and finally state it 259 explicitly. That way one can increase rebustness. *) 260val Microcode_EVALS = store_thm ("Microcode_EVALS",`` 261 (Microcode 0 = ((F,F,T,F,T,F,F,F,F,F,F,F,F),(F,F),0)) /\ 262 (Microcode 1 = ((F,T,F,F,F,F,F,T,F,F,F,F,F),(F,F),0)) /\ 263 (Microcode 2 = ((F,F,T,F,F,F,F,F,T,F,F,F,F),(T,F),0)) /\ 264 (Microcode 3 = ((F,F,F,F,F,F,F,F,F,F,F,F,F),(F,T),10)) /\ 265 (Microcode 4 = ((F,F,F,T,F,F,F,F,T,F,F,F,F),(T,T),0)) /\ 266 (Microcode 5 = ((F,F,F,F,F,F,T,F,F,T,F,F,F),(T,T),12)) /\ 267 (Microcode 6 = ((F,F,F,F,F,F,T,F,F,T,F,F,F),(T,T),13)) /\ 268 (Microcode 7 = ((F,T,F,F,F,T,F,F,F,F,F,F,F),(T,T),10)) /\ 269 (Microcode 8 = ((T,F,F,F,F,F,T,F,F,F,F,F,F),(T,T),10)) /\ 270 (Microcode 9 = ((F,F,F,F,F,F,F,F,F,F,F,F,F),(F,F),0)) /\ 271 (Microcode 10 = ((F,F,F,F,T,F,F,F,F,F,F,T,F),(F,F),0)) /\ 272 (Microcode 11 = ((F,F,F,T,F,F,F,F,F,F,F,F,T),(T,T),0)) /\ 273 (Microcode 12 = ((F,T,F,F,F,F,F,F,F,F,F,F,F),(T,T),14)) /\ 274 (Microcode 13 = ((F,T,F,F,F,F,F,F,F,F,T,F,F),(F,F),0)) /\ 275 (Microcode 14 = ((F,F,F,F,F,T,F,F,F,F,F,F,T),(T,T),10)) /\ 276 (Microcode 15 = ((F,F,F,F,F,F,F,F,F,F,F,F,F),(T,T),0)) /\ 277 (!v. ((v <> 0) /\ (v <> 1) /\ (v <> 2) /\ (v <> 3) /\ (v <> 4) /\ 278 (v <> 5) /\ (v <> 6) /\ (v <> 7) /\ (v <> 8) /\ (v <> 9) /\ 279 (v <> 10) /\ (v <> 11) /\ (v <> 12) /\ (v <> 13) /\ (v <> 14)) ==> 280 (Microcode v = ((F,F,F,F,F,F,F,F,F,F,F,F,F),(T,T),0)))``, 281EVAL_TAC >> SIMP_TAC std_ss []); 282 283 284(* The following tactics correspond to the sequence of steps which take 285 place when a microinstruction is executed: 286 287 tac1 - produce microcode ROM output; 288 tac2 - generate next mpc state; 289 tac3 - generate next data path state. 290 *) 291 292val tac1 : tactic = 293 PURE_REWRITE_TAC [Tamarack_def, CntlUnit_def, ROM_def] THEN 294 REPEAT STRIP_TAC THEN 295 IMP_RES_THEN (MP_TAC o (SPEC ``t:time``)) (fst (EQ_IMP_RULE (SPEC_ALL Decoder_def))) THEN 296 ASM_REWRITE_TAC [Microcode_EVALS, pairTheory.PAIR_EQ] THEN 297 STRIP_TAC 298 299val tac2 : tactic = 300 IMP_RES_THEN MP_TAC (fst (EQ_IMP_RULE (SPEC_ALL MpcUnit_def))) THEN 301 PURE_ONCE_REWRITE_TAC [AND_def,OR_def,MUX_def,HWC_def,ADDER_def,DEL_def] THEN 302 DISCH_THEN ((REPEAT_TCL CHOOSE_THEN) (fn thm => REWRITE_TAC [thm])) THEN 303 ASM_REWRITE_TAC []; 304 305val tac3 : tactic = 306 IMP_RES_THEN MP_TAC (fst (EQ_IMP_RULE (SPEC_ALL DataPath_def))) THEN 307 PURE_ONCE_REWRITE_TAC [CheckCntls_def,MEM_def,REG_def,BITS_def,TNZ_def,ALU_def,PWR_def,GND_def] THEN 308 DISCH_THEN ((REPEAT_TCL CHOOSE_THEN) MP_TAC) THEN 309 DISCH_THEN (MP_TAC o LIST_CONJ o (map (SPEC ``t:time``)) o CONJUNCTS) THEN 310 ASM_REWRITE_TAC [pairTheory.PAIR_EQ] THEN 311 DISCH_THEN (fn thm => MP_TAC (REWRITE_RULE [CONJUNCT1 thm] (CONJUNCT2 thm))) THEN 312 STRIP_TAC THEN 313 ASM_REWRITE_TAC []; 314 315(* Combined Tactic *) 316val MPC_n_TAC = 317 tac1 >> tac2 >> tac3 >> 318 SIMP_TAC arith_ss [ADDn_def] 319 320val MPC_0_THM = store_thm ("MPC_0_THM", 321``!n mpc mem mar pc acc ir arg buf. 322 Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) 323 ==> 324 !t. 325 (mpc t = 0) ==> 326 ((mpc (t+1),mem (t+1),mar (t+1),pc (t+1),acc (t+1)) = 327 (1,mem t,pc t,pc t,acc t))``, 328 329 MPC_n_TAC 330); 331 332 333val MPC_1_THM = store_thm ("MPC_1_THM", 334``!n mpc mem mar pc acc ir arg buf. 335 Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) 336 ==> 337 !t. 338 (mpc t = 1) ==> 339 ((mpc (t+1),mem (t+1),pc (t+1),acc (t+1),ir (t+1)) = 340 (2,mem t,pc t,acc t,mem t (Bits (0,n) (mar t))))``, 341 342 MPC_n_TAC 343); 344 345 346val MPC_2_THM = store_thm ("MPC_2_THM", 347``!n mpc mem mar pc acc ir arg buf. 348 Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) 349 ==> 350 !t. 351 (mpc t = 2) ==> 352 ((mpc (t+1),mem (t+1),mar (t+1),pc (t+1),acc (t+1),ir (t+1)) = 353 ((Bits (n,3) (ir t)) + 3,mem t,ir t,pc t,acc t,ir t))``, 354 355 MPC_n_TAC >> 356 `Bits (n,3) (ir t) < 8` by SIMP_TAC arith_ss [Bits_def] >> 357 DECIDE_TAC 358); 359 360 361 362val MPC_3_THM = store_thm ("MPC_3_THM", 363``!n mpc mem mar pc acc ir arg buf. 364 Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) 365 ==> 366 !t. 367 (mpc t = 3) ==> 368 ((mpc (t+1),mem (t+1),pc (t+1),acc (t+1),ir (t+1)) = 369 (((if ((acc t) = 0) then 4 else 10),mem t,pc t,acc t,ir t)))``, 370 MPC_n_TAC 371); 372 373 374val MPC_4_THM = store_thm ("MPC_4_THM", 375``!n mpc mem mar pc acc ir arg buf. 376 Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) 377 ==> 378 !t. 379 (mpc t = 4) ==> 380 ((mpc (t+1),mem (t+1),pc (t+1),acc (t+1)) = 381 (0,mem t,ir t,acc t))``, 382 383 MPC_n_TAC 384); 385 386 387val MPC_5_THM = store_thm ("MPC_5_THM", 388``!n mpc mem mar pc acc ir arg buf. 389 Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) 390 ==> 391 !t. 392 (mpc t = 5) ==> 393 ((mpc (t+1),mem (t+1),mar (t+1),pc (t+1),acc (t+1),arg (t+1)) = 394 (12,mem t,mar t,pc t,acc t,acc t))``, 395 396 MPC_n_TAC 397); 398 399 400val MPC_6_THM = store_thm ("MPC_6_THM", 401``!n mpc mem mar pc acc ir arg buf. 402 Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) 403 ==> 404 !t. 405 (mpc t = 6) ==> 406 ((mpc (t+1),mem (t+1),mar (t+1),pc (t+1),acc (t+1),arg (t+1)) = 407 (13,mem t,mar t,pc t,acc t,acc t))``, 408 409 MPC_n_TAC 410); 411 412 413val MPC_7_THM = store_thm ("MPC_7_THM", 414``!n mpc mem mar pc acc ir arg buf. 415 Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) 416 ==> 417 !t. 418 (mpc t = 7) ==> 419 ((mpc (t+1),mem (t+1),pc (t+1),acc (t+1)) = 420 (10,mem t,pc t,mem t (Bits (0,n) (mar t))))``, 421 422 MPC_n_TAC 423); 424 425 426val MPC_8_THM = store_thm ("MPC_8_THM", 427``!n mpc mem mar pc acc ir arg buf. 428 Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) 429 ==> 430 !t. 431 (mpc t = 8) ==> 432 ((mpc (t+1),mem (t+1),pc (t+1),acc (t+1)) = 433 (10,Update (mem t,Bits (0,n) (mar t),acc t),pc t,acc t))``, 434 435 MPC_n_TAC 436); 437 438 439val MPC_9_THM = store_thm ("MPC_9_THM", 440``!n mpc mem mar pc acc ir arg buf. 441 Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) 442 ==> 443 !t. 444 (mpc t = 9) ==> 445 ((mpc (t+1),mem (t+1),pc (t+1),acc (t+1)) = 446 (10,mem t,pc t,acc t))``, 447 448 MPC_n_TAC 449); 450 451 452 453val MPC_10_THM = store_thm ("MPC_10_THM", 454``!n mpc mem mar pc acc ir arg buf. 455 Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) 456 ==> 457 !t. 458 (mpc t = 10) ==> 459 ((mpc (t+1),mem (t+1),pc (t+1),acc (t+1),buf (t+1)) = 460 (11,mem t,pc t,acc t,INCn (n+3) (pc t)))``, 461 462 MPC_n_TAC 463); 464 465 466val MPC_11_THM = store_thm ("MPC_11_THM", 467``!n mpc mem mar pc acc ir arg buf. 468 Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) 469 ==> 470 !t. 471 (mpc t = 11) ==> 472 ((mpc (t+1),mem (t+1),pc (t+1),acc (t+1)) = 473 (0,mem t,buf t,acc t))``, 474 475 MPC_n_TAC 476); 477 478 479val MPC_12_THM = store_thm ("MPC_12_THM", 480``!n mpc mem mar pc acc ir arg buf. 481 Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) 482 ==> 483 !t. 484 (mpc t = 12) ==> 485 ((mpc (t+1),mem (t+1),pc (t+1),acc (t+1),buf (t+1)) = 486 (14,mem t,pc t,acc t, 487 ADDn (n+3) (arg t,mem t (Bits (0,n) (mar t)))))``, 488 489 MPC_n_TAC 490); 491 492 493val MPC_13_THM = store_thm ("MPC_13_THM", 494``!n mpc mem mar pc acc ir arg buf. 495 Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) 496 ==> 497 !t. 498 (mpc t = 13) ==> 499 ((mpc (t+1),mem (t+1),pc (t+1),acc (t+1),buf (t+1)) = 500 (14,mem t,pc t,acc t, 501 SUBn (n+3) (arg t,mem t (Bits (0,n) (mar t)))))``, 502 503 MPC_n_TAC); 504 505 506val MPC_14_THM = store_thm ("MPC_14_THM", 507``!n mpc mem mar pc acc ir arg buf. 508 Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) 509 ==> 510 !t. 511 (mpc t = 14) ==> 512 ((mpc (t+1),mem (t+1),pc (t+1),acc (t+1)) = 513 (10,mem t,pc t,buf t))``, 514 515 MPC_n_TAC); 516 517 518val MPC_15_THM = store_thm ("MPC_15_THM", 519``!n mpc mem mar pc acc ir arg buf. 520 Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) 521 ==> 522 !t. 523 (mpc t = 15) ==> 524 ((mpc (t+1),mem (t+1),pc (t+1),acc (t+1)) = 525 (0,mem t,pc t,acc t))``, 526 527 MPC_n_TAC); 528 529 530(* Nowadays, we have much more computational power at our hands. We 531 can therefore prove a stronger version of theorems MPC_0_THM - MPC_15_THM 532 via brute force. The main idea is using Skolemization in reverse. 533 Apart from that, it is unfolding and a little bit of simple reordering. *) 534 535val Tamarack_EVAL_THM = store_thm ("Tamarack_EVAL_THM", 536 ``!n mpc mem mar pc acc ir arg buf. 537 Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) <=> 538 !t. 539 if mpc t = 0 then 540 (mpc (t + 1) = 1) /\ (mem (t + 1) = mem t) /\ 541 (pc (t + 1) = pc t) /\ (mar (t + 1) = pc t) /\ 542 (acc (t + 1) = acc t) /\ (ir (t + 1) = ir t) /\ 543 (arg (t + 1) = arg t) /\ 544 (buf (t + 1) = ADDn (n + 3) (arg t,mar (t + 1))) 545 else if mpc t = 1 then 546 (mpc (t + 1) = 2) /\ (mem (t + 1) = mem t) /\ 547 (mar (t + 1) = mar t) /\ (pc (t + 1) = pc t) /\ 548 (acc (t + 1) = acc t) /\ 549 (ir (t + 1) = mem t (Bits (0,n) (mar t))) /\ 550 (arg (t + 1) = arg t) /\ 551 (buf (t + 1) = 552 ADDn (n + 3) (arg t,mem t (Bits (0,n) (mar t)))) 553 else if mpc t = 2 then 554 (mpc (t + 1) = (Bits (n,3) (ir t) + 3)) /\ 555 (mem (t + 1) = mem t) /\ (pc (t + 1) = pc t) /\ 556 (acc (t + 1) = acc t) /\ (ir (t + 1) = ir t) /\ 557 (mar (t + 1) = ir t) /\ (arg (t + 1) = arg t) /\ 558 (buf (t + 1) = ADDn (n + 3) (arg t,mar (t + 1))) 559 else if mpc t = 3 then 560 (mpc (t + 1) = if acc t = 0 then 4 else 10) /\ 561 (mem (t + 1) = mem t) /\ (mar (t + 1) = mar t) /\ 562 (pc (t + 1) = pc t) /\ (acc (t + 1) = acc t) /\ 563 (ir (t + 1) = ir t) /\ (arg (t + 1) = arg t) /\ 564 ?bus. buf (t + 1) = ADDn (n + 3) (arg t,bus) 565 else if mpc t = 4 then 566 (mpc (t + 1) = 0) /\ (mem (t + 1) = mem t) /\ 567 (mar (t + 1) = mar t) /\ (acc (t + 1) = acc t) /\ 568 (ir (t + 1) = ir t) /\ (pc (t + 1) = ir t) /\ 569 (arg (t + 1) = arg t) /\ 570 (buf (t + 1) = ADDn (n + 3) (arg t,pc (t + 1))) 571 else if mpc t = 5 then 572 (mpc (t + 1) = 12) /\ (mem (t + 1) = mem t) /\ 573 (mar (t + 1) = mar t) /\ (pc (t + 1) = pc t) /\ 574 (acc (t + 1) = acc t) /\ (ir (t + 1) = ir t) /\ 575 (arg (t + 1) = acc t) /\ 576 (buf (t + 1) = ADDn (n + 3) (arg t,acc t)) 577 else if mpc t = 6 then 578 (mpc (t + 1) = 13) /\ (mem (t + 1) = mem t) /\ 579 (mar (t + 1) = mar t) /\ (pc (t + 1) = pc t) /\ 580 (acc (t + 1) = acc t) /\ (ir (t + 1) = ir t) /\ 581 (arg (t + 1) = acc t) /\ 582 (buf (t + 1) = ADDn (n + 3) (arg t,acc t)) 583 else if mpc t = 7 then 584 (mpc (t + 1) = 10) /\ (mem (t + 1) = mem t) /\ 585 (mar (t + 1) = mar t) /\ (pc (t + 1) = pc t) /\ 586 (acc (t + 1) = mem t (Bits (0,n) (mar t))) /\ 587 (ir (t + 1) = ir t) /\ (arg (t + 1) = arg t) /\ 588 (buf (t + 1) = 589 ADDn (n + 3) (arg t,mem t (Bits (0,n) (mar t)))) 590 else if mpc t = 8 then 591 (mpc (t + 1) = 10) /\ 592 (mem (t + 1) = (Bits (0,n) (mar t) =+ acc t) (mem t)) /\ 593 (mar (t + 1) = mar t) /\ (pc (t + 1) = pc t) /\ 594 (acc (t + 1) = acc t) /\ (ir (t + 1) = ir t) /\ 595 (arg (t + 1) = arg t) /\ 596 (buf (t + 1) = ADDn (n + 3) (arg t,acc t)) 597 else if mpc t = 9 then 598 (mpc (t + 1) = 10) /\ (mem (t + 1) = mem t) /\ 599 (mar (t + 1) = mar t) /\ (pc (t + 1) = pc t) /\ 600 (acc (t + 1) = acc t) /\ (ir (t + 1) = ir t) /\ 601 (arg (t + 1) = arg t) /\ 602 ?bus. buf (t + 1) = ADDn (n + 3) (arg t, bus) 603 else if mpc t = 10 then 604 (mpc (t + 1) = 11) /\ (mem (t + 1) = mem t) /\ 605 (mar (t + 1) = mar t) /\ (pc (t + 1) = pc t) /\ 606 (acc (t + 1) = acc t) /\ (ir (t + 1) = ir t) /\ 607 (arg (t + 1) = arg t) /\ (buf (t + 1) = INCn (n + 3) (pc t)) 608 else if mpc t = 11 then 609 (mpc (t + 1) = 0) /\ (mem (t + 1) = mem t) /\ 610 (mar (t + 1) = mar t) /\ (acc (t + 1) = acc t) /\ 611 (ir (t + 1) = ir t) /\ (arg (t + 1) = arg t) /\ 612 (buf (t + 1) = ADDn (n + 3) (arg t,pc (t + 1))) /\ 613 (pc (t + 1) = buf t) 614 else if mpc t = 12 then 615 (mpc (t + 1) = 14) /\ (mem (t + 1) = mem t) /\ 616 (mar (t + 1) = mar t) /\ (pc (t + 1) = pc t) /\ 617 (acc (t + 1) = acc t) /\ (ir (t + 1) = ir t) /\ 618 (arg (t + 1) = arg t) /\ 619 (buf (t + 1) = 620 ADDn (n + 3) (arg t,mem t (Bits (0,n) (mar t)))) 621 else if mpc t = 13 then 622 (mpc (t + 1) = 14) /\ (mem (t + 1) = mem t) /\ 623 (mar (t + 1) = mar t) /\ (pc (t + 1) = pc t) /\ 624 (acc (t + 1) = acc t) /\ (ir (t + 1) = ir t) /\ 625 (arg (t + 1) = arg t) /\ 626 (buf (t + 1) = 627 SUBn (n + 3) (arg t,mem t (Bits (0,n) (mar t)))) 628 else if mpc t = 14 then 629 (mpc (t + 1) = 10) /\ (mem (t + 1) = mem t) /\ 630 (mar (t + 1) = mar t) /\ (pc (t + 1) = pc t) /\ 631 (ir (t + 1) = ir t) /\ (arg (t + 1) = arg t) /\ 632 (buf (t + 1) = ADDn (n + 3) (arg t,acc (t + 1))) /\ 633 (acc (t + 1) = buf t) 634 else 635 (mpc (t + 1) = 0) /\ (mem (t + 1) = mem t) /\ 636 (mar (t + 1) = mar t) /\ (pc (t + 1) = pc t) /\ 637 (acc (t + 1) = acc t) /\ (ir (t + 1) = ir t) /\ 638 (arg (t + 1) = arg t) /\ 639 ?bus. buf (t + 1) = ADDn (n + 3) (arg t,bus)``, 640 641REPEAT STRIP_TAC >> 642SIMP_TAC std_ss [Tamarack_def, CntlUnit_def, 643 ROM_def, Decoder_def, MpcUnit_def, DataPath_def, 644 AND_def, OR_def, MUX_def, HWC_def, MEM_def, ALU_def, REG_def, 645 BITS_def, DEL_def, CheckCntls_def, 646 ADDER_def, PWR_def, GND_def, TNZ_def, 647 GSYM FORALL_AND_THM, PULL_EXISTS] >> 648SIMP_TAC std_ss [GSYM SKOLEM_THM] >> 649ConseqConv.CONSEQ_CONV_TAC (K ConseqConv.FORALL_EQ___CONSEQ_CONV) >> 650SIMP_TAC pure_ss [prove (``(X:'a = if c then x1 else x2) <=> (if c then (X = x1) else (X = x2))``, 651 Cases_on `c` >> REWRITE_TAC[])] >> 652SIMP_TAC (std_ss++boolSimps.EQUIV_EXTRACT_ss) [Microcode_EVALS, ADDn_def, 653 Update_def, GSYM PULL_EXISTS] >> 654`!n m. (Bits (n,3) m + 3) < 16` by ( 655 REPEAT GEN_TAC >> 656 `Bits (n, 3) m < 8` by SIMP_TAC arith_ss [Bits_def] >> 657 DECIDE_TAC 658) >> 659ASM_SIMP_TAC (arith_ss++boolSimps.LIFT_COND_ss) []); 660 661 662 663(* --------------------------- *) 664(* - Proofs 2 - *) 665(* --------------------------- *) 666 667fun EXEC_MPC_TAC tm = 668 Q.PAT_ASSUM `Tamarack _ _` (fn thm => let 669 val thm0 = CONV_RULE (REWR_CONV Tamarack_EVAL_THM) thm 670 val thm1 = SPEC tm thm0 671 in MP_TAC thm1 end) >> 672 SUBST1_TAC (SIMP_CONV arith_ss [] ``^tm + 1``) >> 673 ASM_SIMP_TAC std_ss [ADDn_def, Bits_def] >> 674 STRIP_TAC 675 676fun EXEC_MPC_TACn n = let 677 fun mk_tm n = let val m = numLib.term_of_int n in ``(t:time) + ^m`` end 678 val ns = Lib.for 0 (n-1) mk_tm 679in 680 EVERY (map EXEC_MPC_TAC ns) 681end 682 683fun EXEC_INST_FETCH_TAC n = 684 SIMP_TAC arith_ss [Opc_def,Inst_def] >> 685 REPEAT (FIRST [GEN_TAC,DISCH_THEN STRIP_ASSUME_TAC]) >> 686 EXEC_MPC_TACn n 687 688 689val JZR_T_INST_THM = store_thm ("JZR_T_INST_THM", 690``!n mpc mem mar pc acc ir arg buf. 691 Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) 692 ==> 693 !t. 694 (mpc t = 0) /\ 695 (Opc n (Inst n (mem t,pc t)) = 0) /\ 696 (acc t = 0) 697 ==> 698 (mpc (t+5) = 0) /\ 699 ((mem (t+5),pc (t+5),acc (t+5)) = 700 NextState n (mem t,pc t,acc t))``, 701 702EXEC_INST_FETCH_TAC 5 >> 703ASM_SIMP_TAC std_ss [NextState_def, LET_DEF, Inst_def, Opc_def]); 704 705 706val JZR_F_INST_THM = store_thm ("JZR_F_INST_THM", 707``!n mpc mem mar pc acc ir arg buf. 708 Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) 709 ==> 710 !t. 711 (mpc t = 0) /\ 712 (Opc n (Inst n (mem t,pc t)) = 0) /\ 713 ~(acc t = 0) 714 ==> 715 (mpc (t+6) = 0) /\ 716 ((mem (t+6),pc (t+6),acc (t+6)) = 717 NextState n (mem t,pc t,acc t))``, 718 719EXEC_INST_FETCH_TAC 6 >> 720ASM_SIMP_TAC std_ss [NextState_def, LET_DEF, Inst_def, Opc_def]); 721 722 723val JMP_INST_THM = store_thm ("JMP_INST_THM", 724``!n mpc mem mar pc acc ir arg buf. 725 Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) 726 ==> 727 !t. 728 (mpc t = 0) /\ 729 (Opc n (Inst n (mem t,pc t)) = 1) 730 ==> 731 (mpc (t+4) = 0) /\ 732 ((mem (t+4),pc (t+4),acc (t+4)) = 733 NextState n (mem t,pc t,acc t))``, 734 735EXEC_INST_FETCH_TAC 4 >> 736ASM_SIMP_TAC std_ss [NextState_def, LET_DEF, Inst_def, Opc_def]); 737 738 739val ADD_INST_THM = store_thm ("ADD_INST_THM", 740``!n mpc mem mar pc acc ir arg buf. 741 Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) 742 ==> 743 !t. 744 (mpc t = 0) /\ 745 (Opc n (Inst n (mem t,pc t)) = 2) 746 ==> 747 (mpc (t+8) = 0) /\ 748 ((mem (t+8),pc (t+8),acc (t+8)) = 749 NextState n (mem t,pc t,acc t))``, 750 751EXEC_INST_FETCH_TAC 8 >> 752ASM_SIMP_TAC std_ss [NextState_def, LET_DEF, Inst_def, Opc_def, 753 ADDn_def, Addr_def]); 754 755 756val SUB_INST_THM = store_thm ("ADD_INST_THM", 757``!n mpc mem mar pc acc ir arg buf. 758 Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) 759 ==> 760 !t. 761 (mpc t = 0) /\ 762 (Opc n (Inst n (mem t,pc t)) = 3) 763 ==> 764 (mpc (t+8) = 0) /\ 765 ((mem (t+8),pc (t+8),acc (t+8)) = 766 NextState n (mem t,pc t,acc t))``, 767 768EXEC_INST_FETCH_TAC 8 >> 769ASM_SIMP_TAC std_ss [NextState_def, LET_DEF, Inst_def, Opc_def, 770 ADDn_def, Addr_def]); 771 772 773val LD_INST_THM = store_thm ("LD_INST_THM", 774``!n mpc mem mar pc acc ir arg buf. 775 Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) 776 ==> 777 !t. 778 (mpc t = 0) /\ 779 (Opc n (Inst n (mem t,pc t)) = 4) 780 ==> 781 (mpc (t+6) = 0) /\ 782 ((mem (t+6),pc (t+6),acc (t+6)) = 783 NextState n (mem t,pc t,acc t))``, 784 785EXEC_INST_FETCH_TAC 6 >> 786ASM_SIMP_TAC std_ss [NextState_def, LET_DEF, Inst_def, Opc_def, 787 ADDn_def, Update_def, Addr_def]); 788 789 790val ST_INST_THM = store_thm ("ST_INST_THM", 791``!n mpc mem mar pc acc ir arg buf. 792 Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) 793 ==> 794 !t. 795 (mpc t = 0) /\ 796 (Opc n (Inst n (mem t,pc t)) = 5) 797 ==> 798 (mpc (t+6) = 0) /\ 799 ((mem (t+6),pc (t+6),acc (t+6)) = 800 NextState n (mem t,pc t,acc t))``, 801 802EXEC_INST_FETCH_TAC 6 >> 803ASM_SIMP_TAC std_ss [NextState_def, LET_DEF, Inst_def, Opc_def, 804 ADDn_def, Update_def, Addr_def]); 805 806 807val NOP1_INST_THM = store_thm ("NOP1_INST_THM", 808``!n mpc mem mar pc acc ir arg buf. 809 Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) 810 ==> 811 !t. 812 (mpc t = 0) /\ 813 (Opc n (Inst n (mem t,pc t)) = 6) 814 ==> 815 (mpc (t+6) = 0) /\ 816 ((mem (t+6),pc (t+6),acc (t+6)) = 817 NextState n (mem t,pc t,acc t))``, 818 819EXEC_INST_FETCH_TAC 6 >> 820ASM_SIMP_TAC std_ss [NextState_def, LET_DEF, Inst_def, Opc_def, 821 ADDn_def, Update_def, Addr_def]); 822 823 824val NOP2_INST_THM = store_thm ("NOP2_INST_THM", 825``!n mpc mem mar pc acc ir arg buf. 826 Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) 827 ==> 828 !t. 829 (mpc t = 0) /\ 830 (Opc n (Inst n (mem t,pc t)) = 7) 831 ==> 832 (mpc (t+5) = 0) /\ 833 ((mem (t+5),pc (t+5),acc (t+5)) = 834 NextState n (mem t,pc t,acc t))``, 835 836EXEC_INST_FETCH_TAC 5 >> 837ASM_SIMP_TAC std_ss [NextState_def, LET_DEF, Inst_def, Opc_def, 838 ADDn_def, Update_def, Addr_def]); 839 840 841(* --------------------------- *) 842(* - Proofs 3 - *) 843(* --------------------------- *) 844 845val MicroCycles_def = Define `MicroCycles n (mem,pc,acc) = 846 let opc = Opc n (Inst n (mem,pc)) in 847 (if (opc = 0) then (if (acc = 0) then 5 else 6) else 848 if (opc = 1) then 4 else 849 if (opc = 2) then 8 else 850 if (opc = 3) then 8 else 851 if (opc = 4) then 6 else 852 if (opc = 5) then 6 else 853 if (opc = 6) then 6 else 854 5)`; 855 856val TimeOfCycle_def = Define ` 857 (TimeOfCycle n (mem,pc,acc) 0 = 0) /\ 858 (TimeOfCycle n (mem,pc,acc) (SUC t) = 859 let prev = TimeOfCycle n (mem, pc, acc) t in 860 (prev + (MicroCycles n (mem prev,pc prev,acc prev))))`; 861 862 863val EVERY_INST_THM = store_thm ("EVERY_INST_THM", 864``!n mpc mem mar pc acc ir arg buf. 865 Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) 866 ==> 867 !t. 868 (mpc t = 0) 869 ==> 870 let m = MicroCycles n (mem t,pc t,acc t) in 871 ((mpc (t+m) = 0) /\ 872 ((mem (t+m),pc (t+m),acc (t+m)) = 873 NextState n (mem t,pc t,acc t)))``, 874 875REPEAT STRIP_TAC THEN 876Q.ABBREV_TAC `opc = Opc n (Inst n (mem t,pc t))` >> 877ASM_SIMP_TAC std_ss [MicroCycles_def, LET_DEF] >> 878 879`(opc = 0) \/ (opc = 1) \/ (opc = 2) \/ (opc = 3) \/ 880 (opc = 4) \/ (opc = 5) \/ (opc = 6) \/ (opc = 7)` by ( 881 `opc < 8` suffices_by DECIDE_TAC >> 882 Q.UNABBREV_TAC `opc` >> 883 SIMP_TAC arith_ss [Opc_def] 884) >> ASM_SIMP_TAC std_ss [] >| [ 885 PROVE_TAC [JZR_T_INST_THM, JZR_F_INST_THM], 886 PROVE_TAC [JMP_INST_THM], 887 PROVE_TAC [ADD_INST_THM], 888 PROVE_TAC [SUB_INST_THM], 889 PROVE_TAC [LD_INST_THM], 890 PROVE_TAC [ST_INST_THM], 891 PROVE_TAC [NOP1_INST_THM], 892 PROVE_TAC [NOP2_INST_THM] 893]); 894 895val ALWAYS_MPC_0_THM = store_thm ("ALWAYS_MPC_0_THM", 896``!n mpc mem mar pc acc ir arg buf. 897 Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) /\ 898 (mpc 0 = 0) 899 ==> 900 !t. mpc (TimeOfCycle n (mem,pc,acc) t) = 0``, 901 902REPEAT STRIP_TAC >> 903Induct_on `t` >> ( 904 METIS_TAC [EVERY_INST_THM, TimeOfCycle_def] 905)) 906 907 908val CORRECTNESS_THM = store_thm ("CORRECTNESS_THM", 909``!n mpc mem mar pc acc ir arg buf. 910 Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) /\ 911 (mpc 0 = 0) 912 ==> 913 let f = TimeOfCycle n (mem,pc,acc) in 914 Behaviour n (mem o f,pc o f,acc o f)``, 915 916SIMP_TAC std_ss [Behaviour_def, LET_DEF, TimeOfCycle_def, GSYM ADD1] >> 917METIS_TAC[ALWAYS_MPC_0_THM, EVERY_INST_THM]); 918 919 920val _ = export_theory (); 921