Changeset 2705 for src/ASM/Interpret.ma
 Timestamp:
 Feb 22, 2013, 5:56:31 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Interpret.ma
r2504 r2705 184 184  _ ⇒ λother: False. ⊥ 185 185 ] (subaddressing_modein … addr) 186  JMP _ ⇒ λinstr_refl. (* DPM: always indirect_dptr *) 187 let s ≝ add_ticks1 s in 188 let dptr ≝ (get_8051_sfr … s SFR_DPH) @@ (get_8051_sfr … s SFR_DPL) in 189 let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in 190 let jmp_addr ≝ add … big_acc dptr in 191 let new_pc ≝ add … (program_counter … s) jmp_addr in 192 set_program_counter … s new_pc 186 193  NOP ⇒ λinstr_refl. 187 let s ≝ add_ticks 2s in194 let s ≝ add_ticks1 s in 188 195 s 189 196  DEC addr ⇒ λinstr_refl. … … 604 611  _ ⇒ λother: False. ⊥ 605 612 ] (subaddressing_modein … addr) (refl ? (subaddressing_modeel ?? addr)) 613  JMP _ ⇒ λinstr_refl. (* DPM: always indirect_dptr *) 614 let s ≝ add_ticks1 s in 615 let dptr ≝ (get_8051_sfr … s SFR_DPH) @@ (get_8051_sfr … s SFR_DPL) in 616 let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in 617 let jmp_addr ≝ add … big_acc dptr in 618 let new_pc ≝ add … (program_counter … s) jmp_addr in 619 set_program_counter … s new_pc 606 620  NOP ⇒ λinstr_refl. 607 621 let s ≝ add_ticks2 s in … … 938 952 try (change with (cl_jump = cl_other → ?) #absurd destruct(absurd)) 939 953 try (change with (cl_return = cl_other → ?) #absurd destruct(absurd)) 954 try (change with (cl_call = cl_other → ?) #absurd destruct(absurd)) 940 955 try (@or_introl //) 941 956 try (@or_intror //) … … 1045 1060  _ ⇒ λother: False. ⊥ 1046 1061 ] (subaddressing_modein … addr2) 1047  JMP _ ⇒ λinstr_refl. (* DPM: always indirect_dptr *)1048 let s ≝ set_clock ?? s (ticks + clock … s) in1049 let dptr ≝ (get_8051_sfr … s SFR_DPH) @@ (get_8051_sfr … s SFR_DPL) in1050 let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in1051 let jmp_addr ≝ add … big_acc dptr in1052 let new_pc ≝ add … (program_counter … s) jmp_addr in1053 set_program_counter … s new_pc1054 1062  LJMP addr ⇒ λinstr_refl. 1055 1063 let new_pc ≝ compute_target_of_unconditional_jump (program_counter … s) instr in … … 1098 1106 ] (refl … instr). (*10s*) 1099 1107 try assumption 1100 [1,2,3,4,5,6,7 ,8:1108 [1,2,3,4,5,6,7: 1101 1109 normalize nodelta >clock_set_program_counter <INSTR_PC_TICKS % 1102 1110 try // … … 1110 1118 /demod by clock_set_program_counter/ /demod nohyps/ % 1111 1119 ] 1112  9:1120 8: 1113 1121 cases (execute_1_preinstruction_ok 〈ticks, ticks〉 [[ relative ]] ?? 1114 1122 (λx. λs. … … 1190 1198 let s ≝ set_clock … s (\fst ticks + clock … s) in 1191 1199 set_program_counter … s (address_of_word_labels (\snd cm) jmp) 1200  Jnz acc dst1 dst2 ⇒ 1201 if ¬(eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8)) then 1202 let s ≝ set_clock ?? s (\fst ticks + clock … s) in 1203 set_program_counter … s (address_of_word_labels (\snd cm) dst1) 1204 else 1205 let s ≝ set_clock ?? s (\snd ticks + clock … s) in 1206 set_program_counter … s (address_of_word_labels (\snd cm) dst2) 1207  MovSuccessor dst ws lbl ⇒ 1208 let s ≝ set_clock ?? s (\fst ticks + clock … s) in 1209 let addr ≝ address_of_word_labels (\snd cm) lbl in 1210 let 〈high, low〉 ≝ vsplit ? 8 8 addr in 1211 let v ≝ match ws with [ HIGH ⇒ high  LOW ⇒ low ] in 1212 set_arg_8 … s dst v 1192 1213  Call call ⇒ 1193 1214 let s ≝ set_clock ?? s (\fst ticks + clock … s) in … … 1209 1230 in 1210 1231 s. 1211 normalize 1212 @I 1232 [2: %  @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %] 1213 1233 qed. 1214 1234
Note: See TracChangeset
for help on using the changeset viewer.