Changeset 1511 for src/ASM/Interpret.ma
 Timestamp:
 Nov 16, 2011, 5:35:24 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Interpret.ma
r1494 r1511 545 545 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with 546 546 [ ADDR11 a ⇒ λaddr11: True. 547 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in547 let new_sp ≝ \snd (half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1)) in 548 548 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 549 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in 549 let pc_bu ≝ \fst (split ? 8 8 (program_counter ? s)) in 550 let pc_bl ≝ \snd (split ? 8 8 (program_counter ? s)) in 550 551 let s ≝ write_at_stack_pointer ? s pc_bl in 551 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in552 let new_sp ≝ \snd (half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1)) in 552 553 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 553 554 let s ≝ write_at_stack_pointer ? s pc_bu in 554 let 〈thr, eig〉 ≝ split ? 3 8 a in 555 let 〈fiv, thr'〉 ≝ split ? 5 3 pc_bu in 555 let thr ≝ \fst (split ? 3 8 a) in 556 let eig ≝ \snd (split ? 3 8 a) in 557 let fiv ≝ \fst (split ? 5 3 pc_bu) in 558 let thr' ≝ \snd (split ? 5 3 pc_bu) in 556 559 let new_addr ≝ (fiv @@ thr) @@ pc_bl in 557 560 set_program_counter ? s new_addr … … 562 565 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with 563 566 [ ADDR16 a ⇒ λaddr16: True. 564 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in567 let new_sp ≝ \snd (half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1)) in 565 568 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 566 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in 569 let pc_bu ≝ \fst (split ? 8 8 (program_counter ? s)) in 570 let pc_bl ≝ \snd (split ? 8 8 (program_counter ? s)) in 567 571 let s ≝ write_at_stack_pointer ? s pc_bl in 568 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in572 let new_sp ≝ \snd (half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1)) in 569 573 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 570 574 let s ≝ write_at_stack_pointer ? s pc_bu in … … 596 600 let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in 597 601 let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in 598 let 〈carry, jmp_addr〉 ≝ half_add ? big_acc dptrin599 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) jmp_addrin602 let jmp_addr ≝ \snd (half_add ? big_acc dptr) in 603 let new_pc ≝ \snd (half_add ? (program_counter ? s) jmp_addr) in 600 604 set_program_counter ? s new_pc 601 605  LJMP addr ⇒ … … 610 614 match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with 611 615 [ RELATIVE r ⇒ λrelative: True. 612 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in616 let new_pc ≝ \snd (half_add ? (program_counter ? s) (sign_extension r)) in 613 617 set_program_counter ? s new_pc 614 618  _ ⇒ λother: False. ⊥ … … 618 622 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with 619 623 [ ADDR11 a ⇒ λaddr11: True. 620 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in 621 let 〈nu, nl〉 ≝ split ? 4 4 pc_bu in 624 let pc_bu ≝ \fst (split ? 8 8 (program_counter ? s)) in 625 let pc_bl ≝ \snd (split ? 8 8 (program_counter ? s)) in 626 let nu ≝ \fst (split ? 4 4 pc_bu) in 627 let nl ≝ \snd (split ? 4 4 pc_bu) in 622 628 let bit ≝ get_index' ? O ? nl in 623 let 〈relevant1, relevant2〉 ≝ split ? 3 8 a in 629 let relevant1 ≝ \fst (split ? 3 8 a) in 630 let relevant2 ≝ \snd (split ? 3 8 a) in 624 631 let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in 625 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) new_addrin632 let new_pc ≝ \snd (half_add ? (program_counter ? s) new_addr) in 626 633 set_program_counter ? s new_pc 627 634  _ ⇒ λother: False. ⊥
Note: See TracChangeset
for help on using the changeset viewer.