1(* ========================================================================= *) 2(* FILE : coreScript.sml *) 3(* DESCRIPTION : Model of the ARM6 micro-architecture *) 4(* *) 5(* AUTHORS : (c) Anthony Fox, University of Cambridge *) 6(* DATE : 2001 - 2005 *) 7(* ========================================================================= *) 8 9(* interactive use: 10 app load ["armTheory"]; 11*) 12 13open HolKernel boolLib Parse bossLib; 14open Q io_onestepTheory armTheory; 15 16val _ = new_theory "core"; 17 18(* ------------------------------------------------------------------------- *) 19(* The State Space --------------------------------------------------------- *) 20(* ------------------------------------------------------------------------- *) 21 22val _ = Hol_datatype `iseq = t3 | t4 | t5 | t6 | tn | tm`; 23 24val _ = Hol_datatype 25 `dp = DP of reg=>psr=>word32=>word32=>word32=>word32=>word32`; 26 27val _ = Hol_datatype 28 `ctrl = CTRL of word32=>bool=>word32=>bool=>word32=>bool=>bool=>bool=> 29 bool=>bool=>bool=>iclass=>iseq=>bool=>bool=>bool=>bool=> 30 bool=>bool=>bool=>bool=>bool=>bool=>bool=>word3=>bool=> 31 bool=>bool=>word32=>word32=>word2=>word16=>word4=>word4=> 32 word2=>word32=>bool=>word5`; 33 34val _ = Hol_datatype `state_arm6 = ARM6 of dp=>ctrl`; 35 36val arm6state = ``ARM6 (DP reg psr areg din alua alub dout) 37 (CTRL pipea pipeaval pipeb pipebval ireg iregval ointstart onewinst endinst 38 obaselatch opipebll nxtic nxtis nopc1 oorst resetlatch onfq ooonfq 39 oniq oooniq pipeaabt pipebabt iregabt2 dataabt2 aregn2 mrq2 nbw nrw 40 sctrlreg psrfb oareg mask orp oorp mul mul2 borrow2 mshift)``; 41 42(* ......................................................................... *) 43 44val Rg = inst [alpha |-> ``:32``, beta |-> ``:4``] ``$><``; 45 46val CLEARBIT_def = Define `CLEARBIT x = word_modify (\i b. ~(i = x) /\ b)`; 47val LEASTBIT_def = Define `LEASTBIT n = LEAST b. n %% b`; 48 49val REG_READ6_def = Define` 50 REG_READ6 reg mode n = 51 if n = 15w then 52 FETCH_PC reg 53 else 54 REG_READ reg mode n`; 55 56(* ------------------------------------------------------------------------- *) 57(* Data Path Control: Instruction Fetch Phase 1 ---------------------------- *) 58(* ------------------------------------------------------------------------- *) 59 60val NMREQ_def = Define` 61 NMREQ ic is pencz mulx cpb = 62 (is = t3) /\ ((ic = reg_shift) \/ (ic = mla_mul) \/ (ic = mcr) \/ 63 ((ic = cdp_und) \/ (ic = ldc) \/ (ic = stc)) /\ cpb) \/ 64 (is = t4) /\ (ic = ldr) \/ 65 (is = t5) /\ (ic = swp) \/ 66 (is = tn) /\ (ic = mla_mul) /\ ~mulx \/ 67 ~(is = t3) /\ ~(is = tm) /\ (ic = ldm) /\ pencz \/ 68 ~(is = t5) /\ (ic = mrc)`; 69 70(* True if pc is to be updated by incrementor *) 71 72val PCWA_def = Define` 73 PCWA ic is ireg cpb = 74 let bit24 = ireg %% 24 75 and bit23 = ireg %% 23 76 and bit21 = ireg %% 21 77 and bits1512 = ^Rg 15 12 ireg in 78 (is = t3) /\ 79 ~((ic = data_proc) /\ (~bit24 \/ bit23) /\ (bits1512 = 15w) \/ 80 (ic = mrs_msr) /\ ~bit21 /\ (bits1512 = 15w) \/ 81 (((ic = cdp_und) \/ (ic = mcr) \/ (ic = mrc) \/ 82 (ic = ldc) \/ (ic = stc)) /\ cpb)) \/ 83 (ic = br) \/ (ic = swi_ex)`; 84 85(* ------------------------------------------------------------------------- *) 86(* Data Path Control: Instruction Fetch Phase 2 ---------------------------- *) 87(* ------------------------------------------------------------------------- *) 88 89(* Memory access on next cycle: Byte (F) or word (T) *) 90 91val NBW_def = Define` 92 NBW ic is (ireg:word32) = 93 ~(ireg %% 22 /\ 94 ((is = t3) /\ ((ic = ldr) \/ (ic = str) \/ (ic = swp)) \/ 95 (is = t4) /\ (ic = swp)))`; 96 97val NOPC_def = Define` 98 NOPC ic is pencz cpb = 99 ((ic = ldr) \/ (ic = str) \/ (ic = swp)) /\ (is = t3) \/ 100 ((ic = ldc) \/ (ic = stc)) /\ ~cpb \/ 101 (ic = swp) /\ (is = t4) \/ 102 (ic = ldm) /\ ~(is = tm) /\ ~pencz \/ 103 (ic = stm) /\ ~pencz`; 104 105(* Memory access on next cycle: Write (T) or other (F) *) 106 107val NRW_def = Define` 108 NRW ic is pencz cpb = 109 (is = t3) /\ ((ic = str) \/ (ic = mcr) /\ ~cpb) \/ 110 (is = t4) /\ (ic = swp) \/ 111 (ic = stc) /\ ~cpb \/ 112 (ic = stm) /\ ~pencz`; 113 114val AREG_def = Define` 115 AREG ic is ireg (aregn:word3) (inc:word32) reg15 aluout (list:word16) 116 pencz (oorp:word4) cpb dataabt = 117 let bits1916 = ^Rg 19 16 ireg 118 and bits1512 = ^Rg 15 12 ireg 119 and bit21 = ireg %% 21 120 and bit23 = ireg %% 23 121 and bit24 = ireg %% 24 122 in 123 if (is = t4) /\ (ic = reg_shift) then 124 if (~bit24 \/ bit23) /\ (bits1512 = 15w) then 125 aluout 126 else 127 reg15 128 else if (is = t4) /\ ((ic = ldr) \/ (ic = str)) then 129 if (~bit24 \/ bit21) /\ (bits1916 = 15w) then 130 aluout 131 else 132 reg15 133 else if (is = t5) /\ (ic = ldr) \/ 134 (is = t6) /\ (ic = swp) then 135 if (bits1512 = 15w) /\ ~dataabt then 136 aluout 137 else 138 reg15 139 else if (is = tm) /\ (ic = ldm) then 140 if (oorp = 15w) /\ ~(list = 0w) then 141 aluout 142 else 143 reg15 144 else if (ic = ldc) \/ (ic = stc) then 145 if cpb then 146 reg15 147 else if is = t3 then 148 aluout 149 else 150 inc 151 else if (is = t3) /\ 152 ((ic = data_proc) /\ (~bit24 \/ bit23) /\ (bits1512 = 15w) \/ 153 (ic = mrs_msr) /\ ~bit21 /\ (bits1512 = 15w) \/ 154 (ic = ldr) \/ (ic = str) \/ (ic = ldm) \/ (ic = stm) \/ 155 (ic = br)) \/ (ic = swp) then 156 aluout 157 else if (is = t3) /\ (ic = swi_ex) then 158 4w * w2w aregn 159 else if ((ic = ldm) \/ (ic = stm)) /\ pencz \/ 160 (is = tn) /\ (ic = mla_mul) \/ 161 (is = t3) /\ (ic = cdp_und) /\ cpb \/ 162 (~(is = t3) \/ cpb) /\ ((ic = mcr) \/ (ic = mrc)) then 163 reg15 164 else 165 inc`; 166 167(* ------------------------------------------------------------------------- *) 168(* Data Path Control: Instruction Decode Phase 2 --------------------------- *) 169(* ------------------------------------------------------------------------- *) 170 171val DIN_def = Define` 172 DIN ic is (ireg:word32) data = 173 if ((ic = ldr) \/ (ic = ldm) \/ (ic = swp) \/ (ic = mrc)) /\ (is = t4) \/ 174 (ic = ldm) /\ (is = tn) then 175 data 176 else 177 ireg`; 178 179val DINWRITE_def = Define` 180 DINWRITE ic is = ~((ic = swp) /\ (is = t5))`; 181 182val MASK_def = Define` 183 MASK nxtic nxtis (mask:word16) (rp:word4) = 184 if (nxtic = ldm) \/ (nxtic = stm) then 185 if nxtis = t3 then 186 UINT_MAXw 187 else 188 CLEARBIT (w2n rp) mask 189 else ARB`; 190 191(* ------------------------------------------------------------------------- *) 192(* Data Path Control: Instruction Execute Phase 1 -------------------------- *) 193(* ------------------------------------------------------------------------- *) 194 195val NBS_def = Define` 196 NBS ic is (ireg:word32) m = 197 let bit22 = ireg %% 22 198 and bit15 = ireg %% 15 in 199 if bit22 /\ (((is = tn) \/ (is = tm)) /\ (ic = ldm) /\ ~bit15 \/ 200 ((is = t4) \/ (is = tn)) /\ (ic = stm)) then 201 usr 202 else 203 DECODE_MODE m`; 204 205val RP_def = Define` 206 RP ic (list:word16) mask = 207 if (ic = ldm) \/ (ic = stm) then 208 n2w (LEASTBIT (list && mask)):word4 209 else ARB`; 210 211val PENCZ_def = Define` 212 PENCZ ic (list:word16) mask = 213 if (ic = ldm) \/ (ic = stm) then 214 (list && mask) = 0w 215 else ARB`; 216 217val OFFSET_def = Define` 218 OFFSET ic is (ireg:word32) (list:word16) = 219 let bit24 = ireg %% 24 220 and bit23 = ireg %% 23 221 and w = 4w * n2w (SUM 16 (BITV (w2n list))) - 4w:word32 in 222 if (is = t3) /\ ((ic = ldm) \/ (ic = stm)) then 223 if bit23 then 224 3w 225 else if bit24 then 226 w + 3w 227 else 228 w 229 else if (is = t4) /\ ((ic = ldm) \/ (ic = stm)) then 230 w + 3w 231 else if (is = t5) /\ ((ic = br) \/ (ic = swi_ex)) then 232 3w 233 else 234 ARB`; 235 236val FIELD_def = Define` 237 FIELD ic is (ireg:word32) (oareg:word2) (din:word32) = 238 if is = t3 then 239 if ic = br then 240 sw2sw (((23 >< 0) din):word24):word32 241 else if (ic = ldr) \/ (ic = str) then 242 (11 -- 0) din 243 else if (ic = mrs_msr) \/ (ic = data_proc) \/ 244 (ic = ldc) \/ (ic = stc) then 245 (7 -- 0) din 246 else 247 ARB 248 else if (is = t5) /\ (ic = ldr) \/ (is = t6) /\ (ic = swp) then 249 if ~(ireg %% 22) then 250 din 251 else let a = 8 * w2n oareg in 252 ((a + 7) '' a) din 253 else if (ic = ldm) /\ ((is = tn) \/ (is = tm)) \/ 254 (ic = mrc) /\ (is = t5) then 255 din 256 else 257 ARB`; 258 259val RBA_def = Define` 260 RBA ic is ireg orp = 261 if (is = t3) /\ ((ic = data_proc) \/ (ic = mrs_msr) \/ 262 (ic = ldr) \/ (ic = str)) \/ 263 (is = t4) /\ (ic = reg_shift) \/ 264 (is = t5) /\ (ic = swp) \/ 265 (is = tn) /\ (ic = mla_mul) then 266 ^Rg 3 0 ireg 267 else if (is = t3) /\ ((ic = swp) \/ (ic = ldm) \/ (ic = stm)) then 268 ^Rg 19 16 ireg 269 else if (is = t3) /\ (ic = mla_mul) \/ (is = t4) /\ (ic = str) \/ 270 (is = t4) /\ (ic = mcr) then 271 ^Rg 15 12 ireg 272 else if (is = t5) /\ ((ic = br) \/ (ic = swi_ex)) then 273 14w 274 else if ((is = t4) \/ (is = tn)) /\ (ic = stm) then 275 orp 276 else 277 ARB`; 278 279val RAA_def = Define` 280 RAA ic is ireg = 281 if is = t3 then 282 if (ic = data_proc) \/ (ic = ldr) \/ (ic = str) \/ 283 (ic = ldc) \/ (ic = stc) then 284 ^Rg 19 16 ireg 285 else if (ic = reg_shift) \/ (ic = mla_mul) then 286 ^Rg 11 8 ireg 287 else if (ic = br) \/ (ic = swi_ex) then 288 15w 289 else ARB 290 else if (is = t4) /\ (ic = reg_shift) \/ 291 ((is = tn) \/ (is = tm)) /\ (ic = ldm) \/ 292 (is = tn) /\ (ic = mla_mul) then 293 ^Rg 19 16 ireg 294 else ARB`; 295 296val PSRA_def = Define` 297 PSRA ic is (ireg:word32) = 298 let bit22 = ireg %% 22 299 and bit20 = ireg %% 20 in 300 (is = t3) /\ ((ic = swi_ex) \/ ~bit22 /\ ((ic = mrs_msr) \/ 301 (ic = data_proc) /\ ~bit20)) \/ 302 (is = t4) /\ ~bit22 /\ (ic = reg_shift) /\ ~bit20 \/ 303 (is = tm) /\ ~bit22 /\ (ic = ldm)`; 304 305val BUSB_def = Define` 306 BUSB ic is (ireg:word32) (din':word32) rb = 307 let bit25 = ireg %% 25 in 308 if (is = t3) /\ 309 ((ic = br) \/ 310 (bit25 /\ ((ic = data_proc) \/ (ic = mrs_msr))) \/ 311 (~bit25 /\ ((ic = ldr) \/ (ic = str))) \/ 312 (ic = ldc) \/ (ic = stc)) \/ 313 (is = t5) /\ ((ic = ldr) \/ (ic = mrc)) \/ 314 (is = t6) /\ (ic = swp) \/ 315 ((is = tn) \/ (is = tm)) /\ (ic = ldm) then 316 din' 317 else 318 rb`; 319 320val BUSA_def = Define` 321 BUSA ic is (psrrd:word32) ra offset = 322 if ((is = t3) \/ (is = t4)) /\ ((ic = ldm) \/ (ic = stm)) \/ 323 (is = t5) /\ ((ic = br) \/ (ic = swi_ex)) then 324 offset 325 else if is = t3 then 326 if ic = mrs_msr then 327 psrrd 328 else if (ic = data_proc) \/ (ic = ldr) \/ (ic = str) \/ 329 (ic = br) \/ (ic = swi_ex) \/ (ic = ldc) \/ (ic = stc) then 330 ra 331 else 332 ARB 333 else if (is = t4) /\ (ic = reg_shift) \/ 334 (is = tn) /\ (ic = mla_mul) \/ 335 ((is = tn) \/ (is = tm)) /\ (ic = ldm) then 336 ra 337 else 338 ARB`; 339 340(* Incorporates SCTLC *) 341 342val SHIFTER_def = Define` 343 SHIFTER ic is (ireg:word32) (oareg:word2) (mshift:word5) 344 (sctrlreg:word32) busb c = 345 let bit25 = ireg %% 25 346 and bits118 = (11 >< 8) ireg 347 and bits117 = (11 >< 7) ireg 348 and bits65 = (6 >< 5) ireg in 349 if is = t3 then 350 if bit25 /\ ((ic = data_proc) \/ (ic = mrs_msr)) then 351 ROR busb (2w * bits118) c 352 else if (ic = ldm) \/ (ic = stm) \/ (ic = swp) \/ (ic = mla_mul) \/ 353 ~bit25 /\ ((ic = ldr) \/ (ic = str) \/ (ic = mrs_msr)) then 354 LSL busb 0w c 355 else if (~bit25 /\ (ic = data_proc)) \/ 356 (bit25 /\ ((ic = ldr) \/ (ic = str))) then 357 SHIFT_IMMEDIATE2 bits117 bits65 busb c 358 else if (ic = br) \/ (ic = ldc) \/ (ic = stc) then 359 LSL busb 2w c 360 else 361 ARB 362 else if (is = t4) /\ (ic = reg_shift) then 363 SHIFT_REGISTER2 ((7 >< 0) sctrlreg) bits65 busb c 364 else if (is = t5) /\ (ic = ldr) \/ (is = t6) /\ (ic = swp) then 365 ROR busb (8w * w2w oareg) c 366 else if (is = t5) /\ ((ic = br) \/ (ic = swi_ex) \/ (ic = mrc)) \/ 367 ~(is = t4) /\ (ic = ldm) then 368 LSL busb 0w c 369 else if ic = mla_mul then (* is = tn *) 370 LSL busb (w2w mshift) c 371 else 372 ARB`; 373 374val BORROW_def = Define` 375 BORROW ic is (mul:word2) = 376 if ic = mla_mul then 377 ~(is = t3) /\ mul %% 1 378 else 379 ARB`; 380 381val COUNT1_def = Define` 382 COUNT1 ic is (mshift:word5) = 383 if ic = mla_mul then 384 if is = t3 then (0w:word4) else (4 >< 1) mshift + 1w 385 else 386 ARB`; 387 388val MUL1_def = Define` 389 MUL1 ic is ra (mul2:word32) = 390 if ic = mla_mul then 391 if is = t3 then ra else (29 -- 0) mul2 392 else 393 ARB`; 394 395val MULZ_def = Define` 396 MULZ ic is mul2 = 397 if (is = tn) /\ (ic = mla_mul) then 398 (29 -- 0) mul2 = 0w 399 else 400 ARB`; 401 402val MULX_def = Define` 403 MULX ic is mulz borrow (mshift:word5) = 404 if (is = tn) /\ (ic = mla_mul) then 405 mulz /\ ~borrow \/ ((4 -- 1) mshift = 15w) 406 else 407 ARB`; 408 409val PSRFBWRITE_def = Define` 410 PSRFBWRITE ic is = ~((ic = mla_mul) \/ (is = t4) /\ (ic = swi_ex))`; 411 412val SCTRLREGWRITE_def = Define` 413 SCTRLREGWRITE ic is = (is = t3) /\ (ic = reg_shift)`; 414 415val ALUAWRITE_def = Define` 416 ALUAWRITE ic is obaselatch = 417 (is = t3) /\ ((ic = data_proc) \/ (ic = mrs_msr) \/ 418 (ic = ldr) \/ (ic = str) \/ (ic = ldm) \/ 419 (ic = ldc) \/ (ic = stc)) \/ 420 (is = t4) /\ ((ic = reg_shift) \/ (ic = ldm)) \/ 421 (is = tn) /\ (ic = mla_mul) \/ 422 ~(is = tn) /\ (ic = stm) \/ 423 ~(is = t4) /\ ((ic = br) \/ (ic = swi_ex)) \/ 424 (ic = ldm) /\ obaselatch`; 425 426val ALUBWRITE_def = Define` 427 ALUBWRITE ic is = 428 ~((ic = stm) /\ ~(is = t3) \/ 429 (is = t4) /\ ((ic = ldr) \/ (ic = str) \/ (ic = swp) \/ (ic = ldm)) \/ 430 (is = tn) /\ ((ic = ldc) \/ (ic = stc)))`; 431 432val BASELATCH_def = Define` 433 BASELATCH ic is = (ic = ldm) /\ (is = t4)`; 434 435val NCPI_def = Define` 436 NCPI ic = ~((ic = cdp_und) \/ (ic = mcr) \/ (ic = mrc) \/ 437 (ic = ldc) \/ (ic = stc))`; 438 439val RWA_def = Define` 440 RWA ic is ireg (list:word16) oorp dataabt = 441 let bits1916 = ^Rg 19 16 ireg 442 and bits1512 = ^Rg 15 12 ireg 443 and bit21 = ireg %% 21 444 and bit23 = ireg %% 23 445 and bit24 = ireg %% 24 in 446 if ((is = t3) /\ (ic = data_proc) \/ 447 (is = t4) /\ (ic = reg_shift)) /\ (~bit24 \/ bit23) \/ 448 (is = t3) /\ (ic = mrs_msr) /\ ~bit21 \/ 449 ((is = t5) /\ ((ic = ldr) \/ (ic = mrc) /\ ~(bits1512 = 15w)) \/ 450 (is = t6) /\ (ic = swp)) /\ ~dataabt then 451 (T,bits1512) 452 else if (ic = ldm) /\ (list = 0w) /\ ~dataabt /\ (is = tm) \/ 453 (ic = mla_mul) /\ 454 ((bits1916 = 15w) \/ (bits1916 = ^Rg 3 0 ireg)) then 455 (F,ARB) 456 else if (is = t4) /\ 457 (((ic = ldr) \/ (ic = str)) /\ (~bit24 \/ bit21) \/ 458 ((ic = ldm) \/ (ic = stm)) /\ bit21 /\ ~(bits1916 = 15w)) \/ 459 (is = tm) /\ (ic = ldm) /\ dataabt /\ ~(bits1916 = 15w) \/ 460 (is = tn) /\ 461 ((ic = ldc) \/ (ic = stc)) /\ bit21 /\ ~(bits1916 = 15w) \/ 462 (ic = mla_mul) then 463 (T,bits1916) 464 else if ((is = t4) \/ (is = t5)) /\ 465 (((ic = br) /\ bit24) \/ (ic = swi_ex)) then 466 (T,14w) 467 else if (ic = ldm) /\ ((is = tn) \/ (is = tm)) /\ ~dataabt then 468 (T,oorp) 469 else (F,ARB)`; 470 471(* ------------------------------------------------------------------------- *) 472(* Data Path Control: Instruction Execute Phase 2 -------------------------- *) 473(* ------------------------------------------------------------------------- *) 474 475val ALU6_def = Define` 476 ALU6 ic is ireg borrow2 (mul:word2) dataabt alua alub c = 477 let opc = ^Rg 24 21 ireg in 478 if ((ic = data_proc) /\ (is = t3)) \/ 479 ((ic = reg_shift) /\ (is = t4)) then 480 ALU opc alua alub c 481 else if (ic = mrs_msr) /\ (is = t3) then 482 ALU_logic (if ireg %% 21 then alub else alua) 483 else if ic = mla_mul then 484 if is = t3 then 485 if ireg %% 21 then ALU_logic alub else ALU_logic 0w 486 else 487 if ~borrow2 /\ (mul = 0w) \/ borrow2 /\ (mul = 3w) then 488 ALU_logic alua 489 else if borrow2 /\ (mul = 0w) \/ (mul = 1w) then 490 ADD alua alub F 491 else 492 SUB alua alub T 493 else if (ic = ldr) \/ (ic = str) \/ (ic = ldc) \/ (ic = stc) then 494 if (is = t3) /\ ~(ireg %% 24) then 495 ALU_logic alua 496 else if (is = t3) \/ 497 ((is = t4) /\ (ic = ldr) \/ (ic = str)) \/ 498 ((is = tn) /\ (ic = ldc) \/ (ic = stc)) then 499 if ireg %% 23 then ADD alua alub F else SUB alua alub T 500 else if (is = t5) /\ (ic = ldr) then 501 ALU_logic alub 502 else 503 ARB 504 else if (ic = ldm) \/ (ic = stm) then 505 (let bit24 = ireg %% 24 506 and bit23 = ireg %% 23 in 507 if is = t3 then 508 if bit24 then 509 if bit23 then 510 ADD alua alub T 511 else 512 ADD (~alua) alub F 513 else 514 if bit23 then 515 ALU_logic alub 516 else 517 ADD (~alua) alub T 518 else if is = t4 then 519 if (15 >< 0) ireg = 0w:word16 then 520 ALU_logic alub 521 else if bit23 then 522 ADD alua alub T 523 else 524 ADD (~alua) alub F 525 else if (ic = ldm) /\ (is = tm) /\ dataabt then 526 ALU_logic alua 527 else if (ic = ldm) /\ ((is = tn) \/ (is = tm)) then 528 ALU_logic alub 529 else ARB) 530 else if (is = t3) /\ (ic = br) then 531 ADD alua alub F 532 else if (ic = br) \/ (ic = swi_ex) then 533 if is = t4 then ALU_logic alua else 534 if is = t5 then ADD (~alua) alub F else ARB 535 else if (ic = swp) \/ (is = t5) /\ (ic = mrc) then 536 ALU_logic alub 537 else ARB`; 538 539val MSHIFT_def = Define` 540 MSHIFT ic borrow mul count1 = 541 if ic = mla_mul then 542 MSHIFT2 borrow mul count1 543 else 544 ARB`; 545 546val PSRWA_def = Define` 547 PSRWA ic is ireg nbs = 548 let bits1916 = ^Rg 19 16 ireg 549 and bit22 = ireg %% 22 550 and bit21 = ireg %% 21 551 and bit20 = ireg %% 20 552 and bit19 = ireg %% 19 553 and bit16 = ireg %% 16 in 554 if bit20 /\ 555 (((is = t3) /\ (ic = data_proc)) \/ 556 ((is = t4) /\ (ic = reg_shift)) \/ 557 ((is = tn) /\ (ic = mla_mul)) /\ 558 ~((bits1916 = 15w) \/ (bits1916 = ^Rg 3 0 ireg))) \/ 559 (is = t5) /\ (ic = mrc) \/ 560 (is = t3) /\ (ic = swi_ex) \/ 561 (is = tm) /\ (ic = ldm) /\ ~USER nbs /\ bit22 then 562 (T,T) 563 else if (is = t3) /\ (ic = mrs_msr) then 564 if ~bit21 \/ (~bit19 /\ ~bit16) \/ 565 (USER nbs /\ (bit22 \/ (~bit19 /\ bit16))) then 566 (F,ARB) 567 else 568 (T,~bit22) 569 else if (is = t4) /\ (ic = swi_ex) then 570 (T,F) 571 else 572 (F,ARB)`; 573 574val PSRDAT_def = Define` 575 PSRDAT ic is ireg nbs (oorp:word4) dataabt (aregn:word3) 576 cpsrl psrfb alu sctlc = 577 let bit24 = ireg %% 24 578 and bit23 = ireg %% 23 579 and bit22 = ireg %% 22 580 and bit21 = ireg %% 21 581 and bit20 = ireg %% 20 582 and bit19 = ireg %% 19 583 and bit16 = ireg %% 16 584 and bits1512 = ^Rg 15 12 ireg 585 in 586 if bit20 /\ (((is = t3) /\ (ic = data_proc)) \/ 587 ((is = t4) /\ (ic = reg_shift))) then 588 let (n,z,c,v) = FST alu in 589 if bit24 /\ ~bit23 then 590 if ~bit22 then 591 SET_NZC (n,z,sctlc) cpsrl 592 else 593 SET_NZCV (n,z,c,v) cpsrl 594 else if bits1512 = 15w then 595 if USER nbs then 596 cpsrl 597 else 598 psrfb 599 else if (~bit23 /\ ~bit22) \/ (bit24 /\ bit23) then 600 SET_NZC (n,z,sctlc) cpsrl 601 else 602 SET_NZCV (n,z,c,v) cpsrl 603 else if bit20 /\ (is = tn) /\ (ic = mla_mul) then 604 let (n,z,c,v) = FST alu in SET_NZC (n,z,sctlc) cpsrl 605 else if (is = t5) /\ (ic = mrc) then 606 if bits1512 = 15w then 607 SET_NZCV (NZCV (SND alu)) cpsrl 608 else 609 cpsrl 610 else if (is = t3) /\ (ic = mrs_msr) then 611 let aluout = SND alu in 612 if USER nbs then 613 if ~bit22 /\ bit19 then 614 word_modify (\i b. 28 <= i /\ aluout %% i \/ i < 28 /\ b) psrfb 615 else 616 ARB 617 else 618 word_modify (\i b. 28 <= i /\ (if bit19 then aluout %% i else b) \/ 619 8 <= i /\ i <= 27 /\ b \/ 620 i <= 7 /\ (if bit16 then aluout %% i else b)) psrfb 621 else if (is = t3) /\ (ic = swi_ex) then 622 SET_IFMODE T (if (aregn = 0w) \/ (aregn = 7w) then T else cpsrl %% 6) 623 (exception2mode (num2exception (w2n aregn))) cpsrl 624 else if (is = t4) /\ (ic = swi_ex) then 625 psrfb 626 else if (is = tm) /\ (ic = ldm) then 627 if (oorp = 15w) /\ ~dataabt then psrfb else cpsrl 628 else 629 ARB`; 630 631(* ------------------------------------------------------------------------- *) 632(* Pipeline Control: phase 1 ----------------------------------------------- *) 633(* ------------------------------------------------------------------------- *) 634 635val ABORTINST_def = Define` 636 ABORTINST iregval onewinst ointstart ireg flags = 637 ~iregval \/ (onewinst /\ ~ointstart /\ ~CONDITION_PASSED flags ireg)`; 638 639val DATAABT_def = Define` 640 DATAABT dataabt2 endinst = dataabt2 /\ ~endinst`; 641 642val IC_def = Define` 643 IC abortinst nxtic = 644 if abortinst then unexec else nxtic`; 645 646val IS_def = Define` 647 IS abortinst nxtis = 648 if abortinst then t3 else nxtis`; 649 650val COPROC1_def = Define` 651 COPROC1 cpa ncpi = cpa /\ ~ncpi`; 652 653val DATAABT1_def = Define` 654 DATAABT1 dataabt2 endinst mrq2 nopc1 abort = 655 dataabt2 /\ ~endinst \/ mrq2 /\ nopc1 /\ abort`; 656 657val FIQACT_def = Define` 658 FIQACT cpsrf ooonfq = ~cpsrf /\ ~ooonfq`; 659 660val IRQACT_def = Define` 661 IRQACT cpsri oooniq = ~cpsri /\ ~oooniq`; 662 663val PCCHANGE_def = Define` 664 PCCHANGE rwa = let (rw,a:word4) = rwa in rw /\ (a = 15w)`; 665 666val RESETLATCH_def = Define` 667 RESETLATCH ph1 oorst resetstart resetlatch = 668 if ph1 then 669 oorst \/ resetlatch 670 else (* ph2 *) 671 if oorst \/ resetstart then oorst else resetlatch`; 672 673val RESETSTART_def = Define` 674 RESETSTART resetlatch oorst = resetlatch /\ ~oorst`; 675 676val INTSEQ_def = Define` 677 INTSEQ mrq2 nopc1 abort dataabt2 endinst ncpi cpa cpb 678 fiqact iregabt1 irqact resetlatch oorst = 679 mrq2 /\ nopc1 /\ abort \/ 680 dataabt2 /\ ~endinst \/ 681 ~ncpi /\ cpa /\ cpb \/ 682 fiqact \/ iregabt1 \/ irqact \/ 683 resetlatch /\ ~oorst`; 684 685val NEWINST_def = Define` 686 NEWINST ic is cpb intseq pencz mulx = 687 (ic = data_proc) \/ (ic = mrs_msr) \/ (ic = unexec) \/ 688 (ic = cdp_und) /\ ~cpb \/ 689 ((ic = cdp_und) \/ (ic = mcr) \/ (ic = mrc) \/ 690 (ic = ldc) \/ (ic = stc)) /\ ((is = t3) /\ cpb /\ intseq) \/ 691 (ic = mcr) /\ (is = t4) \/ 692 (ic = mrc) /\ (is = t5) \/ 693 ((ic = ldc) \/ (ic = stc)) /\ (is = tn) /\ cpb \/ 694 (((ic = str) \/ (ic = reg_shift)) /\ (is = t4)) \/ 695 (((ic = ldr) \/ (ic = br) \/ (ic = swi_ex)) /\ (is = t5)) \/ 696 (ic = ldm) /\ (is = tm) \/ 697 ((ic = swp) /\ (is = t6)) \/ 698 (ic = mla_mul) /\ (is = tn) /\ mulx \/ 699 (ic = stm) /\ pencz /\ ((is = t4) \/ (is = tn))`; 700 701val PIPEALL_def = Define` 702 PIPEALL opipebll = opipebll`; 703 704val PIPEBLL_def = Define` 705 PIPEBLL ic newinst = 706 newinst \/ (ic = br) \/ (ic = swi_ex)`; 707 708val PIPECWRITE_def = Define` 709 PIPECWRITE newinst = newinst`; 710 711(* ------------------------------------------------------------------------- *) 712(* Pipeline Control: phase 2 ----------------------------------------------- *) 713(* ------------------------------------------------------------------------- *) 714 715val NXTIC_def = Define` 716 NXTIC intstart newinst ic ireg = 717 if ~newinst then 718 ic 719 else if intstart then 720 swi_ex 721 else 722 DECODE_INST ireg`; 723 724val INC_IS_def = Define`INC_IS is = num2iseq (iseq2num is + 1)`; 725 726val NXTIS_def = Define` 727 NXTIS ic is newinst cpb pencz = 728 if newinst \/ 729 ((ic = cdp_und) \/ (ic = mcr) \/ (ic = mrc) \/ 730 (ic = ldc) \/ (ic = stc)) /\ (is = t3) /\ cpb then 731 t3 732 else if ((is = t4) \/ (is = tn)) /\ (ic = ldm) then 733 if pencz then tm else tn 734 else if ((is = t4) \/ (is = tn)) /\ (ic = stm) \/ (ic = mla_mul) \/ 735 ((ic = ldc) \/ (ic = stc)) /\ ~cpb then 736 tn 737 else 738 INC_IS is`; 739 740val PIPEAWRITE_def = Define` 741 PIPEAWRITE pipeall = pipeall`; 742 743val PIPEBWRITE_def = Define` 744 PIPEBWRITE pipebll = pipebll`; 745 746val PIPESTATAWRITE_def = Define` 747 PIPESTATAWRITE pipeall pcchange = pipeall \/ pcchange`; 748 749val PIPESTATBWRITE_def = Define` 750 PIPESTATBWRITE pipebll pcchange = pipebll \/ pcchange`; 751 752val PIPESTATIREGWRITE_def = Define` 753 PIPESTATIREGWRITE pipeall newinst srst = 754 pipeall \/ newinst \/ srst`; 755 756val PIPEAVAL_def = Define` 757 PIPEAVAL srst pcchange = srst \/ ~pcchange`; 758 759val IREGVAL_def = Define` 760 IREGVAL pipecval srst pcchange = pipecval /\ ~srst /\ ~pcchange`; 761 762val PIPEAABT_def = Define` 763 PIPEAABT abortlatch srst pcchange = abortlatch /\ (srst \/ ~pcchange)`; 764 765val IREGABT2_def = Define` 766 IREGABT2 iregabt1 srst pcchange = iregabt1 /\ ~srst /\ ~pcchange`; 767 768val AREGN1_def = Define` 769 AREGN1 resetstart dataabt1 fiqactl irqactl coproc1 iregabt2 = 770 if resetstart then 0w else 771 if dataabt1 then 4w else 772 if fiqactl then 7w else 773 if irqactl then 6w else 774 if coproc1 then 1w else 775 if iregabt2 then 3w else 2w:word3`; 776 777val ENDINST_def = Define` 778 ENDINST resetstart iregval newinst = 779 resetstart \/ iregval /\ newinst`; 780 781(* ------------------------------------------------------------------------- *) 782(* The State Function ------------------------------------------------------ *) 783(* ------------------------------------------------------------------------- *) 784 785val NEXT_ARM6_def = Define` 786 NEXT_ARM6 (^arm6state) (NRESET,ABORT,NFQ,NIQ,DATA,CPA,CPB) = 787 let cpsr = CPSR_READ psr 788 in 789 let (nzcv,cpsri,cpsrf,m) = DECODE_PSR cpsr 790 and list = (15 >< 0) ireg 791 in 792 let abortinst = ABORTINST iregval onewinst ointstart ireg nzcv (* PIPELINE CONTROL: PHASE 1 *) 793 and dataabt = DATAABT dataabt2 endinst 794 in 795 let ic = IC abortinst nxtic 796 and is = IS abortinst nxtis 797 in 798 let nbs = NBS ic is ireg m (* DATAPATH CONTROL: EXECUTE PHASE 1 *) 799 and rp = RP ic list mask 800 and pencz = PENCZ ic list mask 801 and offset = OFFSET ic is ireg list 802 and din' = FIELD ic is ireg oareg din 803 and rba = RBA ic is ireg orp 804 and raa = RAA ic is ireg 805 in 806 let psrrd = if PSRA ic is ireg then cpsr else SPSR_READ psr nbs 807 and rb = REG_READ6 reg nbs rba 808 and ra = REG_READ6 reg nbs raa 809 in 810 let busb = BUSB ic is ireg din' rb 811 and busa = BUSA ic is psrrd ra offset 812 in 813 let shifter = SHIFTER ic is ireg oareg mshift sctrlreg busb (CARRY nzcv) 814 and borrow = BORROW ic is mul 815 and count1 = COUNT1 ic is mshift 816 and mul1 = MUL1 ic is ra mul2 817 and mulz = MULZ ic is mul2 818 in 819 let mulx = MULX ic is mulz borrow mshift 820 and psrfb' = if PSRFBWRITE ic is then psrrd else psrfb 821 and sctrlreg' = if SCTRLREGWRITE ic is then ra else sctrlreg 822 and shcout = FST shifter 823 and alua' = if ALUAWRITE ic is obaselatch then busa else alua 824 and alub' = if ALUBWRITE ic is then (SND shifter) else alub 825 and baselatch = BASELATCH ic is 826 and ncpi = NCPI ic 827 and rwa = RWA ic is ireg list oorp dataabt 828 in 829 let nmreq = NMREQ ic is pencz mulx CPB (* DATAPATH CONTROL: INSTRUCTION FETCH PHASE 1 *) 830 and pcwa = PCWA ic is ireg CPB 831 in 832 let orst = ~NRESET (* PIPELINE CONTROL: PHASE 1 *) 833 and srst = oorst 834 and oonfq = onfq 835 and ooniq = oniq 836 and iregabt1 = pipebabt 837 and coproc1 = COPROC1 CPA ncpi 838 and dataabt1 = DATAABT1 dataabt2 endinst mrq2 nopc1 ABORT 839 and fiqactl = FIQACT cpsrf ooonfq 840 and irqactl = IRQACT cpsri oooniq 841 and pcchange = PCCHANGE rwa 842 and abortlatch = ABORT 843 and resetlatch' = RESETLATCH T oorst ARB resetlatch 844 and aregn = aregn2 845 in 846 let resetstart = RESETSTART resetlatch' oorst 847 and intstart = INTSEQ mrq2 nopc1 ABORT dataabt2 endinst ncpi CPA CPB 848 fiqactl iregabt1 irqactl resetlatch' oorst 849 in 850 let newinst = NEWINST ic is CPB intstart pencz mulx 851 in 852 let pipeall = PIPEALL opipebll 853 and pipebll = PIPEBLL ic newinst 854 and pipec = if PIPECWRITE newinst then pipeb else ireg 855 and pipecval = pipebval 856 in 857 let mul' = (1 >< 0) mul1 (* DATAPATH CONTROL: PIPELINE PHASE 2 *) 858 and mul2' = (31 -- 2) mul1 859 in 860 let alu = ALU6 ic is ireg borrow2 mul dataabt alua' alub' (CARRY nzcv) (* DATAPATH CONTROL: EXECUTE PHASE 2 *) 861 and mshift' = MSHIFT ic borrow mul' count1 862 and psrwa = PSRWA ic is ireg nbs 863 in 864 let aluout = SND alu 865 and psrdat = PSRDAT ic is ireg nbs oorp dataabt aregn cpsr 866 psrfb' alu shcout 867 and inc = areg + 4w 868 and pcbus = REG_READ6 reg usr 15w 869 in 870 let reg' = if pcwa then REG_WRITE reg nbs 15w inc else reg 871 in 872 let reg'' = if FST rwa then REG_WRITE reg' nbs (SND rwa) aluout else reg' 873 and psr' = if FST psrwa then 874 if SND psrwa then CPSR_WRITE psr psrdat 875 else SPSR_WRITE psr nbs psrdat 876 else psr 877 in 878 let nxtic' = NXTIC intstart newinst ic pipec (* PIPELINE CONTROL: PHASE 2 *) 879 and nxtis' = NXTIS ic is newinst CPB pencz 880 and oorst' = orst 881 and pipea' = if PIPEAWRITE pipeall then DATA else pipea 882 in 883 let pipeb' = if PIPEBWRITE pipebll then pipea' else pipeb 884 and (pipeaval',pipeaabt') = 885 if PIPESTATAWRITE pipeall pcchange then 886 (PIPEAVAL srst pcchange, PIPEAABT abortlatch srst pcchange) 887 else (pipeaval, pipeaabt) 888 in 889 let (pipebval',pipebabt') = 890 if PIPESTATBWRITE pipebll pcchange then 891 (pipeaval', pipeaabt') 892 else (pipebval, pipebabt) 893 and (iregval',iregabt2') = 894 if PIPESTATIREGWRITE pipeall newinst srst then 895 (IREGVAL pipecval srst pcchange, IREGABT2 iregabt1 srst pcchange) 896 else (iregval, iregabt2) 897 in 898 let aregn1 = AREGN1 resetstart dataabt1 fiqactl irqactl coproc1 iregabt2' 899 and endinst' = ENDINST resetstart iregval' newinst 900 and resetlatch'' = RESETLATCH F oorst' resetstart resetlatch' 901 in 902 let nxtdin = if DINWRITE ic is then DIN ic is pipec DATA else din (* DATAPATH CONTROL: DECODE PHASE 2 *) 903 and mask' = MASK nxtic' nxtis' mask rp 904 in 905 let nbw' = NBW ic is ireg (* DATAPATH CONTROL: FETCH PHASE 2 *) 906 and nopc = NOPC ic is pencz CPB 907 and nrw' = NRW ic is pencz CPB 908 and oareg' = (1 >< 0) areg 909 and areg' = AREG ic is ireg aregn inc pcbus aluout list 910 pencz oorp CPB dataabt 911 in 912 ARM6 (DP reg'' psr' areg' nxtdin alua' alub' busb) 913 (CTRL pipea' pipeaval' pipeb' pipebval' pipec iregval' intstart newinst 914 endinst' baselatch pipebll nxtic' nxtis' nopc oorst' resetlatch'' 915 NFQ oonfq NIQ ooniq pipeaabt' pipebabt' iregabt2' dataabt1 aregn1 916 (~nmreq) nbw' nrw' sctrlreg' psrfb' oareg' mask' rp orp mul' mul2' 917 borrow mshift')`; 918 919val OUT_ARM6_def = Define` 920 OUT_ARM6 (^arm6state) = (dout,~mrq2,nopc1,nrw,nbw,areg)`; 921 922val INIT_ARM6_def = Define` 923 INIT_ARM6 (^arm6state) = 924 let ointstart1 = ~(aregn2 = 2w) in 925 let nxtic1 = if ointstart1 then swi_ex else NXTIC F T nxtic ireg in 926 ARM6 (DP reg psr (if ointstart1 then areg else REG_READ6 reg usr 15w) 927 (if ointstart1 then din else ireg) alua alub dout) 928 (CTRL pipea T pipeb T ireg T 929 ointstart1 T T obaselatch T nxtic1 t3 F F F 930 onfq ooonfq oniq oooniq pipeaabt pipebabt iregabt2 dataabt2 931 aregn2 mrq2 nbw F sctrlreg psrfb oareg 932 (MASK nxtic1 t3 mask ARB) orp oorp mul mul2 borrow2 mshift)`; 933 934val STATE_ARM6_def = Define` 935 (STATE_ARM6 0 x = INIT_ARM6 x.state) /\ 936 (STATE_ARM6 (SUC t) x = NEXT_ARM6 (STATE_ARM6 t x) (x.inp t))`; 937 938val ARM6_SPEC_def = Define` 939 ARM6_SPEC t x = let s = STATE_ARM6 t x in 940 <| state := s; out := OUT_ARM6 s |>`; 941 942(* ------------------------------------------------------------------------- *) 943(* Projections ------------------------------------------------------------- *) 944(* ------------------------------------------------------------------------- *) 945 946val arm6inp = 947 ``(NRESET:bool,ABORT:bool,NFIQ:bool,NIRQ:bool,DATA:word32,CPA:bool,CPB:bool)``; 948 949val PROJ_NRESET_def = Define `PROJ_NRESET (^arm6inp) = NRESET`; 950val PROJ_ABORT_def = Define `PROJ_ABORT (^arm6inp) = ABORT`; 951val PROJ_NFIQ_def = Define `PROJ_NFIQ (^arm6inp) = NFIQ`; 952val PROJ_NIRQ_def = Define `PROJ_NIRQ (^arm6inp) = NIRQ`; 953val PROJ_DATA_def = Define `PROJ_DATA (^arm6inp) = DATA`; 954val PROJ_CPA_def = Define `PROJ_CPA (^arm6inp) = CPA`; 955val PROJ_CPB_def = Define `PROJ_CPB (^arm6inp) = CPB`; 956 957val IS_RESET_def = Define `IS_RESET i (t:num) = ~PROJ_NRESET (i t)`; 958val IS_ABORT_def = Define `IS_ABORT i (t:num) = PROJ_ABORT (i t)`; 959val IS_FIQ_def = Define `IS_FIQ i (t:num) = ~PROJ_NFIQ (i t)`; 960val IS_IRQ_def = Define `IS_IRQ i (t:num) = ~PROJ_NIRQ (i t)`; 961val IS_ABSENT_def = Define `IS_ABSENT i (t:num) = PROJ_CPA (i t)`; 962val IS_BUSY_def = Define `IS_BUSY i (t:num) = PROJ_CPB (i t)`; 963 964val arm6out = 965 ``(dout:word32, mrq2:bool, nopc1:bool, nrw:bool, nbw:bool, areg:word32)``; 966 967val IS_MEMOP_def = Define `IS_MEMOP (^arm6out) = nopc1`; 968 969(* ------------------------------------------------------------------------- *) 970(* The Uniform Immersion --------------------------------------------------- *) 971(* ------------------------------------------------------------------------- *) 972 973val CP_INTERRUPT_def = Define` 974 CP_INTERRUPT (onfq,ooonfq,oniq,oooniq,cpsrf,cpsri,pipebabt) i n = 975 IS_ABSENT i n \/ 976 ~cpsrf /\ (if n = 0 then ~ooonfq else 977 if n = 1 then ~onfq else IS_FIQ i (n - 2)) \/ 978 ~cpsri /\ (if n = 0 then ~oooniq else 979 if n = 1 then ~oniq else IS_IRQ i (n - 2)) \/ 980 pipebabt`; (* abort on fetch *) 981 982val BUSY_WAIT_DONE_def = Define` 983 BUSY_WAIT_DONE iflags i n = IS_BUSY i n ==> CP_INTERRUPT iflags i n`; 984 985val BUSY_WAIT_def = Define` 986 BUSY_WAIT x i = LEAST n. BUSY_WAIT_DONE x i n`; 987 988val DUR_IC_def = Define` 989 DUR_IC ic ireg rs iflags inp = 990 if (ic = br) \/ (ic = swi_ex) then 991 3 992 else if (ic = mrs_msr) \/ (ic = data_proc) then 993 if PCCHANGE (RWA ic t3 ireg ARB ARB ARB) then 3 else 1 994 else if ic = reg_shift then 995 if PCCHANGE (RWA ic t4 ireg ARB ARB ARB) then 4 else 2 996 else if ic = ldr then 997 if PCCHANGE (RWA ic t4 ireg ARB ARB ARB) \/ 998 PCCHANGE (RWA ic t5 ireg ARB ARB (IS_ABORT inp 1)) then 5 else 3 999 else if ic = str then 1000 if PCCHANGE (RWA ic t4 ireg ARB ARB ARB) then 4 else 2 1001 else if ic = swp then 1002 if PCCHANGE (RWA ic t6 ireg ARB ARB 1003 (IS_ABORT inp 1 \/ IS_ABORT inp 2)) then 6 else 4 1004 else if ic = mla_mul then 1005 1 + MLA_MUL_DUR rs 1006 else let l = LENGTH (REGISTER_LIST ((15 >< 0) ireg)) in 1007 if ic = ldm then 1008 2 + (l - 1) + 1 + 1009 (if ireg %% 15 /\ ~(?s. s < l /\ IS_ABORT inp (s + 1)) then 2 else 0) 1010 else if ic = stm then 1011 2 + (l - 1) 1012 else let b = BUSY_WAIT iflags inp in 1013 if (ic = cdp_und) \/ 1014 ic IN {mcr; mrc; ldc; stc} /\ IS_BUSY inp b /\ 1015 CP_INTERRUPT iflags inp b then 1016 1 + b 1017 else if ic = mcr then 1018 1 + b + 1 1019 else if ic = mrc then 1020 1 + b + 2 1021 else if (ic = ldc) \/ (ic = stc) then 1022 1 + b + (LEAST n. IS_BUSY (ADVANCE b inp) n) 1023 else (* unexec *) 1024 1`; 1025 1026val IFLAGS_def = Define` 1027 IFLAGS x = case x of (^arm6state) => 1028 let (flags,cpsri,cpsrf,m) = DECODE_PSR (CPSR_READ psr) in 1029 (onfq,ooonfq,oniq,oooniq,cpsrf,cpsri,pipebabt)`; 1030 1031val DUR_X_def = Define` 1032 DUR_X x = case x.state of (^arm6state) => 1033 let (flags,cpsri,cpsrf,m) = DECODE_PSR (CPSR_READ psr) in 1034 let abortinst = ABORTINST iregval onewinst ointstart ireg flags in 1035 let ic = IC abortinst nxtic 1036 and rs = REG_READ6 reg (DECODE_MODE m) (^Rg 11 8 ireg) in 1037 let d = DUR_IC ic ireg rs (IFLAGS x.state) x.inp 1038 in 1039 if ?t. t < d /\ IS_RESET x.inp t then (* oorst = F *) 1040 (T,(LEAST t. IS_RESET x.inp t /\ 1041 ~IS_RESET x.inp (t + 1) /\ ~IS_RESET x.inp (t + 2)) + 3) 1042 else 1043 (F,d)`; 1044 1045val DUR_ARM6_def = Define`DUR_ARM6 x = SND (DUR_X x)`; 1046 1047val IMM_ARM6_def = Define` 1048 (IMM_ARM6 x 0 = 0) /\ 1049 (IMM_ARM6 x (SUC t) = 1050 DUR_ARM6 <|state := STATE_ARM6 (IMM_ARM6 x t) x; 1051 inp := ADVANCE (IMM_ARM6 x t) x.inp|> + IMM_ARM6 x t)`; 1052 1053(* ------------------------------------------------------------------------- *) 1054(* The Data Abstraction ---------------------------------------------------- *) 1055(* ------------------------------------------------------------------------- *) 1056 1057val SUB8_PC_def = Define `SUB8_PC (reg:reg) = (r15 =+ reg r15 - 8w) reg`; 1058val ADD8_PC_def = Define `ADD8_PC (reg:reg) = (r15 =+ reg r15 + 8w) reg`; 1059 1060val ABS_ARM6_def = Define` 1061 ABS_ARM6 (^arm6state) = 1062 ARM_EX (ARM (SUB8_PC reg) psr) ireg (num2exception (w2n aregn2))`; 1063 1064(* ------------------------------------------------------------------------- *) 1065(* Stream Domain and Abstraction ------------------------------------------- *) 1066(* ------------------------------------------------------------------------- *) 1067 1068val STRM_ARM6_def = Define` 1069 STRM_ARM6 i = 1070 (!t. IS_RESET i t ==> 1071 ~(t = 0) /\ IS_RESET i (t - 1) \/ 1072 (IS_RESET i (t + 1) /\ IS_RESET i (t + 2) /\ IS_RESET i (t + 3))) /\ 1073 (!t. IS_ABSENT i t ==> IS_BUSY i t) /\ 1074 (!t. ?t2. t < t2 /\ ~IS_RESET i t2 /\ ~IS_RESET i (t2 + 1)) /\ 1075 (!t. ?t2. t < t2 /\ (IS_BUSY i t2 ==> IS_ABSENT i t2)) /\ 1076 (!t. ~IS_BUSY i t ==> ?t2. t < t2 /\ IS_BUSY i t2)`; 1077 1078val exc2exception_def = Define` 1079 exc2exception exc a n = 1080 case exc of 1081 reset => SOME (Reset a) 1082 | dabort => SOME (Dabort n) 1083 | fast => SOME Fiq 1084 | interrupt => SOME Irq 1085 | pabort => SOME Prefetch 1086 | undefined => SOME Undef 1087 | _ => NONE`; 1088 1089val SMPL_EXC_ARM6_def = Define` 1090 SMPL_EXC_ARM6 x t = 1091 case ABS_ARM6 (STATE_ARM6 (IMM_ARM6 x (t + 1)) x) of 1092 ARM_EX state ireg exc => 1093 (exc2exception exc state 1094 (LEAST s. IS_ABORT x.inp (IMM_ARM6 x t + (s + 1))), 1095 let s = IMM_ARM6 x t in 1096 let b = BUSY_WAIT (IFLAGS (STATE_ARM6 s x)) (ADVANCE s x.inp) in 1097 IS_BUSY x.inp (s + b), 1098 ireg)`; 1099 1100val SMPL_DATA_ARM6_def = Define` 1101 SMPL_DATA_ARM6 x = 1102 MAP_STRM TL (PACK (IMM_ARM6 x) (MAP_STRM PROJ_DATA x.inp))`; 1103 1104val SMPL_ARM6_def = Define` 1105 SMPL_ARM6 x = 1106 COMBINE (\(a,b,c) d. (a,b,c,d)) (SMPL_EXC_ARM6 x) (SMPL_DATA_ARM6 x)`; 1107 1108val MOVE_DOUT_def = Define` 1109 MOVE_DOUT x l = 1110 if NULL l then [] else ZIP (SNOC x (TL (MAP FST l)),MAP SND l)`; 1111 1112val MEMOP_def = Define` 1113 MEMOP (^arm6out) = 1114 if nrw then 1115 MemWrite (~nbw) areg dout 1116 else 1117 MemRead areg`; 1118 1119val PROJ_IREG_def = Define `PROJ_IREG (^arm6state) = ireg`; 1120 1121val OSMPL_ARM6_def = Define` 1122 OSMPL_ARM6 x l = 1123 let x0 = SINIT INIT_ARM6 x in 1124 let ireg = PROJ_IREG x0.state in 1125 let ic = DECODE_INST ireg in 1126 if FST (DUR_X x0) \/ 1127 (ic = mcr) \/ (ic = ldc) \/ (ic = stc) 1128 (* in future should add "sanity checks" for coproc. cases e.g. 1129 if executed and no interrupt then: 1130 "l" contains correct sequential memory requsets, 1131 or "l" finishes with DOUT set for write to coproc. *) 1132 then 1133 OUT_ARM (ABS_ARM6 x.state) 1134 else 1135 (MAP MEMOP o FILTER IS_MEMOP o 1136 MOVE_DOUT (FST (OUT_ARM6 (STATE_ARM6 (IMM_ARM6 x 1) x)))) l`; 1137 1138(* ------------------------------------------------------------------------- *) 1139(* Basic Theorems ---------------------------------------------------------- *) 1140(* ------------------------------------------------------------------------- *) 1141 1142val STATE_ARM6_THM = store_thm("STATE_ARM6_THM", 1143 `IMAP ARM6_SPEC INIT_ARM6 NEXT_ARM6 OUT_ARM6`, 1144 RW_TAC (std_ss++boolSimps.LET_ss) [ARM6_SPEC_def,STATE_ARM6_def,IMAP_def]); 1145 1146val STATE_ARM6_IMAP_INIT = store_thm("STATE_ARM6_IMAP_INIT", 1147 `IS_IMAP_INIT ARM6_SPEC INIT_ARM6`, 1148 PROVE_TAC [STATE_ARM6_THM,IS_IMAP_INIT_def]); 1149 1150val STATE_ARM6_IMAP = store_thm("STATE_ARM6_IMAP", 1151 `IS_IMAP ARM6_SPEC`, PROVE_TAC [STATE_ARM6_THM,IS_IMAP_def]); 1152 1153val ARM6_SPEC_STATE = save_thm("ARM6_SPEC_STATE", 1154 (SIMP_CONV (srw_ss()++boolSimps.LET_ss) [ARM6_SPEC_def]) 1155 ``(ARM6_SPEC t x).state``); 1156 1157val STATE_ARM6_COR = save_thm("STATE_ARM6_COR", 1158 REWRITE_RULE [ARM6_SPEC_STATE] (MATCH_MP STATE_FUNPOW_INIT4 STATE_ARM6_THM)); 1159 1160val ARM6_SPEC_OUT = save_thm("ARM6_SPEC_OUT", 1161 REWRITE_RULE [ARM6_SPEC_STATE] (MATCH_MP OUTPUT_THM STATE_ARM6_THM)); 1162 1163val MSHIFT = save_thm("MSHIFT",REWRITE_RULE [MSHIFT2_def] MSHIFT_def); 1164 1165val INC_IS = save_thm("INC_IS", 1166 LIST_CONJ (map (fn is => (GEN_ALL o RIGHT_CONV_RULE (SIMP_CONV arith_ss 1167 [theorem "iseq2num_thm",theorem "num2iseq_thm"]) o SPEC is) INC_IS_def) 1168 [`t3`,`t4`,`t5`])); 1169 1170val DUR_X = save_thm("DUR_X", 1171 (SIMP_RULE (srw_ss()++boolSimps.LET_ss) [DECODE_PSR_def,GSYM IMP_DISJ_THM] o 1172 ONCE_REWRITE_RULE [PROVE [] 1173 ``!a b c. (if a then c else b) = (if ~a then b else c)``] o 1174 SPEC `<|state := (^arm6state); inp := i|>`) DUR_X_def); 1175 1176(* ------------------------------------------------------------------------- *) 1177 1178val _ = export_theory(); 1179