Changeset 757 for src/ASM/Interpret.ma


Ignore:
Timestamp:
Apr 18, 2011, 12:30:53 PM (9 years ago)
Author:
mulligan
Message:

Lots more fixing to get both front and backends using same conventions and types.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret.ma

    r712 r757  
    156156
    157157include alias "arithmetics/nat.ma".
     158include alias "ASM/BitVectorTrie.ma".
    158159
    159160definition execute_1: Status → Status ≝
     
    172173            let ov_flag ≝ get_index' ? 2 ? flags in
    173174            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
    175176        | ADDC addr1 addr2 ⇒
    176177            let old_cy_flag ≝ get_cy_flag s in
     
    240241        | INC addr ⇒
    241242            match addr return λx. bool_to_Prop (is_in … [[ acc_a;
    242                                                            register;
     243                                                           registr;
    243244                                                           direct;
    244245                                                           indirect;
     
    427428            | _ ⇒ λother: False. ⊥
    428429            ] (subaddressing_modein … addr)
    429         | MOVC addr1 addr2 ⇒
    430           match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → ? with
    431             [ ACC_DPTR ⇒ λacc_dptr: True.
    432               let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in
    433               let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
    434               let 〈carry, new_addr〉 ≝ half_add ? dptr big_acc in
    435               let result ≝ lookup ? ? new_addr (code_memory s) (zero ?) in
    436                 set_8051_sfr s SFR_ACC_A result
    437             | ACC_PC ⇒ λacc_pc: True.
    438               let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in
    439               let 〈carry,inc_pc〉 ≝ half_add ? (program_counter s) (bitvector_of_nat 16 1) in
    440               (* 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 in
    443               let 〈carry, new_addr〉 ≝ half_add ? inc_pc big_acc in
    444               let result ≝ lookup ? ? new_addr (code_memory s) (zero ?) in
    445                 set_8051_sfr s SFR_ACC_A result
    446             | _ ⇒ λother: False. ⊥
    447             ] (subaddressing_modein … addr2)
    448430        | MOVX addr ⇒
    449431          (* DPM: only copies --- doesn't affect I/O *)
     
    631613                ] (subaddressing_modein … addr2)
    632614            ]
     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)
    633634        | NOP ⇒ s
    634635        ]
Note: See TracChangeset for help on using the changeset viewer.