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

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

Moved definitions around so related are grouped together.

File size: 24.3 KB
Line 
1(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
2(* Interpret.ma: Operational semantics for the 8051/8052 processor.           *)
3(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
4
5(* include "ASM.ma". *)
6include "Arithmetic.ma".
7include "BitVectorTrie.ma".
8
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
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;
97  special_function_registers_8052: Vector Byte five;
98 
99  p1_latch: Byte;
100  p3_latch: Byte
101}.
102
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.
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.
152
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
171ndefinition set_8051_sfr ≝
172  λs: Status.
173  λi: SFR8051.
174  λb: Byte.
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
185    let old_p1_latch ≝ p1_latch s in
186    let old_p3_latch ≝ p3_latch s in
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
193                old_special_function_registers_8052
194                old_p1_latch
195                old_p3_latch.
196    napply (sfr8051_index_nineteen i).
197nqed.
198
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
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.
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
236    let old_p1_latch ≝ p1_latch s in
237    let old_p3_latch ≝ p3_latch s in
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
244                old_special_function_registers_8052
245                old_p1_latch
246                old_p3_latch.
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
257    let old_p1_latch ≝ p1_latch s in
258    let old_p3_latch ≝ p3_latch s in
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
265                old_special_function_registers_8052
266                old_p1_latch
267                old_p3_latch.
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
278    let old_p1_latch ≝ p1_latch s in
279    let old_p3_latch ≝ p3_latch s in
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
286                old_special_function_registers_8052
287                old_p1_latch
288                old_p3_latch.
289               
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               
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               
318ndefinition get_cy_flag ≝
319  λs: Status.
320    let sfr ≝ special_function_registers_8051 s in
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.
413
414ndefinition set_flags ≝
415  λs: Status.
416  λcy: Bit.
417  λac: Maybe Bit.
418  λov: Bit.
419    let 〈 nu, nl 〉 ≝ split … four four (get_8051_sfr s SFR_PSW) in
420    let old_cy ≝ get_index … nu Z ? in
421    let old_ac ≝ get_index … nu one ? in
422    let old_fo ≝ get_index … nu two ? in
423    let old_rs1 ≝ get_index … nu three ? in
424    let old_rs0 ≝ get_index … nl Z ? in
425    let old_ov ≝ get_index … nl one ? in
426    let old_ud ≝ get_index … nl two ? in
427    let old_p ≝ get_index … nl three ? in
428    let new_ac ≝ match ac with [ Nothing ⇒ old_ac | Just j ⇒ j ] in
429    let new_psw ≝ [[ old_cy ; new_ac ; old_fo ; old_rs1 ;
430                     old_rs0 ; old_ov ; old_ud ; old_p ]] in
431      set_8051_sfr s SFR_PSW new_psw.
432    ##[##1,2,3,4,5,6,7,8:
433        nnormalize;
434        nrepeat (napply less_than_or_equal_monotone);
435        napply (less_than_or_equal_zero);
436    ##]
437nqed.
438
439ndefinition initialise_status ≝
440  let status ≝ mk_Status (Stub Byte sixteen)                    (* Code mem. *)
441                         (Stub Byte seven)                      (* Low mem.  *)
442                         (Stub Byte seven)                      (* High mem. *)
443                         (Stub Byte sixteen)                    (* Ext mem.  *)
444                         (zero sixteen)                         (* PC.       *)
445                         (replicate Byte nineteen (zero eight)) (* 8051 SFR. *)
446                         (replicate Byte five (zero eight))     (* 8052 SFR. *)
447                         (zero eight)                           (* P1 latch. *)
448                         (zero eight) in                        (* P3 latch. *)
449  set_program_counter status (bitvector_of_nat sixteen seven).
450 
451naxiom not_implemented: False.
452 
453include "Arithmetic.ma".
454 
455ndefinition get_bit_addressable_sfr ≝
456  λs: Status.
457  λn: Nat.
458  λb: BitVector n.
459  λl: Bool.
460    let address ≝ nat_of_bitvector … b in
461      if (decidable_equality address one_hundred_and_twenty_eight) then
462        ?
463      else if (decidable_equality address one_hundred_and_forty_four) then
464        if l then
465          (p1_latch s)
466        else
467          (get_8051_sfr s SFR_P1)
468      else if (decidable_equality address one_hundred_and_sixty) then
469        ?
470      else if (decidable_equality address one_hundred_and_seventy_six) then
471        if l then
472          (p3_latch s)
473        else
474          (get_8051_sfr s SFR_P3)
475      else if (decidable_equality address one_hundred_and_fifty_three) then
476        get_8051_sfr s SFR_SBUF
477      else if (decidable_equality address one_hundred_and_thirty_eight) then
478        get_8051_sfr s SFR_TL0
479      else if (decidable_equality address one_hundred_and_thirty_nine) then
480        get_8051_sfr s SFR_TL1
481      else if (decidable_equality address one_hundred_and_forty) then
482        get_8051_sfr s SFR_TH0
483      else if (decidable_equality address one_hundred_and_forty_one) then
484        get_8051_sfr s SFR_TH1
485      else if (decidable_equality address two_hundred) then
486        get_8052_sfr s SFR_T2CON
487      else if (decidable_equality address two_hundred_and_two) then
488        get_8052_sfr s SFR_RCAP2L
489      else if (decidable_equality address two_hundred_and_three) then
490        get_8052_sfr s SFR_RCAP2H
491      else if (decidable_equality address two_hundred_and_four) then
492        get_8052_sfr s SFR_TL2
493      else if (decidable_equality address two_hundred_and_five) then
494        get_8052_sfr s SFR_TH2
495      else if (decidable_equality address one_hundred_and_thirty_five) then
496        get_8051_sfr s SFR_PCON
497      else if (decidable_equality address one_hundred_and_thirty_six) then
498        get_8051_sfr s SFR_TCON
499      else if (decidable_equality address one_hundred_and_thirty_seven) then
500        get_8051_sfr s SFR_TMOD
501      else if (decidable_equality address one_hundred_and_fifty_two) then
502        get_8051_sfr s SFR_SCON
503      else if (decidable_equality address one_hundred_and_sixty_eight) then
504        get_8051_sfr s SFR_IE
505      else if (decidable_equality address one_hundred_and_eighty_four) then
506        get_8051_sfr s SFR_IP
507      else if (decidable_equality address one_hundred_and_twenty_nine) then
508        get_8051_sfr s SFR_SP
509      else if (decidable_equality address one_hundred_and_thirty) then
510        get_8051_sfr s SFR_DPL
511      else if (decidable_equality address one_hundred_and_thirty_one) then
512        get_8051_sfr s SFR_DPH
513      else if (decidable_equality address two_hundred_and_eight) then
514        get_8051_sfr s SFR_PSW
515      else if (decidable_equality address two_hundred_and_twenty_four) then
516        get_8051_sfr s SFR_ACC_A
517      else if (decidable_equality address two_hundred_and_forty) then
518        get_8051_sfr s SFR_ACC_B
519      else
520        ?.
521      ncases not_implemented.
522nqed.
523
524ndefinition set_bit_addressable_sfr ≝
525  λs: Status.
526  λb: Byte.
527    let address ≝ nat_of_bitvector … b in
528      if (decidable_equality address one_hundred_and_twenty_eight) then
529        ?
530      else if (decidable_equality address one_hundred_and_forty_four) then
531        let status_1 ≝ set_8051_sfr s SFR_P1 b in
532        let status_2 ≝ set_p1_latch s b in
533          status_2
534      else if (decidable_equality address one_hundred_and_sixty) then
535        ?
536      else if (decidable_equality address one_hundred_and_seventy_six) then
537        let status_1 ≝ set_8051_sfr s SFR_P3 b in
538        let status_2 ≝ set_p3_latch s b in
539          status_2
540      else if (decidable_equality address one_hundred_and_fifty_three) then
541        set_8051_sfr s SFR_SBUF b
542      else if (decidable_equality address one_hundred_and_thirty_eight) then
543        set_8051_sfr s SFR_TL0 b
544      else if (decidable_equality address one_hundred_and_thirty_nine) then
545        set_8051_sfr s SFR_TL1 b
546      else if (decidable_equality address one_hundred_and_forty) then
547        set_8051_sfr s SFR_TH0 b
548      else if (decidable_equality address one_hundred_and_forty_one) then
549        set_8051_sfr s SFR_TH1 b
550      else if (decidable_equality address two_hundred) then
551        set_8052_sfr s SFR_T2CON b
552      else if (decidable_equality address two_hundred_and_two) then
553        set_8052_sfr s SFR_RCAP2L b
554      else if (decidable_equality address two_hundred_and_three) then
555        set_8052_sfr s SFR_RCAP2H b
556      else if (decidable_equality address two_hundred_and_four) then
557        set_8052_sfr s SFR_TL2 b
558      else if (decidable_equality address two_hundred_and_five) then
559        set_8052_sfr s SFR_TH2 b
560      else if (decidable_equality address one_hundred_and_thirty_five) then
561        set_8051_sfr s SFR_PCON b
562      else if (decidable_equality address one_hundred_and_thirty_six) then
563        set_8051_sfr s SFR_TCON b
564      else if (decidable_equality address one_hundred_and_thirty_seven) then
565        set_8051_sfr s SFR_TMOD b
566      else if (decidable_equality address one_hundred_and_fifty_two) then
567        set_8051_sfr s SFR_SCON b
568      else if (decidable_equality address one_hundred_and_sixty_eight) then
569        set_8051_sfr s SFR_IE b
570      else if (decidable_equality address one_hundred_and_eighty_four) then
571        set_8051_sfr s SFR_IP b
572      else if (decidable_equality address one_hundred_and_twenty_nine) then
573        set_8051_sfr s SFR_SP b
574      else if (decidable_equality address one_hundred_and_thirty) then
575        set_8051_sfr s SFR_DPL b
576      else if (decidable_equality address one_hundred_and_thirty_one) then
577        set_8051_sfr s SFR_DPH b
578      else if (decidable_equality address two_hundred_and_eight) then
579        set_8051_sfr s SFR_PSW b
580      else if (decidable_equality address two_hundred_and_twenty_four) then
581        set_8051_sfr s SFR_ACC_A b
582      else if (decidable_equality address two_hundred_and_forty) then
583        set_8051_sfr s SFR_ACC_B b
584      else
585        ?.
586      ncases not_implemented.
587nqed.
588
589ndefinition bit_address_of_register ≝
590  λs: Status.
591  λb, c, d: Bit.
592    let 〈 un, ln 〉 ≝ split ? four four (get_8051_sfr s SFR_PSW) in
593    let 〈 r1, r0 〉 ≝ mk_Cartesian … (get_index four un two ?) (get_index four un three ?) in
594    let offset ≝
595      if conjunction (negation r1) (negation r0) then
596        Z
597      else if conjunction (negation r1) r0 then
598        eight
599      else if conjunction r1 r0 then
600        twenty_four
601      else
602        sixteen
603    in
604      bitvector_of_nat seven (offset + (nat_of_bitvector ? [[ false ; b ; c ; d ]])).
605    nnormalize.
606    nrepeat (napply less_than_or_equal_monotone).
607    napply less_than_or_equal_zero.
608    nrepeat (napply less_than_or_equal_monotone).
609    napply less_than_or_equal_zero.
610nqed.
611
612ndefinition get_register ≝
613  λs: Status.
614  λb, c, d: Bit.
615    let address ≝ bit_address_of_register s b c d in
616      lookup … address (low_internal_ram s) (zero eight).
617     
618ndefinition set_register ≝
619  λs: Status.
620  λb, c, d: Bit.
621  λv: Byte.
622    let address ≝ bit_address_of_register s b c d in
623    let old_low_internal_ram ≝ low_internal_ram s in
624    let new_low_internal_ram ≝ insert … address v old_low_internal_ram in
625      set_low_internal_ram s new_low_internal_ram.
626     
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    ##]
647nqed.
648
649ndefinition write_at_stack_pointer ≝
650  λs: Status.
651  λv: Byte.
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.