Ignore:
Timestamp:
Jul 24, 2012, 6:00:48 PM (8 years ago)
Author:
mulligan
Message:

Work on the MOV instruction from today and bug fixes in set_arg_1.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r2209 r2247  
    464464
    465465definition addressing_mode_ok ≝
    466  λT.λM:internal_pseudo_address_map.λcm.λs:PreStatus T cm.
    467   λaddr:addressing_mode.
    468    match addr with
     466  λT.
     467  λM: internal_pseudo_address_map.
     468  λcm.
     469  λs: PreStatus T cm.
     470  λaddr: addressing_mode.
     471  match addr with
    469472    [ DIRECT d ⇒
    470473        if eq_bv … d (bitvector_of_nat … 224) then
     
    481484        let address ≝ bit_address_of_register … s r in
    482485          ¬assoc_list_exists … (false:::address) (eq_bv 8) (\fst M)
    483     | ACC_A ⇒ match \snd M with [ data ⇒ true | _ ⇒ false ]
     486    | ACC_A ⇒
     487      match \snd M with
     488      [ data ⇒ true
     489      | _ ⇒ false
     490      ]
    484491    | ACC_B ⇒ true
    485492    | DPTR ⇒ true
     
    491498    | INDIRECT_DPTR ⇒ true
    492499    | CARRY ⇒ true
    493     | BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *)
    494     | N_BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *)
     500    | BIT_ADDR b ⇒
     501      let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 b in
     502        if head' bool 0 bit_one then
     503          eq_accumulator_address_map_entry (\snd M) data
     504        else
     505          let address ≝ nat_of_bitvector 7 seven_bits in 
     506          let address' ≝ bitvector_of_nat 7 ((address÷8)+32) in
     507            ¬assoc_list_exists ?? (false:::address') (eq_bv 8) (\fst M)
     508    | N_BIT_ADDR b ⇒ ¬true (* TO BE COMPLETED *)
    495509    | RELATIVE _ ⇒ true
    496510    | ADDR11 _ ⇒ true
     
    650664      | RET ⇒
    651665        let 〈callM, accM〉 ≝ M in
    652         let sp_plus_1 ≝ assoc_list_exists ?? (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) (eq_bv 8) callM in
    653         let sp_plus_2 ≝ assoc_list_exists ?? (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)) (eq_bv 8) callM in
     666        let sp_plus_1 ≝ assoc_list_exists ?? (subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) (eq_bv 8) callM in
     667        let sp_plus_2 ≝ assoc_list_exists ?? (subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)) (eq_bv 8) callM in
    654668          if sp_plus_1 ∧ sp_plus_2 then
    655669            Some … M
     
    658672      | RETI ⇒
    659673        let 〈callM, accM〉 ≝ M in
    660         let sp_plus_1 ≝ assoc_list_exists ?? (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) (eq_bv 8) callM in
    661         let sp_plus_2 ≝ assoc_list_exists ?? (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)) (eq_bv 8) callM in
     674        let sp_plus_1 ≝ assoc_list_exists ?? (subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) (eq_bv 8) callM in
     675        let sp_plus_2 ≝ assoc_list_exists ?? (subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)) (eq_bv 8) callM in
    662676          if sp_plus_1 ∧ sp_plus_2 then
    663677            Some … M
     
    745759            None ?
    746760        ]
    747       | MOV addr1 ⇒ Some … M
     761      | MOV addr1 ⇒
     762        match addr1 with
     763        [ inl l ⇒
     764          match l with
     765          [ inl l' ⇒
     766            match l' with
     767            [ inl l'' ⇒
     768              match l'' with
     769              [ inl l''' ⇒
     770                match l''' with
     771                [ inl l'''' ⇒
     772                  let 〈acc_a, others〉 ≝ l'''' in
     773                  if addressing_mode_ok T M … s acc_a ∧ addressing_mode_ok T M … s others then
     774                    Some ? M
     775                  else
     776                    None ?
     777                | inr r ⇒
     778                  let 〈others, others'〉 ≝ r in
     779                  if addressing_mode_ok T M … s others ∧ addressing_mode_ok T M … s others' then
     780                    Some ? M
     781                  else
     782                    None ?
     783                ]
     784              | inr r ⇒
     785                let 〈direct, others〉 ≝ r in
     786                if addressing_mode_ok T M … s direct ∧ addressing_mode_ok T M … s others then
     787                  Some ? M
     788                else
     789                  None ?
     790              ]
     791            | inr r ⇒
     792              let 〈dptr, data_16〉 ≝ r in
     793              if addressing_mode_ok T M … s dptr ∧ addressing_mode_ok T M … s data_16 then
     794                Some ? M
     795              else
     796                None ?
     797            ]
     798          | inr r ⇒
     799            let 〈carry, bit_addr〉 ≝ r in
     800            if addressing_mode_ok T M … s carry ∧ addressing_mode_ok T M … s bit_addr then
     801              Some ? M
     802            else
     803              None ?
     804          ]
     805        | inr r ⇒
     806          let 〈bit_addr, carry〉 ≝ r in
     807          if addressing_mode_ok T M … s bit_addr ∧ addressing_mode_ok T M … s carry then
     808            Some ? M
     809          else
     810            None ?
     811        ]
    748812      ]
    749813    ].
Note: See TracChangeset for help on using the changeset viewer.