Ignore:
Timestamp:
Oct 19, 2011, 4:43:49 PM (8 years ago)
Author:
sacerdot
Message:

Maps from hardware registers to beval now implemented in ASM/I8051 (in place
of the old huge implementation to Bytes).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/SemanticUtils.ma

    r1415 r1416  
    1212
    1313(*** Store/retrieve on hardware registers ***)
    14 
    15 axiom hw_register_env: Type[0]. (* CSC: use the one in I8051? *)
    16 axiom empty_hw_register_env: hw_register_env.
    17 axiom hwreg_retrieve : hw_register_env → Register → beval.
    18 axiom hwreg_store : Register → beval → hw_register_env → hw_register_env.
    1914
    2015definition init_hw_register_env: address → hw_register_env ≝
Note: See TracChangeset for help on using the changeset viewer.