Ignore:
Timestamp:
Nov 30, 2010, 6:13:00 PM (9 years ago)
Author:
mulligan
Message:

Work on main execution loop. All cases covered. Need to close open proof states and remove computational axioms.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/Interpret.ma

    r343 r347  
    1010  λb.
    1111    zero eight @@ b.
     12
     13naxiom daemon: False.
    1214
    1315ndefinition execute_1: Status → Status ≝
     
    395397            ] (subaddressing_modein … addr)
    396398        | MOVC addr1 addr2 ⇒
    397           match addr2 return λx. bool_to_Prop (is_in [[ acc_dptr; acc_pc ]] x) → ? with
    398             [ ACC_DPTR ⇒ λacc_dptr: True. ?
    399             | ACC_PC ⇒ λacc_pc: True. ?
    400             | _ ⇒ λother: False. ?
    401             ] (subaddressing_modein … ?)
     399          match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → ? with
     400            [ ACC_DPTR ⇒ λacc_dptr: True.
     401              let big_acc ≝ (zero eight) @@ (get_8051_sfr s SFR_ACC_A) in
     402              let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
     403              let 〈carry, new_addr〉 ≝ half_add ? dptr big_acc in
     404              let result ≝ lookup ? ? new_addr (code_memory s) (zero ?) in
     405                set_8051_sfr s SFR_ACC_A result
     406            | ACC_PC ⇒ λacc_pc: True.
     407              let big_acc ≝ (zero eight) @@ (get_8051_sfr s SFR_ACC_A) in
     408              let 〈carry,inc_pc〉 ≝ half_add ? (program_counter s) (bitvector_of_nat sixteen one) in
     409              (* DPM: Under specified: does the carry from PC incrementation affect the *)
     410              (*      addition of the PC with the DPTR? At the moment, no.              *)
     411              let s ≝ set_program_counter s inc_pc in
     412              let 〈carry, new_addr〉 ≝ half_add ? inc_pc big_acc in
     413              let result ≝ lookup ? ? new_addr (code_memory s) (zero ?) in
     414                set_8051_sfr s SFR_ACC_A result
     415            | _ ⇒ λother: False. ?
     416            ] (subaddressing_modein … addr2)
     417        | MOVX addr ⇒
     418          (* DPM: only copies --- doesn't affect I/O *)
     419          match addr with
     420            [ Left l ⇒
     421              let 〈addr1, addr2〉 ≝ l in
     422                set_arg_8 s addr1 (get_arg_8 s false addr2)
     423            | Right r ⇒
     424              let 〈addr1, addr2〉 ≝ r in
     425                set_arg_8 s addr1 (get_arg_8 s false addr2)
     426            ]
     427        | MOV addr ⇒
     428          match addr with
     429            [ Left l ⇒
     430              match l with
     431                [ Left l' ⇒
     432                  match l' with
     433                    [ Left l'' ⇒
     434                      match l'' with
     435                        [ Left l''' ⇒
     436                          match l''' with
     437                            [ Left l'''' ⇒
     438                              let 〈addr1, addr2〉 ≝ l'''' in
     439                                set_arg_8 s addr1 (get_arg_8 s false addr2)
     440                            | Right r'''' ⇒
     441                              let 〈addr1, addr2〉 ≝ r'''' in
     442                                set_arg_8 s addr1 (get_arg_8 s false addr2)
     443                            ]
     444                        | Right r''' ⇒
     445                          let 〈addr1, addr2〉 ≝ r''' in
     446                            set_arg_8 s addr1 (get_arg_8 s false addr2)
     447                        ]
     448                    | Right r'' ⇒
     449                      let 〈addr1, addr2〉 ≝ r'' in
     450                        set_arg_16 s (get_arg_16 s addr2) addr1
     451                    ]
     452                | Right r ⇒
     453                  let 〈addr1, addr2〉 ≝ r in
     454                    set_arg_1 s addr1 (get_arg_1 s addr2 false)
     455                ]
     456            | Right r ⇒
     457              let 〈addr1, addr2〉 ≝ r in
     458                set_arg_1 s addr1 (get_arg_1 s addr2 false)
     459            ]
     460        | LCALL addr ⇒
     461          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with
     462            [ ADDR16 a ⇒ λaddr16: True.
     463              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) in
     464              let s ≝ set_8051_sfr s SFR_SP new_sp in
     465              let 〈pc_bu, pc_bl〉 ≝ split ? eight eight (program_counter s) in
     466              let s ≝ write_at_stack_pointer s pc_bl in
     467              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) in
     468              let s ≝ set_8051_sfr s SFR_SP new_sp in
     469              let s ≝ write_at_stack_pointer s pc_bu in
     470                set_program_counter s a
     471            | _ ⇒ λother: False. ?
     472            ] (subaddressing_modein … addr)
     473        | ACALL addr ⇒
     474          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
     475            [ ADDR11 a ⇒ λaddr11: True.
     476              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) in
     477              let s ≝ set_8051_sfr s SFR_SP new_sp in
     478              let 〈pc_bu, pc_bl〉 ≝ split ? eight eight (program_counter s) in
     479              let s ≝ write_at_stack_pointer s pc_bl in
     480              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) in
     481              let s ≝ set_8051_sfr s SFR_SP new_sp in
     482              let s ≝ write_at_stack_pointer s pc_bu in
     483              let 〈thr, eig〉 ≝ split ? three eight a in
     484              let 〈fiv, thr'〉 ≝ split ? five three pc_bu in
     485              let new_addr ≝ (fiv @@ thr) @@ pc_bl in
     486                set_program_counter s new_addr
     487            | _ ⇒ λother: False. ?
     488            ] (subaddressing_modein … addr)
    402489        | NOP ⇒ s
    403         | _ ⇒ s
    404490        ]
    405491    in
    406492      s.
     493    ncases daemon;
     494nqed.
     495
     496nlet rec execute (n: Nat) (s: Status) on n: Status ≝
     497  match n with
     498    [ Z ⇒ s
     499    | S o ⇒ execute o (execute_1 s)
     500    ].
Note: See TracChangeset for help on using the changeset viewer.