Changeset 1526
 Timestamp:
 Nov 22, 2011, 10:43:47 AM (8 years ago)
 Location:
 src/ASM
 Files:

 2 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 
src/ASM/Status.ma
r1522 r1526 6 6 include "ASM/Arithmetic.ma". 7 7 include "ASM/BitVectorTrie.ma". 8 include "ASM/JMCoercions.ma". 8 9 9 10 definition Time ≝ nat. … … 853 854 qed. 854 855 855 definition set_arg_8: ∀M: Type[0]. PreStatus M → [[ direct ; indirect ; registr ; 856 axiom set_bit_addressable_sfr_ignores_clock: ∀m,s,d,v. clock m s = clock … (set_bit_addressable_sfr … s d v). 857 858 definition set_arg_8: ∀M: Type[0]. ∀s:PreStatus M. [[ direct ; indirect ; registr ; 856 859 acc_a ; acc_b ; ext_indirect ; 857 ext_indirect_dptr ]] → Byte → PreStatus M ≝ 860 ext_indirect_dptr ]] → Byte → Σs':PreStatus M. 861 clock … s = clock … s' ≝ 858 862 λm, s, a, v. 859 863 match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ; 860 864 acc_a ; acc_b ; ext_indirect ; 861 ext_indirect_dptr ]] x) → ? with 865 ext_indirect_dptr ]] x) → 866 Σs':PreStatus m. ?(*clock … s*) = ?(*clock … s'*) 867 (*CSC: bug here if one specified the two clock above*) 868 with 862 869 [ DIRECT d ⇒ 863 870 λdirect: True. … … 899 906 let memory ≝ insert ? 16 address v (external_ram ? s) in 900 907 set_external_ram ? s memory 901  _ ⇒ 908  _ ⇒ 902 909 λother: False. 903 910 match other in False with [ ] 904 911 ] (subaddressing_modein … a). 905 [1,2,3,4: 906 normalize 907 repeat (@ le_S_S) 908 @ le_O_n 909 ] 910 qed. 912 // qed. 911 913 912 914 theorem modulus_less_than: … … 1024 1026 [ BIT_ADDR b ⇒ λbit_addr: True. 1025 1027 let 〈 nu, nl 〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_PSW) in 1026 let bit_1 ≝ get_index_v …nu 0 ? in1028 let bit_1 ≝ get_index_v ?? nu 0 ? in 1027 1029 let 〈 ignore, three_bits 〉 ≝ split ? 1 3 nu in 1028 1030 match bit_1 with
Note: See TracChangeset
for help on using the changeset viewer.