Changeset 1526 for src/ASM/Interpret.ma
 Timestamp:
 Nov 22, 2011, 10:43:47 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Interpret.ma
r1522 r1526 1 1 include "ASM/Status.ma". 2 2 include "ASM/Fetch.ma". 3 include "ASM/JMCoercions.ma". 3 4 4 5 definition sign_extension: Byte → Word ≝ … … 119 120 include alias "ASM/BitVectorTrie.ma". 120 121 122 123 lemma set_flags_ignores_clock: 124 ∀M,s,f1,f2,f3. clock M s ≤ clock … (set_flags … s f1 f2 f3). 125 // 126 qed. 127 128 lemma set_args_8_ignores_clock: 129 ∀M,s,f1,f2. clock M s = clock … (set_arg_8 … s f1 f2). 130 #M #s #f1 #f2 cases (set_arg_8 M s f1 f2) 131 #a #E >E // 132 qed. 133 121 134 definition execute_1_preinstruction: 122 135 ∀ticks: nat × nat. 123 ∀A, M: Type[0]. (A → PreStatus M → Word) → preinstruction A → PreStatus M → PreStatus M ≝ 136 ∀A, M: Type[0]. (A → PreStatus M → Word) → preinstruction A → 137 ∀s:PreStatus M. Σs':PreStatus M. clock … s ≤ clock … s' ≝ 124 138 λticks. 125 139 λA, M: Type[0]. … … 210 224 ] 211 225  INC addr ⇒ 212 let s ≝ add_ticks1 s in226 let s' ≝ add_ticks1 s in 213 227 match addr return λx. bool_to_Prop (is_in … [[ acc_a; 214 228 registr; 215 229 direct; 216 230 indirect; 217 dptr ]] x) → ?with231 dptr ]] x) → Σs'.clock … s ≤ clock … s' with 218 232 [ ACC_A ⇒ λacc_a: True. 219 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s true ACC_A) (bitvector_of_nat 8 1) in220 set_arg_8 ? s ACC_A result233 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s' true ACC_A) (bitvector_of_nat 8 1) in 234 eject … (set_arg_8 ? s' ACC_A result) 221 235  REGISTER r ⇒ λregister: True. 222 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s true (REGISTER r)) (bitvector_of_nat 8 1) in223 set_arg_8 ? s (REGISTER r) result236 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s' true (REGISTER r)) (bitvector_of_nat 8 1) in 237 eject … (set_arg_8 ? s' (REGISTER r) result) 224 238  DIRECT d ⇒ λdirect: True. 225 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s true (DIRECT d)) (bitvector_of_nat 8 1) in226 set_arg_8 ? s (DIRECT d) result239 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s' true (DIRECT d)) (bitvector_of_nat 8 1) in 240 eject … (set_arg_8 ? s' (DIRECT d) result) 227 241  INDIRECT i ⇒ λindirect: True. 228 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s true (INDIRECT i)) (bitvector_of_nat 8 1) in229 set_arg_8 ? s (INDIRECT i) result242 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s' true (INDIRECT i)) (bitvector_of_nat 8 1) in 243 eject … (set_arg_8 ? s' (INDIRECT i) result) 230 244  DPTR ⇒ λdptr: True. 231 let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr ? s SFR_DPL) (bitvector_of_nat 8 1) in232 let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr ? s SFR_DPH) (zero 8) carry in233 let s ≝ set_8051_sfr ? s SFR_DPL bl in234 set_8051_sfr ? s SFR_DPH bu245 let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr ? s' SFR_DPL) (bitvector_of_nat 8 1) in 246 let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr ? s' SFR_DPH) (zero 8) carry in 247 let s ≝ set_8051_sfr ? s' SFR_DPL bl in 248 set_8051_sfr ? s' SFR_DPH bu 235 249  _ ⇒ λother: False. ⊥ 236 250 ] (subaddressing_modein … addr) … … 519 533 let s ≝ add_ticks2 s in 520 534 s 521 ]. 522 try assumption 523 try @I535 ]. (*67s*) 536 try assumption (*180s*) 537 try % (*41s*) 524 538 try ( 525 539 @ (execute_1_technical … (subaddressing_modein …)) 526 540 @ I 527 ) 541 ) (*132s*) 542 [(*1:/by/,2,3: /by/*) 543 4: 544 6,7,8,10,11,12,13,14,15: /by/ (*56s*) 545 16,17,18,19,22,23,24,25,26,27,28,29: /by/ (*73s*) 546 33,35,39,41,43,54,55,56: /by/ (*48s*) 547  548 (* 31,32,34,36,44,48 facili *) 549 (* 4,5,9,20,21,30,37,38,40,42,45,46,47,49,50,51,52,53: ??? *) 528 550 qed. 529 551
Note: See TracChangeset
for help on using the changeset viewer.