Ignore:
Timestamp:
Mar 18, 2011, 11:22:49 AM (10 years ago)
Author:
mulligan
Message:

Most of LIN completed.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.2-4.3/ASM/I8051.ma

    r683 r686  
    11include "arithmetics/nat.ma".
     2include "basics/jmeq.ma".
    23
    34include "cerco/String.ma".
     
    132133definition RegisterSPH ≝ Register07.
    133134
    134 definition register_address: Register → addressing_mode
     135definition register_address: Register → [[ acc_a; direct; register ]]
    135136  λr: Register.
    136137    match r with
     
    144145    | Register07 ⇒ REGISTER [[ true; true; true ]]
    145146    | RegisterA ⇒ ACC_A
    146     | RegisterB ⇒ ACC_B
     147    | RegisterB ⇒ DIRECT (bitvector_of_nat 8 240)
    147148    | RegisterDPL ⇒ DIRECT (bitvector_of_nat 8 82)
    148149    | RegisterDPH ⇒ DIRECT (bitvector_of_nat 8 83)
    149     | _ ⇒ DIRECT (bitvector_of_nat 8 (nat_of_register r))
     150    | _ ⇒ DIRECT (bitvector_of_nat 8 (nat_of_register r)) 
    150151    ].
     152    [*: normalize
     153        @ I
     154    ]
     155qed.
    151156   
    152157definition registers: list Register ≝
Note: See TracChangeset for help on using the changeset viewer.