Changeset 757 for src/ASM/Interpret.ma
 Timestamp:
 Apr 18, 2011, 12:30:53 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Interpret.ma
r712 r757 156 156 157 157 include alias "arithmetics/nat.ma". 158 include alias "ASM/BitVectorTrie.ma". 158 159 159 160 definition execute_1: Status → Status ≝ … … 172 173 let ov_flag ≝ get_index' ? 2 ? flags in 173 174 let s ≝ set_arg_8 s ACC_A result in 174 set_flags s cy_flag (Some Bit ac_flag) ov_flag 175 set_flags s cy_flag (Some Bit ac_flag) ov_flag 175 176  ADDC addr1 addr2 ⇒ 176 177 let old_cy_flag ≝ get_cy_flag s in … … 240 241  INC addr ⇒ 241 242 match addr return λx. bool_to_Prop (is_in … [[ acc_a; 242 regist er;243 registr; 243 244 direct; 244 245 indirect; … … 427 428  _ ⇒ λother: False. ⊥ 428 429 ] (subaddressing_modein … addr) 429  MOVC addr1 addr2 ⇒430 match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → ? with431 [ ACC_DPTR ⇒ λacc_dptr: True.432 let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in433 let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in434 let 〈carry, new_addr〉 ≝ half_add ? dptr big_acc in435 let result ≝ lookup ? ? new_addr (code_memory s) (zero ?) in436 set_8051_sfr s SFR_ACC_A result437  ACC_PC ⇒ λacc_pc: True.438 let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in439 let 〈carry,inc_pc〉 ≝ half_add ? (program_counter s) (bitvector_of_nat 16 1) in440 (* DPM: Under specified: does the carry from PC incrementation affect the *)441 (* addition of the PC with the DPTR? At the moment, no. *)442 let s ≝ set_program_counter s inc_pc in443 let 〈carry, new_addr〉 ≝ half_add ? inc_pc big_acc in444 let result ≝ lookup ? ? new_addr (code_memory s) (zero ?) in445 set_8051_sfr s SFR_ACC_A result446  _ ⇒ λother: False. ⊥447 ] (subaddressing_modein … addr2)448 430  MOVX addr ⇒ 449 431 (* DPM: only copies  doesn't affect I/O *) … … 631 613 ] (subaddressing_modein … addr2) 632 614 ] 615  MOVC addr1 addr2 ⇒ 616 match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → ? with 617 [ ACC_DPTR ⇒ λacc_dptr: True. 618 let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in 619 let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in 620 let 〈carry, new_addr〉 ≝ half_add ? dptr big_acc in 621 let result ≝ lookup ? ? new_addr (code_memory s) (zero ?) in 622 set_8051_sfr s SFR_ACC_A result 623  ACC_PC ⇒ λacc_pc: True. 624 let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in 625 let 〈carry,inc_pc〉 ≝ half_add ? (program_counter s) (bitvector_of_nat 16 1) in 626 (* DPM: Under specified: does the carry from PC incrementation affect the *) 627 (* addition of the PC with the DPTR? At the moment, no. *) 628 let s ≝ set_program_counter s inc_pc in 629 let 〈carry, new_addr〉 ≝ half_add ? inc_pc big_acc in 630 let result ≝ lookup ? ? new_addr (code_memory s) (zero ?) in 631 set_8051_sfr s SFR_ACC_A result 632  _ ⇒ λother: False. ⊥ 633 ] (subaddressing_modein … addr2) 633 634  NOP ⇒ s 634 635 ]
Note: See TracChangeset
for help on using the changeset viewer.