source: Deliverables/D4.1/Matita/Status.ma @ 289

Last change on this file since 289 was 289, checked in by mulligan, 9 years ago

Writing at stack pointer implemented.

File size: 24.3 KB
RevLine 
[257]1(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
2(* Interpret.ma: Operational semantics for the 8051/8052 processor.           *)
3(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
4
5(* include "ASM.ma". *)
[259]6include "Arithmetic.ma".
[257]7include "BitVectorTrie.ma".
8
[276]9ndefinition Time ≝ Nat.
10
11ninductive SerialBufferType: Type[0] ≝
12  Eight: Byte → SerialBufferType
13| Nine: Bit → Byte → SerialBufferType.
14
15ninductive LineType: Type[0] ≝
16  P1: Byte → LineType
17| P3: Byte → LineType
18| SerialBuffer: SerialBufferType → LineType.
19
20(* What is a continuation, now? *)
21
[257]22ninductive SFR8051: Type[0] ≝
23  SFR_SP: SFR8051
24| SFR_DPL: SFR8051
25| SFR_DPH: SFR8051
26| SFR_PCON: SFR8051
27| SFR_TCON: SFR8051
28| SFR_TMOD: SFR8051
29| SFR_TL0: SFR8051
30| SFR_TL1: SFR8051
31| SFR_TH0: SFR8051
32| SFR_TH1: SFR8051
33| SFR_P1: SFR8051
34| SFR_SCON: SFR8051
35| SFR_SBUF: SFR8051
36| SFR_IE: SFR8051
37| SFR_P3: SFR8051
38| SFR_IP: SFR8051
39| SFR_PSW: SFR8051
40| SFR_ACC_A: SFR8051
41| SFR_ACC_B: SFR8051.
42
43ndefinition sfr_8051_index ≝
44  λs: SFR8051.
45    match s with
46      [ SFR_SP ⇒ Z
47      | SFR_DPL ⇒ S Z
48      | SFR_DPH ⇒ two
49      | SFR_PCON ⇒ three
50      | SFR_TCON ⇒ four
51      | SFR_TMOD ⇒ five
52      | SFR_TL0 ⇒ six
53      | SFR_TL1 ⇒ seven
54      | SFR_TH0 ⇒ eight
55      | SFR_TH1 ⇒ nine
56      | SFR_P1 ⇒ ten
57      | SFR_SCON ⇒ eleven
58      | SFR_SBUF ⇒ twelve
59      | SFR_IE ⇒ thirteen
60      | SFR_P3 ⇒ fourteen
61      | SFR_IP ⇒ fifteen
62      | SFR_PSW ⇒ sixteen
63      | SFR_ACC_A ⇒ seventeen
64      | SFR_ACC_B ⇒ eighteen
65      ].
66     
67ninductive SFR8052: Type[0] ≝
68   SFR_T2CON: SFR8052
69|  SFR_RCAP2L: SFR8052
70|  SFR_RCAP2H: SFR8052
71|  SFR_TL2: SFR8052
72|  SFR_TH2: SFR8052.
73
74ndefinition sfr_8052_index ≝
75  λs: SFR8052.
76    match s with
77      [ SFR_T2CON ⇒ Z
78      | SFR_RCAP2L ⇒ S Z
79      | SFR_RCAP2H ⇒ two
80      | SFR_TL2 ⇒ three
81      | SFR_TH2 ⇒ four
82      ].
83
84(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
85(* Processor status.                                                          *)
86(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
87nrecord Status: Type[0] ≝
88{
89  code_memory: BitVectorTrie Byte sixteen;
90  low_internal_ram: BitVectorTrie Byte seven;
91  high_internal_ram: BitVectorTrie Byte seven;
92  external_ram: BitVectorTrie Byte sixteen;
93 
94  program_counter: Word;
95 
96  special_function_registers_8051: Vector Byte nineteen;
[281]97  special_function_registers_8052: Vector Byte five;
98 
99  p1_latch: Byte;
100  p3_latch: Byte
[257]101}.
102
[265]103naxiom sfr8051_index_nineteen:
104  ∀i: SFR8051.
105    sfr_8051_index i < nineteen.
106   
107naxiom sfr8052_index_five:
108  ∀i: SFR8052.
109    sfr_8052_index i < five.
[285]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.
[265]131
[285]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.
152
[265]153ndefinition get_8051_sfr ≝
154  λs: Status.
155  λi: SFR8051.
156    let sfr ≝ special_function_registers_8051 s in
157    let index ≝ sfr_8051_index i in
158      get_index … sfr index ?.
159    napply (sfr8051_index_nineteen i).
160nqed.
161
162ndefinition get_8052_sfr ≝
163  λs: Status.
164  λi: SFR8052.
165    let sfr ≝ special_function_registers_8052 s in
166    let index ≝ sfr_8052_index i in
167      get_index … sfr index ?.
168    napply (sfr8052_index_five i).
169nqed.
170
[259]171ndefinition set_8051_sfr ≝
172  λs: Status.
173  λi: SFR8051.
174  λb: Byte.
[265]175    let index ≝ sfr_8051_index i in
176    let old_code_memory ≝ code_memory s in
177    let old_low_internal_ram ≝ low_internal_ram s in
178    let old_high_internal_ram ≝ high_internal_ram s in
179    let old_external_ram ≝ external_ram s in
180    let old_program_counter ≝ program_counter s in
181    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
182    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
183    let new_special_function_registers_8051 ≝
184      cic:/matita/ng/Vector/set_index.fix(0,3,2) Byte nineteen old_special_function_registers_8051 index b ? in
[285]185    let old_p1_latch ≝ p1_latch s in
186    let old_p3_latch ≝ p3_latch s in
[265]187      mk_Status old_code_memory
188                old_low_internal_ram
189                old_high_internal_ram
190                old_external_ram
191                old_program_counter
192                new_special_function_registers_8051
[285]193                old_special_function_registers_8052
194                old_p1_latch
195                old_p3_latch.
[265]196    napply (sfr8051_index_nineteen i).
197nqed.
[258]198
[265]199ndefinition set_8052_sfr ≝
200  λs: Status.
201  λi: SFR8052.
202  λb: Byte.
203    let index ≝ sfr_8052_index i in
204    let old_code_memory ≝ code_memory s in
205    let old_low_internal_ram ≝ low_internal_ram s in
206    let old_high_internal_ram ≝ high_internal_ram s in
207    let old_external_ram ≝ external_ram s in
208    let old_program_counter ≝ program_counter s in
209    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
210    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
211    let new_special_function_registers_8052 ≝
212      cic:/matita/ng/Vector/set_index.fix(0,3,2) Byte five old_special_function_registers_8052 index b ? in
[285]213    let old_p1_latch ≝ p1_latch s in
214    let old_p3_latch ≝ p3_latch s in
[265]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
[285]221                new_special_function_registers_8052
222                old_p1_latch
223                old_p3_latch.
[265]224    napply (sfr8052_index_five i).
225nqed.
226
227ndefinition set_program_counter ≝
228  λs: Status.
229  λw: Word.
230    let old_code_memory ≝ code_memory s in
231    let old_low_internal_ram ≝ low_internal_ram s in
232    let old_high_internal_ram ≝ high_internal_ram s in
233    let old_external_ram ≝ external_ram s in
234    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
235    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
[285]236    let old_p1_latch ≝ p1_latch s in
237    let old_p3_latch ≝ p3_latch s in
[265]238      mk_Status old_code_memory
239                old_low_internal_ram
240                old_high_internal_ram
241                old_external_ram
242                w
243                old_special_function_registers_8051
[285]244                old_special_function_registers_8052
245                old_p1_latch
246                old_p3_latch.
[265]247               
248ndefinition set_code_memory ≝
249  λs: Status.
250  λr: BitVectorTrie Byte sixteen.
251    let old_low_internal_ram ≝ low_internal_ram s in
252    let old_high_internal_ram ≝ high_internal_ram s in
253    let old_external_ram ≝ external_ram s in
254    let old_program_counter ≝ program_counter s in
255    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
256    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
[285]257    let old_p1_latch ≝ p1_latch s in
258    let old_p3_latch ≝ p3_latch s in
[265]259      mk_Status r
260                old_low_internal_ram
261                old_high_internal_ram
262                old_external_ram
263                old_program_counter
264                old_special_function_registers_8051
[285]265                old_special_function_registers_8052
266                old_p1_latch
267                old_p3_latch.
[265]268               
269ndefinition set_low_internal_ram ≝
270  λs: Status.
271  λr: BitVectorTrie Byte seven.
272    let old_code_memory ≝ code_memory s in
273    let old_high_internal_ram ≝ high_internal_ram s in
274    let old_external_ram ≝ external_ram s in
275    let old_program_counter ≝ program_counter s in
276    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
277    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
[285]278    let old_p1_latch ≝ p1_latch s in
279    let old_p3_latch ≝ p3_latch s in
[265]280      mk_Status old_code_memory
281                r
282                old_high_internal_ram
283                old_external_ram
284                old_program_counter
285                old_special_function_registers_8051
[285]286                old_special_function_registers_8052
287                old_p1_latch
288                old_p3_latch.
[265]289               
[285]290ndefinition set_high_internal_ram ≝
291  λs: Status.
292  λr: BitVectorTrie Byte seven.
293    let old_code_memory ≝ code_memory s in
294    let old_low_internal_ram ≝ low_internal_ram s in
295    let old_high_internal_ram ≝ high_internal_ram s in
296    let old_external_ram ≝ external_ram s in
297    let old_program_counter ≝ program_counter s in
298    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
299    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
300    let old_p1_latch ≝ p1_latch s in
301    let old_p3_latch ≝ p3_latch s in
302      mk_Status old_code_memory
303                old_low_internal_ram
304                r
305                old_external_ram
306                old_program_counter
307                old_special_function_registers_8051
308                old_special_function_registers_8052
309                old_p1_latch
310                old_p3_latch.
311               
[267]312naxiom less_than_or_equal_monotone:
313  ∀m, n: Nat.
314    m ≤ n → S m ≤ S n.
315   
316alias id "get_index" = "cic:/matita/ng/Vector/get_index.fix(0,3,2)".
317               
[265]318ndefinition get_cy_flag ≝
319  λs: Status.
320    let sfr ≝ special_function_registers_8051 s in
[267]321    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
322      get_index Bool eight psw Z ?.
323    nnormalize.
324    napply (less_than_or_equal_monotone ? ?).
325    napply (less_than_or_equal_zero).
326    nrepeat (napply (less_than_or_equal_monotone ? ?)).
327    napply (less_than_or_equal_zero).
328nqed.
329
330ndefinition get_ac_flag ≝
331  λs: Status.
332    let sfr ≝ special_function_registers_8051 s in
333    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
334      get_index Bool eight psw (S Z) ?.
335    nnormalize.
336    nrepeat (napply (less_than_or_equal_monotone ? ?)).
337    napply (less_than_or_equal_zero).
338    nrepeat (napply (less_than_or_equal_monotone ? ?)).
339    napply (less_than_or_equal_zero).
340nqed.
341
342ndefinition get_fo_flag ≝
343  λs: Status.
344    let sfr ≝ special_function_registers_8051 s in
345    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
346      get_index Bool eight psw two ?.
347    nnormalize.
348    nrepeat (napply (less_than_or_equal_monotone ? ?)).
349    napply (less_than_or_equal_zero).
350    nrepeat (napply (less_than_or_equal_monotone ? ?)).
351    napply (less_than_or_equal_zero).
352nqed.
353
354ndefinition get_rs1_flag ≝
355  λs: Status.
356    let sfr ≝ special_function_registers_8051 s in
357    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
358      get_index Bool eight psw three ?.
359    nnormalize.
360    nrepeat (napply (less_than_or_equal_monotone ? ?)).
361    napply (less_than_or_equal_zero).
362    nrepeat (napply (less_than_or_equal_monotone ? ?)).
363    napply (less_than_or_equal_zero).
364nqed.
365
366ndefinition get_rs0_flag ≝
367  λs: Status.
368    let sfr ≝ special_function_registers_8051 s in
369    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
370      get_index Bool eight psw four ?.
371    nnormalize.
372    nrepeat (napply (less_than_or_equal_monotone ? ?)).
373    napply (less_than_or_equal_zero).
374    nrepeat (napply (less_than_or_equal_monotone ? ?)).
375    napply (less_than_or_equal_zero).
376nqed.
377
378ndefinition get_ov_flag ≝
379  λs: Status.
380    let sfr ≝ special_function_registers_8051 s in
381    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
382      get_index Bool eight psw five ?.
383    nnormalize.
384    nrepeat (napply (less_than_or_equal_monotone ? ?)).
385    napply (less_than_or_equal_zero).
386    nrepeat (napply (less_than_or_equal_monotone ? ?)).
387    napply (less_than_or_equal_zero).
388nqed.
389
390ndefinition get_ud_flag ≝
391  λs: Status.
392    let sfr ≝ special_function_registers_8051 s in
393    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
394      get_index Bool eight psw six ?.
395    nnormalize.
396    nrepeat (napply (less_than_or_equal_monotone ? ?)).
397    napply (less_than_or_equal_zero).
398    nrepeat (napply (less_than_or_equal_monotone ? ?)).
399    napply (less_than_or_equal_zero).
400nqed.
401
402ndefinition get_p_flag ≝
403  λs: Status.
404    let sfr ≝ special_function_registers_8051 s in
405    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
406      get_index Bool eight psw seven ?.
407    nnormalize.
408    nrepeat (napply (less_than_or_equal_monotone ? ?)).
409    napply (less_than_or_equal_zero).
410    nrepeat (napply (less_than_or_equal_monotone ? ?)).
411    napply (less_than_or_equal_zero).
412nqed.
[265]413
[257]414ndefinition initialise_status ≝
[285]415  let status ≝ mk_Status (Stub Byte sixteen)                    (* Code mem. *)
416                         (Stub Byte seven)                      (* Low mem.  *)
417                         (Stub Byte seven)                      (* High mem. *)
418                         (Stub Byte sixteen)                    (* Ext mem.  *)
419                         (zero sixteen)                         (* PC.       *)
420                         (replicate Byte nineteen (zero eight)) (* 8051 SFR. *)
421                         (replicate Byte five (zero eight))     (* 8052 SFR. *)
422                         (zero eight)                           (* P1 latch. *)
423                         (zero eight) in                        (* P3 latch. *)
[281]424  set_program_counter status (bitvector_of_nat sixteen seven).
425 
426naxiom not_implemented: False.
427 
428include "Arithmetic.ma".
429 
430ndefinition get_bit_addressable_sfr ≝
431  λs: Status.
432  λn: Nat.
433  λb: BitVector n.
434  λl: Bool.
435    let address ≝ nat_of_bitvector … b in
436      if (decidable_equality address one_hundred_and_twenty_eight) then
437        ?
438      else if (decidable_equality address one_hundred_and_forty_four) then
439        if l then
440          (p1_latch s)
441        else
442          (get_8051_sfr s SFR_P1)
443      else if (decidable_equality address one_hundred_and_sixty) then
444        ?
445      else if (decidable_equality address one_hundred_and_seventy_six) then
446        if l then
447          (p3_latch s)
448        else
449          (get_8051_sfr s SFR_P3)
450      else if (decidable_equality address one_hundred_and_fifty_three) then
451        get_8051_sfr s SFR_SBUF
452      else if (decidable_equality address one_hundred_and_thirty_eight) then
453        get_8051_sfr s SFR_TL0
454      else if (decidable_equality address one_hundred_and_thirty_nine) then
455        get_8051_sfr s SFR_TL1
456      else if (decidable_equality address one_hundred_and_forty) then
457        get_8051_sfr s SFR_TH0
458      else if (decidable_equality address one_hundred_and_forty_one) then
459        get_8051_sfr s SFR_TH1
460      else if (decidable_equality address two_hundred) then
461        get_8052_sfr s SFR_T2CON
462      else if (decidable_equality address two_hundred_and_two) then
463        get_8052_sfr s SFR_RCAP2L
464      else if (decidable_equality address two_hundred_and_three) then
465        get_8052_sfr s SFR_RCAP2H
466      else if (decidable_equality address two_hundred_and_four) then
467        get_8052_sfr s SFR_TL2
468      else if (decidable_equality address two_hundred_and_five) then
469        get_8052_sfr s SFR_TH2
470      else if (decidable_equality address one_hundred_and_thirty_five) then
471        get_8051_sfr s SFR_PCON
472      else if (decidable_equality address one_hundred_and_thirty_six) then
473        get_8051_sfr s SFR_TCON
474      else if (decidable_equality address one_hundred_and_thirty_seven) then
475        get_8051_sfr s SFR_TMOD
476      else if (decidable_equality address one_hundred_and_fifty_two) then
477        get_8051_sfr s SFR_SCON
478      else if (decidable_equality address one_hundred_and_sixty_eight) then
479        get_8051_sfr s SFR_IE
480      else if (decidable_equality address one_hundred_and_eighty_four) then
481        get_8051_sfr s SFR_IP
482      else if (decidable_equality address one_hundred_and_twenty_nine) then
483        get_8051_sfr s SFR_SP
484      else if (decidable_equality address one_hundred_and_thirty) then
485        get_8051_sfr s SFR_DPL
486      else if (decidable_equality address one_hundred_and_thirty_one) then
487        get_8051_sfr s SFR_DPH
488      else if (decidable_equality address two_hundred_and_eight) then
489        get_8051_sfr s SFR_PSW
490      else if (decidable_equality address two_hundred_and_twenty_four) then
491        get_8051_sfr s SFR_ACC_A
492      else if (decidable_equality address two_hundred_and_forty) then
493        get_8051_sfr s SFR_ACC_B
494      else
495        ?.
496      ncases not_implemented.
[285]497nqed.
498
499ndefinition set_bit_addressable_sfr ≝
500  λs: Status.
501  λb: Byte.
502    let address ≝ nat_of_bitvector … b in
503      if (decidable_equality address one_hundred_and_twenty_eight) then
504        ?
505      else if (decidable_equality address one_hundred_and_forty_four) then
506        let status_1 ≝ set_8051_sfr s SFR_P1 b in
507        let status_2 ≝ set_p1_latch s b in
508          status_2
509      else if (decidable_equality address one_hundred_and_sixty) then
510        ?
511      else if (decidable_equality address one_hundred_and_seventy_six) then
512        let status_1 ≝ set_8051_sfr s SFR_P3 b in
513        let status_2 ≝ set_p3_latch s b in
514          status_2
515      else if (decidable_equality address one_hundred_and_fifty_three) then
516        set_8051_sfr s SFR_SBUF b
517      else if (decidable_equality address one_hundred_and_thirty_eight) then
518        set_8051_sfr s SFR_TL0 b
519      else if (decidable_equality address one_hundred_and_thirty_nine) then
520        set_8051_sfr s SFR_TL1 b
521      else if (decidable_equality address one_hundred_and_forty) then
522        set_8051_sfr s SFR_TH0 b
523      else if (decidable_equality address one_hundred_and_forty_one) then
524        set_8051_sfr s SFR_TH1 b
525      else if (decidable_equality address two_hundred) then
526        set_8052_sfr s SFR_T2CON b
527      else if (decidable_equality address two_hundred_and_two) then
528        set_8052_sfr s SFR_RCAP2L b
529      else if (decidable_equality address two_hundred_and_three) then
530        set_8052_sfr s SFR_RCAP2H b
531      else if (decidable_equality address two_hundred_and_four) then
532        set_8052_sfr s SFR_TL2 b
533      else if (decidable_equality address two_hundred_and_five) then
534        set_8052_sfr s SFR_TH2 b
535      else if (decidable_equality address one_hundred_and_thirty_five) then
536        set_8051_sfr s SFR_PCON b
537      else if (decidable_equality address one_hundred_and_thirty_six) then
538        set_8051_sfr s SFR_TCON b
539      else if (decidable_equality address one_hundred_and_thirty_seven) then
540        set_8051_sfr s SFR_TMOD b
541      else if (decidable_equality address one_hundred_and_fifty_two) then
542        set_8051_sfr s SFR_SCON b
543      else if (decidable_equality address one_hundred_and_sixty_eight) then
544        set_8051_sfr s SFR_IE b
545      else if (decidable_equality address one_hundred_and_eighty_four) then
546        set_8051_sfr s SFR_IP b
547      else if (decidable_equality address one_hundred_and_twenty_nine) then
548        set_8051_sfr s SFR_SP b
549      else if (decidable_equality address one_hundred_and_thirty) then
550        set_8051_sfr s SFR_DPL b
551      else if (decidable_equality address one_hundred_and_thirty_one) then
552        set_8051_sfr s SFR_DPH b
553      else if (decidable_equality address two_hundred_and_eight) then
554        set_8051_sfr s SFR_PSW b
555      else if (decidable_equality address two_hundred_and_twenty_four) then
556        set_8051_sfr s SFR_ACC_A b
557      else if (decidable_equality address two_hundred_and_forty) then
558        set_8051_sfr s SFR_ACC_B b
559      else
560        ?.
561      ncases not_implemented.
[286]562nqed.
563
564ndefinition bit_address_of_register ≝
565  λs: Status.
566  λb, c, d: Bit.
567    let 〈 un, ln 〉 ≝ split ? four four (get_8051_sfr s SFR_PSW) in
568    let 〈 r1, r0 〉 ≝ mk_Cartesian … (get_index four un two ?) (get_index four un three ?) in
569    let offset ≝
570      if conjunction (negation r1) (negation r0) then
571        Z
572      else if conjunction (negation r1) r0 then
573        eight
574      else if conjunction r1 r0 then
575        twenty_four
576      else
577        sixteen
578    in
579      bitvector_of_nat seven (offset + (nat_of_bitvector ? [[ false ; b ; c ; d ]])).
580    nnormalize.
581    nrepeat (napply less_than_or_equal_monotone).
582    napply less_than_or_equal_zero.
583    nrepeat (napply less_than_or_equal_monotone).
584    napply less_than_or_equal_zero.
[287]585nqed.
586
587ndefinition get_register ≝
588  λs: Status.
589  λb, c, d: Bit.
590    let address ≝ bit_address_of_register s b c d in
591      lookup … address (low_internal_ram s) (zero eight).
592     
593ndefinition set_register ≝
594  λs: Status.
595  λb, c, d: Bit.
596  λv: Byte.
597    let address ≝ bit_address_of_register s b c d in
598    let old_low_internal_ram ≝ low_internal_ram s in
599    let new_low_internal_ram ≝ insert … address v old_low_internal_ram in
600      set_low_internal_ram s new_low_internal_ram.
601     
[288]602ndefinition set_flags ≝
603  λs: Status.
604  λcy: Bit.
605  λac: Maybe Bit.
606  λov: Bit.
607    let 〈 nu, nl 〉 ≝ split … four four (get_8051_sfr s SFR_PSW) in
608    let old_cy ≝ get_index … nu Z ? in
609    let old_ac ≝ get_index … nu one ? in
610    let old_fo ≝ get_index … nu two ? in
611    let old_rs1 ≝ get_index … nu three ? in
612    let old_rs0 ≝ get_index … nl Z ? in
613    let old_ov ≝ get_index … nl one ? in
614    let old_ud ≝ get_index … nl two ? in
615    let old_p ≝ get_index … nl three ? in
616    let new_ac ≝ match ac with [ Nothing ⇒ old_ac | Just j ⇒ j ] in
617    let new_psw ≝ [[ old_cy ; new_ac ; old_fo ; old_rs1 ;
618                     old_rs0 ; old_ov ; old_ud ; old_p ]] in
619      set_8051_sfr s SFR_PSW new_psw.
620    ##[##1,2,3,4,5,6,7,8:
621        nnormalize;
622        nrepeat (napply less_than_or_equal_monotone);
623        napply (less_than_or_equal_zero);
624    ##]
625nqed.
626     
[287]627ndefinition read_at_stack_pointer ≝
628  λs: Status.
629    let 〈 nu, nl 〉 ≝ split … four four (get_8051_sfr s SFR_SP) in
630    let m ≝ get_index … nu Z ? in
631    let r1 ≝ get_index … nu one ? in
632    let r2 ≝ get_index … nu two ? in
633    let r3 ≝ get_index … nu three ? in
634    let address ≝ [[ r1 ; r2 ; r3 ]] @@ nl in
635    let memory ≝
636      if m then
637        (low_internal_ram s)
638      else
639        (high_internal_ram s)
640    in
641      lookup … address memory (zero eight).
642    ##[##1,2,3,4:
643        nnormalize;
644        nrepeat (napply less_than_or_equal_monotone);
645        napply less_than_or_equal_zero;
646    ##]
[288]647nqed.
648
[289]649ndefinition write_at_stack_pointer ≝
[288]650  λs: Status.
651  λv: Byte.
[289]652    let 〈 nu, nl 〉 ≝ split … four four (get_8051_sfr s SFR_SP) in
653    let bit_zero ≝ get_index … nu Z ? in
654    let bit_one ≝ get_index … nu one ? in
655    let bit_two ≝ get_index … nu two ? in
656    let bit_three ≝ get_index … nu three ? in
657      if bit_zero then
658        let memory ≝ insert … ([[ bit_one ; bit_two ; bit_three ]] @@ nl)
659                              v (low_internal_ram s) in
660          set_low_internal_ram s memory
661      else
662        let memory ≝ insert … ([[ bit_one ; bit_two ; bit_three ]] @@ nl)
663                              v (high_internal_ram s) in
664          set_high_internal_ram s memory.
665    ##[##1,2,3,4:
666        nnormalize;
667        nrepeat (napply less_than_or_equal_monotone);
668        napply less_than_or_equal_zero;
669    ##]
670nqed.
Note: See TracBrowser for help on using the repository browser.