Changeset 1514 for src/ASM/Interpret.ma
- Timestamp:
- Nov 17, 2011, 5:41:08 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Interpret.ma
r1511 r1514 582 582 let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in 583 583 let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in 584 let 〈carry, new_addr〉 ≝ half_add ? dptr big_accin584 let new_addr ≝ \snd (half_add ? dptr big_acc) in 585 585 let result ≝ lookup ? ? new_addr (code_memory ? s) (zero ?) in 586 586 set_8051_sfr ? s SFR_ACC_A result 587 587 | ACC_PC ⇒ λacc_pc: True. 588 588 let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in 589 let 〈carry,inc_pc〉 ≝ half_add ? (program_counter ? s) (bitvector_of_nat 16 1) in589 let inc_pc ≝ \snd (half_add ? (program_counter ? s) (bitvector_of_nat 16 1)) in 590 590 (* DPM: Under specified: does the carry from PC incrementation affect the *) 591 591 (* addition of the PC with the DPTR? At the moment, no. *) 592 592 let s ≝ set_program_counter ? s inc_pc in 593 let 〈carry, new_addr〉 ≝ half_add ? inc_pc big_accin593 let new_addr ≝ \snd (half_add ? inc_pc big_acc) in 594 594 let result ≝ lookup ? ? new_addr (code_memory ? s) (zero ?) in 595 595 set_8051_sfr ? s SFR_ACC_A result
Note: See TracChangeset
for help on using the changeset viewer.