Ignore:
Timestamp:
Aug 30, 2011, 6:55:12 PM (9 years ago)
Author:
campbell
Message:

Merge trunk into branch.

Location:
Deliverables/D3.3/id-lookup-branch
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch

  • Deliverables/D3.3/id-lookup-branch/ASM

  • Deliverables/D3.3/id-lookup-branch/ASM/I8051.ma

    r1098 r1153  
    147147definition RegisterSPL ≝ Register06.
    148148definition RegisterSPH ≝ Register07.
     149definition RegisterForbidden: list Register ≝
     150  [ RegisterSST; RegisterST0; RegisterST1;
     151    RegisterSPL; RegisterSPH ].
     152definition RegisterParams: list Register ≝
     153  [ Register30; Register31; Register32; Register33;
     154    Register34; Register35; Register36; Register37 ].
    149155definition Registers ≝
    150156  [Register00; Register01; Register02; Register03; Register04;
     
    167173  [Register20; Register21; Register22; Register23; Register24;
    168174   Register25; Register26; Register27].
    169 definition RegisterParameters ≝
    170   [Register30; Register31; Register32; Register33; Register34; Register35;
    171    Register36; Register37].
    172175
    173176definition register_address: Register → [[ acc_a; direct; registr ]] ≝
     
    192195    ]
    193196qed.
    194    
    195 definition registers: list Register ≝
    196   [ Register00; Register01; Register02; Register03;
    197     Register04; Register05; Register06; Register07;
    198     RegisterA; RegisterB; RegisterDPL; RegisterDPH;
    199     Register10; Register11; Register12; Register13;
    200     Register14; Register15; Register16; Register17;
    201     Register20; Register21; Register22; Register23;
    202     Register24; Register25; Register26; Register27;
    203     Register30; Register31; Register32; Register33;
    204     Register34; Register35; Register36; Register37;
    205     RegisterSST; RegisterST0; RegisterST1;
    206     RegisterSPL; RegisterSPH ].
    207    
    208 definition forbidden_registers: list Register ≝
    209   [ RegisterSST; RegisterST0; RegisterST1;
    210     RegisterSPL; RegisterSPH ].
    211    
    212 definition parameters: list Register ≝
    213   [ Register30; Register31; Register32; Register33;
    214     Register34; Register35; Register36; Register37 ].
    215197   
    216198record RegisterMap: Type[0] ≝
     
    32423224record Eval: Type[0] ≝
    32433225{
    3244   opaccs: OpAccs → Byte → Byte → option Byte;
     3226  opaccs: OpAccs → Byte → Byte → Byte × Byte;
    32453227  op1: Op1 → Byte → Byte;
    32463228  op2: Bit → Op2 → Byte → Byte → (Byte × Bit)
    32473229}.
    32483230
    3249 axiom opaccs_implementation: OpAccs → Byte → Byte → option Byte.
     3231axiom opaccs_implementation: OpAccs → Byte → Byte → Byte × Byte.
    32503232axiom op1_implementation: Op1 → Byte → Byte.
    32513233axiom op2_implementation: Bit → Op2 → Byte → Byte → (Byte × Bit).
Note: See TracChangeset for help on using the changeset viewer.