Ignore:
Timestamp:
Nov 25, 2010, 11:18:27 AM (10 years ago)
Author:
mulligan
Message:

Added bit address lookup for registers.

File:
1 edited

Legend:

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

    r285 r286  
    567567      ncases not_implemented.
    568568nqed.
     569
     570ndefinition bit_address_of_register ≝
     571  λs: Status.
     572  λb, c, d: Bit.
     573    let 〈 un, ln 〉 ≝ split ? four four (get_8051_sfr s SFR_PSW) in
     574    let 〈 r1, r0 〉 ≝ mk_Cartesian … (get_index four un two ?) (get_index four un three ?) in
     575    let offset ≝
     576      if conjunction (negation r1) (negation r0) then
     577        Z
     578      else if conjunction (negation r1) r0 then
     579        eight
     580      else if conjunction r1 r0 then
     581        twenty_four
     582      else
     583        sixteen
     584    in
     585      bitvector_of_nat seven (offset + (nat_of_bitvector ? [[ false ; b ; c ; d ]])).
     586    nnormalize.
     587    nrepeat (napply less_than_or_equal_monotone).
     588    napply less_than_or_equal_zero.
     589    nrepeat (napply less_than_or_equal_monotone).
     590    napply less_than_or_equal_zero.
     591nqed.
Note: See TracChangeset for help on using the changeset viewer.