Changeset 338


Ignore:
Timestamp:
Nov 30, 2010, 2:35:04 PM (9 years ago)
Author:
mulligan
Message:

Most jumps finished. Only CJNE to do.

File:
1 edited

Legend:

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

    r337 r338  
    88
    99alias id "inclusive_disjunction" = "cic:/matita/ng/Bool/inclusive_disjunction.fix(0,0,1)".
     10
     11ndefinition sign_extension: Byte → Word ≝
     12  λb.
     13    zero eight @@ b.
    1014
    1115ndefinition execute_1: Status → Status ≝
     
    176180            let s ≝ set_8051_sfr s SFR_ACC_A old_addr in
    177181              set_arg_8 s addr2 old_acc
     182        | XCHD addr1 addr2 ⇒
     183            let 〈acc_nu, acc_nl〉 ≝ split … four four (get_8051_sfr s SFR_ACC_A) in
     184            let 〈arg_nu, arg_nl〉 ≝ split … four four (get_arg_8 s false addr2) in
     185            let new_acc ≝ acc_nu @@ arg_nl in
     186            let new_arg ≝ arg_nu @@ acc_nl in
     187            let s ≝ set_8051_sfr s SFR_ACC_A new_acc in
     188              set_arg_8 s addr2 new_arg
     189        | Jump j ⇒
     190          match j with
     191            [ JC addr ⇒
     192              match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
     193                [ RELATIVE r ⇒ λrel: True.
     194                  if get_cy_flag s then
     195                    let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
     196                      set_program_counter s new_pc
     197                  else
     198                    s
     199                | _ ⇒ λother: False. ?
     200                ] (subaddressing_modein … addr)
     201            | JNC addr ⇒
     202              match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
     203                [ RELATIVE r ⇒ λrel: True.
     204                  if negation (get_cy_flag s) then
     205                    let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
     206                      set_program_counter s new_pc
     207                  else
     208                    s
     209                | _ ⇒ λother: False. ?
     210                ] (subaddressing_modein … addr)
     211            | JB addr1 addr2 ⇒
     212              match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
     213                [ RELATIVE r ⇒ λrel: True.
     214                  if get_arg_1 s addr1 false then
     215                    let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
     216                      set_program_counter s new_pc
     217                  else
     218                    s
     219                | _ ⇒ λother: False. ?
     220                ] (subaddressing_modein … addr2)
     221            | JNB addr1 addr2 ⇒
     222              match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
     223                [ RELATIVE r ⇒ λrel: True.
     224                  if negation (get_arg_1 s addr1 false) then
     225                    let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
     226                      set_program_counter s new_pc
     227                  else
     228                    s
     229                | _ ⇒ λother: False. ?
     230                ] (subaddressing_modein … addr2)
     231            | JBC addr1 addr2 ⇒
     232              match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
     233                [ RELATIVE r ⇒ λrel: True.
     234                  let s ≝ set_arg_1 s addr1 false in
     235                    if get_arg_1 s addr1 false then
     236                      let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
     237                        set_program_counter s new_pc
     238                    else
     239                      s
     240                | _ ⇒ λother: False. ?
     241                ] (subaddressing_modein … addr2)
     242            | JZ addr ⇒
     243              match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
     244                [ RELATIVE r ⇒ λrel: True.
     245                    if eq_bv ? (get_8051_sfr s SFR_ACC_A) (zero eight) then
     246                      let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
     247                        set_program_counter s new_pc
     248                    else
     249                      s
     250                | _ ⇒ λother: False. ?
     251                ] (subaddressing_modein … addr)
     252            | JNZ addr ⇒
     253              match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
     254                [ RELATIVE r ⇒ λrel: True.
     255                    if negation (eq_bv ? (get_8051_sfr s SFR_ACC_A) (zero eight)) then
     256                      let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
     257                        set_program_counter s new_pc
     258                    else
     259                      s
     260                | _ ⇒ λother: False. ?
     261                ] (subaddressing_modein … addr)
     262            | CJNE addr1 addr2 ⇒ ?
     263              match addr1 with
     264                [ Left l ⇒ ?
     265                | Right r ⇒ ?
     266                ]
     267            | DJNZ addr1 addr2 ⇒
     268              match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
     269                [ RELATIVE r ⇒ λrel: True.
     270                    let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 s true addr1) (bitvector_of_nat eight one) false in
     271                    let s ≝ set_arg_8 s addr1 result in
     272                      if negation (eq_bv ? result (zero eight)) then
     273                        let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
     274                          set_program_counter s new_pc
     275                      else
     276                        s
     277                | _ ⇒ λother: False. ?
     278                ] (subaddressing_modein … addr2)
     279            ]
    178280        | NOP ⇒ s
    179281        | _ ⇒ s
Note: See TracChangeset for help on using the changeset viewer.