Changeset 2167


Ignore:
Timestamp:
Jul 8, 2012, 4:24:10 PM (5 years ago)
Author:
sacerdot
Message:

Only one daemon left.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Test.ma

    r2166 r2167  
    486486qed.
    487487
     488lemma set_register_status_of_pseudo_status:
     489 ∀M,cm,s,sigma,policy,r,v,v'.
     490  map_internal_ram_address_using_pseudo_address_map M sigma
     491   (false:::bit_address_of_register pseudo_assembly_program cm s r) v =v' →
     492  set_register (BitVectorTrie Byte 16)
     493   (code_memory_of_pseudo_assembly_program cm sigma policy)
     494   (status_of_pseudo_status M cm s sigma policy) r v'
     495  = status_of_pseudo_status M cm (set_register pseudo_assembly_program cm s r v)
     496    sigma policy.
     497 #M #cm #s #sigma #policy #r #v #v' #v_ok
     498 whd in match set_register; normalize nodelta
     499 >bit_address_of_register_status_of_pseudo_status
     500 >(insert_low_internal_ram_status_of_pseudo_status … v_ok)
     501 @set_low_internal_ram_status_of_pseudo_status
     502qed.
     503
    488504definition map_address_mode_using_internal_pseudo_address_map_ok1 ≝
    489505 λM:internal_pseudo_address_map.λcm.λs:PreStatus ? cm.λaddr.
     
    510526     let register ≝ get_register ?? s [[ false; false; i ]] in
    511527     map_internal_ram_address_using_pseudo_address_map M sigma register v
     528  | REGISTER r ⇒
     529     map_internal_ram_address_using_pseudo_address_map M sigma
     530      (false:::bit_address_of_register … s r) v
    512531  | ACC_A ⇒
    513532     map_address_using_internal_pseudo_address_map M sigma SFR_ACC_A v
     
    664683      >EQ1 normalize nodelta
    665684      >external_ram_status_of_pseudo_status @set_external_ram_status_of_pseudo_status
    666   |6: #_ #EQ <EQ cases daemon (*CSC*)
     685  |6: #EQ1 #EQ2 <EQ2 /2 by set_register_status_of_pseudo_status/
    667686  |7: #EQ1 #EQ2 <EQ2 /2 by set_8051_sfr_status_of_pseudo_status/
    668687  |8: #_ #EQ <EQ @set_8051_sfr_status_of_pseudo_status %
Note: See TracChangeset for help on using the changeset viewer.