Changeset 935 for src/ASM/Status.ma


Ignore:
Timestamp:
Jun 10, 2011, 1:15:11 PM (9 years ago)
Author:
mulligan
Message:

changes to status and assembly proof

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Status.ma

    r911 r935  
    498498  λac: option Bit.
    499499  λov: Bit.
    500     let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr ? s SFR_PSW) in
    501     let old_cy ≝ get_index_v… nu O ? in
    502     let old_ac ≝ get_index_v… nu 1 ? in
    503     let old_fo ≝ get_index_v… nu 2 ? in
    504     let old_rs1 ≝ get_index_v… nu 3 ? in
    505     let old_rs0 ≝ get_index_v… nl O ? in
    506     let old_ov ≝ get_index_v… nl 1 ? in
    507     let old_ud ≝ get_index_v… nl 2 ? in
    508     let old_p ≝ get_index_v… nl 3 ? in
     500    let old_cy ≝ get_index_v… (get_8051_sfr ? s SFR_PSW) O ? in
     501    let old_ac ≝ get_index_v… (get_8051_sfr ? s SFR_PSW) 1 ? in
     502    let old_fo ≝ get_index_v… (get_8051_sfr ? s SFR_PSW) 2 ? in
     503    let old_rs1 ≝ get_index_v… (get_8051_sfr ? s SFR_PSW) 3 ? in
     504    let old_rs0 ≝ get_index_v… (get_8051_sfr ? s SFR_PSW) 4 ? in
     505    let old_ov ≝ get_index_v… (get_8051_sfr ? s SFR_PSW) 5 ? in
     506    let old_ud ≝ get_index_v… (get_8051_sfr ? s SFR_PSW) 6 ? in
     507    let old_p ≝ get_index_v… (get_8051_sfr ? s SFR_PSW) 7 ? in
    509508    let new_ac ≝ match ac with [ None ⇒ old_ac | Some j ⇒ j ] in
    510509    let new_psw ≝ [[ old_cy ; new_ac ; old_fo ; old_rs1 ;
Note: See TracChangeset for help on using the changeset viewer.