Changeset 285


Ignore:
Timestamp:
Nov 25, 2010, 10:53:04 AM (9 years ago)
Author:
mulligan
Message:

Get and set for bitaddressable SFRs now completed.

File:
1 edited

Legend:

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

    r281 r285  
    108108  ∀i: SFR8052.
    109109    sfr_8052_index i < five.
     110   
     111ndefinition set_p1_latch ≝
     112  λs: Status.
     113  λb: Byte.
     114    let old_code_memory ≝ code_memory s in
     115    let old_low_internal_ram ≝ low_internal_ram s in
     116    let old_high_internal_ram ≝ high_internal_ram s in
     117    let old_external_ram ≝ external_ram s in
     118    let old_program_counter ≝ program_counter s in
     119    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
     120    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
     121    let old_p3_latch ≝ p3_latch s in
     122      mk_Status old_code_memory
     123                old_low_internal_ram
     124                old_high_internal_ram
     125                old_external_ram
     126                old_program_counter
     127                old_special_function_registers_8051
     128                old_special_function_registers_8052
     129                b
     130                old_p3_latch.
     131
     132ndefinition set_p3_latch ≝
     133  λs: Status.
     134  λb: Byte.
     135    let old_code_memory ≝ code_memory s in
     136    let old_low_internal_ram ≝ low_internal_ram s in
     137    let old_high_internal_ram ≝ high_internal_ram s in
     138    let old_external_ram ≝ external_ram s in
     139    let old_program_counter ≝ program_counter s in
     140    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
     141    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
     142    let old_p1_latch ≝ p1_latch s in
     143      mk_Status old_code_memory
     144                old_low_internal_ram
     145                old_high_internal_ram
     146                old_external_ram
     147                old_program_counter
     148                old_special_function_registers_8051
     149                old_special_function_registers_8052
     150                old_p1_latch
     151                b.
    110152
    111153ndefinition get_8051_sfr ≝
     
    141183    let new_special_function_registers_8051 ≝
    142184      cic:/matita/ng/Vector/set_index.fix(0,3,2) Byte nineteen old_special_function_registers_8051 index b ? in
     185    let old_p1_latch ≝ p1_latch s in
     186    let old_p3_latch ≝ p3_latch s in
    143187      mk_Status old_code_memory
    144188                old_low_internal_ram
     
    147191                old_program_counter
    148192                new_special_function_registers_8051
    149                 old_special_function_registers_8052.
     193                old_special_function_registers_8052
     194                old_p1_latch
     195                old_p3_latch.
    150196    napply (sfr8051_index_nineteen i).
    151197nqed.
     
    165211    let new_special_function_registers_8052 ≝
    166212      cic:/matita/ng/Vector/set_index.fix(0,3,2) Byte five old_special_function_registers_8052 index b ? in
    167       mk_Status old_code_memory
    168                 old_low_internal_ram
    169                 old_high_internal_ram
    170                 old_external_ram
    171                 old_program_counter
    172                 old_special_function_registers_8051
    173                 new_special_function_registers_8052.
     213    let old_p1_latch ≝ p1_latch s in
     214    let old_p3_latch ≝ p3_latch s in
     215      mk_Status old_code_memory
     216                old_low_internal_ram
     217                old_high_internal_ram
     218                old_external_ram
     219                old_program_counter
     220                old_special_function_registers_8051
     221                new_special_function_registers_8052
     222                old_p1_latch
     223                old_p3_latch.
    174224    napply (sfr8052_index_five i).
    175225nqed.
     
    184234    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
    185235    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
     236    let old_p1_latch ≝ p1_latch s in
     237    let old_p3_latch ≝ p3_latch s in
    186238      mk_Status old_code_memory
    187239                old_low_internal_ram
     
    190242                w
    191243                old_special_function_registers_8051
    192                 old_special_function_registers_8052.
     244                old_special_function_registers_8052
     245                old_p1_latch
     246                old_p3_latch.
    193247               
    194248ndefinition set_code_memory ≝
     
    203257    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
    204258    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
     259    let old_p1_latch ≝ p1_latch s in
     260    let old_p3_latch ≝ p3_latch s in
    205261      mk_Status r
    206262                old_low_internal_ram
     
    209265                old_program_counter
    210266                old_special_function_registers_8051
    211                 old_special_function_registers_8052.
     267                old_special_function_registers_8052
     268                old_p1_latch
     269                old_p3_latch.
    212270               
    213271ndefinition set_low_internal_ram ≝
     
    222280    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
    223281    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
     282    let old_p1_latch ≝ p1_latch s in
     283    let old_p3_latch ≝ p3_latch s in
    224284      mk_Status old_code_memory
    225285                r
     
    228288                old_program_counter
    229289                old_special_function_registers_8051
    230                 old_special_function_registers_8052.
     290                old_special_function_registers_8052
     291                old_p1_latch
     292                old_p3_latch.
     293               
     294ndefinition set_high_internal_ram ≝
     295  λs: Status.
     296  λi: SFR8052.
     297  λr: BitVectorTrie Byte seven.
     298    let index ≝ sfr_8052_index i in
     299    let old_code_memory ≝ code_memory s in
     300    let old_low_internal_ram ≝ low_internal_ram s in
     301    let old_high_internal_ram ≝ high_internal_ram s in
     302    let old_external_ram ≝ external_ram s in
     303    let old_program_counter ≝ program_counter s in
     304    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
     305    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
     306    let old_p1_latch ≝ p1_latch s in
     307    let old_p3_latch ≝ p3_latch s in
     308      mk_Status old_code_memory
     309                old_low_internal_ram
     310                r
     311                old_external_ram
     312                old_program_counter
     313                old_special_function_registers_8051
     314                old_special_function_registers_8052
     315                old_p1_latch
     316                old_p3_latch.
    231317               
    232318naxiom less_than_or_equal_monotone:
     
    331417    napply (less_than_or_equal_zero).
    332418nqed.
    333                
    334 ndefinition set_high_internal_ram ≝
    335   λs: Status.
    336   λi: SFR8052.
    337   λr: BitVectorTrie Byte seven.
    338     let index ≝ sfr_8052_index i in
    339     let old_code_memory ≝ code_memory s in
    340     let old_low_internal_ram ≝ low_internal_ram s in
    341     let old_high_internal_ram ≝ high_internal_ram s in
    342     let old_external_ram ≝ external_ram s in
    343     let old_program_counter ≝ program_counter s in
    344     let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
    345     let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
    346       mk_Status old_code_memory
    347                 old_low_internal_ram
    348                 r
    349                 old_external_ram
    350                 old_program_counter
    351                 old_special_function_registers_8051
    352                 old_special_function_registers_8052.
    353419
    354420ndefinition initialise_status ≝
    355   let status ≝ mk_Status (Stub Byte sixteen)
    356                          (Stub Byte seven)
    357                          (Stub Byte seven)
    358                          (Stub Byte sixteen)
    359                          (zero sixteen)
    360                          (replicate Byte nineteen (zero eight))
    361                          (replicate Byte five (zero eight))
    362                          (zero eight)
    363                          (zero eight) in
     421  let status ≝ mk_Status (Stub Byte sixteen)                    (* Code mem. *)
     422                         (Stub Byte seven)                      (* Low mem.  *)
     423                         (Stub Byte seven)                      (* High mem. *)
     424                         (Stub Byte sixteen)                    (* Ext mem.  *)
     425                         (zero sixteen)                         (* PC.       *)
     426                         (replicate Byte nineteen (zero eight)) (* 8051 SFR. *)
     427                         (replicate Byte five (zero eight))     (* 8052 SFR. *)
     428                         (zero eight)                           (* P1 latch. *)
     429                         (zero eight) in                        (* P3 latch. *)
    364430  set_program_counter status (bitvector_of_nat sixteen seven).
    365431 
     
    436502      ncases not_implemented.
    437503nqed.
     504
     505ndefinition set_bit_addressable_sfr ≝
     506  λs: Status.
     507  λb: Byte.
     508    let address ≝ nat_of_bitvector … b in
     509      if (decidable_equality address one_hundred_and_twenty_eight) then
     510        ?
     511      else if (decidable_equality address one_hundred_and_forty_four) then
     512        let status_1 ≝ set_8051_sfr s SFR_P1 b in
     513        let status_2 ≝ set_p1_latch s b in
     514          status_2
     515      else if (decidable_equality address one_hundred_and_sixty) then
     516        ?
     517      else if (decidable_equality address one_hundred_and_seventy_six) then
     518        let status_1 ≝ set_8051_sfr s SFR_P3 b in
     519        let status_2 ≝ set_p3_latch s b in
     520          status_2
     521      else if (decidable_equality address one_hundred_and_fifty_three) then
     522        set_8051_sfr s SFR_SBUF b
     523      else if (decidable_equality address one_hundred_and_thirty_eight) then
     524        set_8051_sfr s SFR_TL0 b
     525      else if (decidable_equality address one_hundred_and_thirty_nine) then
     526        set_8051_sfr s SFR_TL1 b
     527      else if (decidable_equality address one_hundred_and_forty) then
     528        set_8051_sfr s SFR_TH0 b
     529      else if (decidable_equality address one_hundred_and_forty_one) then
     530        set_8051_sfr s SFR_TH1 b
     531      else if (decidable_equality address two_hundred) then
     532        set_8052_sfr s SFR_T2CON b
     533      else if (decidable_equality address two_hundred_and_two) then
     534        set_8052_sfr s SFR_RCAP2L b
     535      else if (decidable_equality address two_hundred_and_three) then
     536        set_8052_sfr s SFR_RCAP2H b
     537      else if (decidable_equality address two_hundred_and_four) then
     538        set_8052_sfr s SFR_TL2 b
     539      else if (decidable_equality address two_hundred_and_five) then
     540        set_8052_sfr s SFR_TH2 b
     541      else if (decidable_equality address one_hundred_and_thirty_five) then
     542        set_8051_sfr s SFR_PCON b
     543      else if (decidable_equality address one_hundred_and_thirty_six) then
     544        set_8051_sfr s SFR_TCON b
     545      else if (decidable_equality address one_hundred_and_thirty_seven) then
     546        set_8051_sfr s SFR_TMOD b
     547      else if (decidable_equality address one_hundred_and_fifty_two) then
     548        set_8051_sfr s SFR_SCON b
     549      else if (decidable_equality address one_hundred_and_sixty_eight) then
     550        set_8051_sfr s SFR_IE b
     551      else if (decidable_equality address one_hundred_and_eighty_four) then
     552        set_8051_sfr s SFR_IP b
     553      else if (decidable_equality address one_hundred_and_twenty_nine) then
     554        set_8051_sfr s SFR_SP b
     555      else if (decidable_equality address one_hundred_and_thirty) then
     556        set_8051_sfr s SFR_DPL b
     557      else if (decidable_equality address one_hundred_and_thirty_one) then
     558        set_8051_sfr s SFR_DPH b
     559      else if (decidable_equality address two_hundred_and_eight) then
     560        set_8051_sfr s SFR_PSW b
     561      else if (decidable_equality address two_hundred_and_twenty_four) then
     562        set_8051_sfr s SFR_ACC_A b
     563      else if (decidable_equality address two_hundred_and_forty) then
     564        set_8051_sfr s SFR_ACC_B b
     565      else
     566        ?.
     567      ncases not_implemented.
     568nqed.
Note: See TracChangeset for help on using the changeset viewer.