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

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

Finished all get_ and set_arg_* functions.

File size: 36.5 KB
Line 
1(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
2(* Interpret.ma: Operational semantics for the 8051/8052 processor.           *)
3(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
4
5include "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               
312ndefinition set_external_ram ≝
313  λs: Status.
314  λr: BitVectorTrie Byte sixteen.
315    let old_code_memory ≝ code_memory s in
316    let old_low_internal_ram ≝ low_internal_ram s in
317    let old_high_internal_ram ≝ high_internal_ram s in
318    let old_program_counter ≝ program_counter s in
319    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
320    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
321    let old_p1_latch ≝ p1_latch s in
322    let old_p3_latch ≝ p3_latch s in
323      mk_Status old_code_memory
324                old_low_internal_ram
325                old_high_internal_ram
326                r
327                old_program_counter
328                old_special_function_registers_8051
329                old_special_function_registers_8052
330                old_p1_latch
331                old_p3_latch.
332               
333naxiom less_than_or_equal_monotone:
334  ∀m, n: Nat.
335    m ≤ n → S m ≤ S n.
336   
337alias id "get_index" = "cic:/matita/ng/Vector/get_index.fix(0,3,2)".
338               
339ndefinition get_cy_flag ≝
340  λs: Status.
341    let sfr ≝ special_function_registers_8051 s in
342    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
343      get_index Bool eight psw Z ?.
344    nnormalize.
345    napply (less_than_or_equal_monotone ? ?).
346    napply (less_than_or_equal_zero).
347    nrepeat (napply (less_than_or_equal_monotone ? ?)).
348    napply (less_than_or_equal_zero).
349nqed.
350
351ndefinition get_ac_flag ≝
352  λs: Status.
353    let sfr ≝ special_function_registers_8051 s in
354    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
355      get_index Bool eight psw (S Z) ?.
356    nnormalize.
357    nrepeat (napply (less_than_or_equal_monotone ? ?)).
358    napply (less_than_or_equal_zero).
359    nrepeat (napply (less_than_or_equal_monotone ? ?)).
360    napply (less_than_or_equal_zero).
361nqed.
362
363ndefinition get_fo_flag ≝
364  λs: Status.
365    let sfr ≝ special_function_registers_8051 s in
366    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
367      get_index Bool eight psw two ?.
368    nnormalize.
369    nrepeat (napply (less_than_or_equal_monotone ? ?)).
370    napply (less_than_or_equal_zero).
371    nrepeat (napply (less_than_or_equal_monotone ? ?)).
372    napply (less_than_or_equal_zero).
373nqed.
374
375ndefinition get_rs1_flag ≝
376  λs: Status.
377    let sfr ≝ special_function_registers_8051 s in
378    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
379      get_index Bool eight psw three ?.
380    nnormalize.
381    nrepeat (napply (less_than_or_equal_monotone ? ?)).
382    napply (less_than_or_equal_zero).
383    nrepeat (napply (less_than_or_equal_monotone ? ?)).
384    napply (less_than_or_equal_zero).
385nqed.
386
387ndefinition get_rs0_flag ≝
388  λs: Status.
389    let sfr ≝ special_function_registers_8051 s in
390    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
391      get_index Bool eight psw four ?.
392    nnormalize.
393    nrepeat (napply (less_than_or_equal_monotone ? ?)).
394    napply (less_than_or_equal_zero).
395    nrepeat (napply (less_than_or_equal_monotone ? ?)).
396    napply (less_than_or_equal_zero).
397nqed.
398
399ndefinition get_ov_flag ≝
400  λs: Status.
401    let sfr ≝ special_function_registers_8051 s in
402    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
403      get_index Bool eight psw five ?.
404    nnormalize.
405    nrepeat (napply (less_than_or_equal_monotone ? ?)).
406    napply (less_than_or_equal_zero).
407    nrepeat (napply (less_than_or_equal_monotone ? ?)).
408    napply (less_than_or_equal_zero).
409nqed.
410
411ndefinition get_ud_flag ≝
412  λs: Status.
413    let sfr ≝ special_function_registers_8051 s in
414    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
415      get_index Bool eight psw six ?.
416    nnormalize.
417    nrepeat (napply (less_than_or_equal_monotone ? ?)).
418    napply (less_than_or_equal_zero).
419    nrepeat (napply (less_than_or_equal_monotone ? ?)).
420    napply (less_than_or_equal_zero).
421nqed.
422
423ndefinition get_p_flag ≝
424  λs: Status.
425    let sfr ≝ special_function_registers_8051 s in
426    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
427      get_index Bool eight psw seven ?.
428    nnormalize.
429    nrepeat (napply (less_than_or_equal_monotone ? ?)).
430    napply (less_than_or_equal_zero).
431    nrepeat (napply (less_than_or_equal_monotone ? ?)).
432    napply (less_than_or_equal_zero).
433nqed.
434
435ndefinition set_flags ≝
436  λs: Status.
437  λcy: Bit.
438  λac: Maybe Bit.
439  λov: Bit.
440    let 〈 nu, nl 〉 ≝ split … four four (get_8051_sfr s SFR_PSW) in
441    let old_cy ≝ get_index … nu Z ? in
442    let old_ac ≝ get_index … nu one ? in
443    let old_fo ≝ get_index … nu two ? in
444    let old_rs1 ≝ get_index … nu three ? in
445    let old_rs0 ≝ get_index … nl Z ? in
446    let old_ov ≝ get_index … nl one ? in
447    let old_ud ≝ get_index … nl two ? in
448    let old_p ≝ get_index … nl three ? in
449    let new_ac ≝ match ac with [ Nothing ⇒ old_ac | Just j ⇒ j ] in
450    let new_psw ≝ [[ old_cy ; new_ac ; old_fo ; old_rs1 ;
451                     old_rs0 ; old_ov ; old_ud ; old_p ]] in
452      set_8051_sfr s SFR_PSW new_psw.
453    ##[##1,2,3,4,5,6,7,8:
454        nnormalize;
455        nrepeat (napply less_than_or_equal_monotone);
456        napply (less_than_or_equal_zero);
457    ##]
458nqed.
459
460ndefinition initialise_status ≝
461  let status ≝ mk_Status (Stub Byte sixteen)                    (* Code mem. *)
462                         (Stub Byte seven)                      (* Low mem.  *)
463                         (Stub Byte seven)                      (* High mem. *)
464                         (Stub Byte sixteen)                    (* Ext mem.  *)
465                         (zero sixteen)                         (* PC.       *)
466                         (replicate Byte nineteen (zero eight)) (* 8051 SFR. *)
467                         (replicate Byte five (zero eight))     (* 8052 SFR. *)
468                         (zero eight)                           (* P1 latch. *)
469                         (zero eight) in                        (* P3 latch. *)
470  set_program_counter status (bitvector_of_nat sixteen seven).
471 
472naxiom not_implemented: False.
473 
474include "Arithmetic.ma".
475 
476ndefinition get_bit_addressable_sfr ≝
477  λs: Status.
478  λn: Nat.
479  λb: BitVector n.
480  λl: Bool.
481    let address ≝ nat_of_bitvector … b in
482      if (decidable_equality address one_hundred_and_twenty_eight) then
483        ?
484      else if (decidable_equality address one_hundred_and_forty_four) then
485        if l then
486          (p1_latch s)
487        else
488          (get_8051_sfr s SFR_P1)
489      else if (decidable_equality address one_hundred_and_sixty) then
490        ?
491      else if (decidable_equality address one_hundred_and_seventy_six) then
492        if l then
493          (p3_latch s)
494        else
495          (get_8051_sfr s SFR_P3)
496      else if (decidable_equality address one_hundred_and_fifty_three) then
497        get_8051_sfr s SFR_SBUF
498      else if (decidable_equality address one_hundred_and_thirty_eight) then
499        get_8051_sfr s SFR_TL0
500      else if (decidable_equality address one_hundred_and_thirty_nine) then
501        get_8051_sfr s SFR_TL1
502      else if (decidable_equality address one_hundred_and_forty) then
503        get_8051_sfr s SFR_TH0
504      else if (decidable_equality address one_hundred_and_forty_one) then
505        get_8051_sfr s SFR_TH1
506      else if (decidable_equality address two_hundred) then
507        get_8052_sfr s SFR_T2CON
508      else if (decidable_equality address two_hundred_and_two) then
509        get_8052_sfr s SFR_RCAP2L
510      else if (decidable_equality address two_hundred_and_three) then
511        get_8052_sfr s SFR_RCAP2H
512      else if (decidable_equality address two_hundred_and_four) then
513        get_8052_sfr s SFR_TL2
514      else if (decidable_equality address two_hundred_and_five) then
515        get_8052_sfr s SFR_TH2
516      else if (decidable_equality address one_hundred_and_thirty_five) then
517        get_8051_sfr s SFR_PCON
518      else if (decidable_equality address one_hundred_and_thirty_six) then
519        get_8051_sfr s SFR_TCON
520      else if (decidable_equality address one_hundred_and_thirty_seven) then
521        get_8051_sfr s SFR_TMOD
522      else if (decidable_equality address one_hundred_and_fifty_two) then
523        get_8051_sfr s SFR_SCON
524      else if (decidable_equality address one_hundred_and_sixty_eight) then
525        get_8051_sfr s SFR_IE
526      else if (decidable_equality address one_hundred_and_eighty_four) then
527        get_8051_sfr s SFR_IP
528      else if (decidable_equality address one_hundred_and_twenty_nine) then
529        get_8051_sfr s SFR_SP
530      else if (decidable_equality address one_hundred_and_thirty) then
531        get_8051_sfr s SFR_DPL
532      else if (decidable_equality address one_hundred_and_thirty_one) then
533        get_8051_sfr s SFR_DPH
534      else if (decidable_equality address two_hundred_and_eight) then
535        get_8051_sfr s SFR_PSW
536      else if (decidable_equality address two_hundred_and_twenty_four) then
537        get_8051_sfr s SFR_ACC_A
538      else if (decidable_equality address two_hundred_and_forty) then
539        get_8051_sfr s SFR_ACC_B
540      else
541        ?.
542      ncases not_implemented.
543nqed.
544
545ndefinition set_bit_addressable_sfr ≝
546  λs: Status.
547  λb: Byte.
548  λv: Byte.
549    let address ≝ nat_of_bitvector … b in
550      if (decidable_equality address one_hundred_and_twenty_eight) then
551        ?
552      else if (decidable_equality address one_hundred_and_forty_four) then
553        let status_1 ≝ set_8051_sfr s SFR_P1 v in
554        let status_2 ≝ set_p1_latch s v in
555          status_2
556      else if (decidable_equality address one_hundred_and_sixty) then
557        ?
558      else if (decidable_equality address one_hundred_and_seventy_six) then
559        let status_1 ≝ set_8051_sfr s SFR_P3 v in
560        let status_2 ≝ set_p3_latch s v in
561          status_2
562      else if (decidable_equality address one_hundred_and_fifty_three) then
563        set_8051_sfr s SFR_SBUF v
564      else if (decidable_equality address one_hundred_and_thirty_eight) then
565        set_8051_sfr s SFR_TL0 v
566      else if (decidable_equality address one_hundred_and_thirty_nine) then
567        set_8051_sfr s SFR_TL1 v
568      else if (decidable_equality address one_hundred_and_forty) then
569        set_8051_sfr s SFR_TH0 v
570      else if (decidable_equality address one_hundred_and_forty_one) then
571        set_8051_sfr s SFR_TH1 v
572      else if (decidable_equality address two_hundred) then
573        set_8052_sfr s SFR_T2CON v
574      else if (decidable_equality address two_hundred_and_two) then
575        set_8052_sfr s SFR_RCAP2L v
576      else if (decidable_equality address two_hundred_and_three) then
577        set_8052_sfr s SFR_RCAP2H v
578      else if (decidable_equality address two_hundred_and_four) then
579        set_8052_sfr s SFR_TL2 v
580      else if (decidable_equality address two_hundred_and_five) then
581        set_8052_sfr s SFR_TH2 v
582      else if (decidable_equality address one_hundred_and_thirty_five) then
583        set_8051_sfr s SFR_PCON v
584      else if (decidable_equality address one_hundred_and_thirty_six) then
585        set_8051_sfr s SFR_TCON v
586      else if (decidable_equality address one_hundred_and_thirty_seven) then
587        set_8051_sfr s SFR_TMOD v
588      else if (decidable_equality address one_hundred_and_fifty_two) then
589        set_8051_sfr s SFR_SCON v
590      else if (decidable_equality address one_hundred_and_sixty_eight) then
591        set_8051_sfr s SFR_IE v
592      else if (decidable_equality address one_hundred_and_eighty_four) then
593        set_8051_sfr s SFR_IP v
594      else if (decidable_equality address one_hundred_and_twenty_nine) then
595        set_8051_sfr s SFR_SP v
596      else if (decidable_equality address one_hundred_and_thirty) then
597        set_8051_sfr s SFR_DPL v
598      else if (decidable_equality address one_hundred_and_thirty_one) then
599        set_8051_sfr s SFR_DPH v
600      else if (decidable_equality address two_hundred_and_eight) then
601        set_8051_sfr s SFR_PSW v
602      else if (decidable_equality address two_hundred_and_twenty_four) then
603        set_8051_sfr s SFR_ACC_A v
604      else if (decidable_equality address two_hundred_and_forty) then
605        set_8051_sfr s SFR_ACC_B v
606      else
607        ?.
608      ncases not_implemented.
609nqed.
610
611ndefinition bit_address_of_register ≝
612  λs: Status.
613  λb, c, d: Bit.
614    let 〈 un, ln 〉 ≝ split ? four four (get_8051_sfr s SFR_PSW) in
615    let 〈 r1, r0 〉 ≝ mk_Cartesian … (get_index four un two ?) (get_index four un three ?) in
616    let offset ≝
617      if conjunction (negation r1) (negation r0) then
618        Z
619      else if conjunction (negation r1) r0 then
620        eight
621      else if conjunction r1 r0 then
622        twenty_four
623      else
624        sixteen
625    in
626      bitvector_of_nat seven (offset + (nat_of_bitvector ? [[ false ; b ; c ; d ]])).
627    nnormalize.
628    nrepeat (napply less_than_or_equal_monotone).
629    napply less_than_or_equal_zero.
630    nrepeat (napply less_than_or_equal_monotone).
631    napply less_than_or_equal_zero.
632nqed.
633
634ndefinition get_register ≝
635  λs: Status.
636  λb, c, d: Bit.
637    let address ≝ bit_address_of_register s b c d in
638      lookup … address (low_internal_ram s) (zero eight).
639     
640ndefinition set_register ≝
641  λs: Status.
642  λb, c, d: Bit.
643  λv: Byte.
644    let address ≝ bit_address_of_register s b c d in
645    let old_low_internal_ram ≝ low_internal_ram s in
646    let new_low_internal_ram ≝ insert … address v old_low_internal_ram in
647      set_low_internal_ram s new_low_internal_ram.
648     
649ndefinition read_at_stack_pointer ≝
650  λs: Status.
651    let 〈 nu, nl 〉 ≝ split … four four (get_8051_sfr s SFR_SP) in
652    let m ≝ get_index … nu Z ? in
653    let r1 ≝ get_index … nu one ? in
654    let r2 ≝ get_index … nu two ? in
655    let r3 ≝ get_index … nu three ? in
656    let address ≝ [[ r1 ; r2 ; r3 ]] @@ nl in
657    let memory ≝
658      if m then
659        (low_internal_ram s)
660      else
661        (high_internal_ram s)
662    in
663      lookup … address memory (zero eight).
664    ##[##1,2,3,4:
665        nnormalize;
666        nrepeat (napply less_than_or_equal_monotone);
667        napply less_than_or_equal_zero;
668    ##]
669nqed.
670
671ndefinition write_at_stack_pointer ≝
672  λs: Status.
673  λv: Byte.
674    let 〈 nu, nl 〉 ≝ split … four four (get_8051_sfr s SFR_SP) in
675    let bit_zero ≝ get_index … nu Z ? in
676    let bit_one ≝ get_index … nu one ? in
677    let bit_two ≝ get_index … nu two ? in
678    let bit_three ≝ get_index … nu three ? in
679      if bit_zero then
680        let memory ≝ insert … ([[ bit_one ; bit_two ; bit_three ]] @@ nl)
681                              v (low_internal_ram s) in
682          set_low_internal_ram s memory
683      else
684        let memory ≝ insert … ([[ bit_one ; bit_two ; bit_three ]] @@ nl)
685                              v (high_internal_ram s) in
686          set_high_internal_ram s memory.
687    ##[##1,2,3,4:
688        nnormalize;
689        nrepeat (napply less_than_or_equal_monotone);
690        napply less_than_or_equal_zero;
691    ##]
692nqed.
693
694ndefinition set_arg_16: Status → Word → [[ dptr ]] → Status ≝
695  λs,v,a.
696   match a return λx. bool_to_Prop (is_in ? [[ dptr ]] x) → ? with
697     [ DPTR ⇒ λ_:True.
698       let 〈 bu, bl 〉 ≝ split … eight eight v in
699       let status ≝ set_8051_sfr s SFR_DPH bu in
700       let status ≝ set_8051_sfr status SFR_DPL bl in
701         status
702     | _ ⇒ λK.
703       match K in False with
704       [
705       ]
706     ] (subaddressing_modein … a).
707   
708ndefinition get_arg_16: Status → [[ data16 ]] → Word ≝
709  λs, a.
710    match a return λx. bool_to_Prop (is_in ? [[ data16 ]] x) → ? with
711      [ DATA16 d ⇒ λ_:True. d
712      | _ ⇒ λK.
713        match K in False with
714        [
715        ]
716      ] (subaddressing_modein … a).
717     
718ndefinition get_arg_8: Status → Bool → [[ direct ; indirect ; register ;
719                                          acc_a ; acc_b ; data ; acc_dptr ;
720                                          acc_pc ; ext_indirect ;
721                                          ext_indirect_dptr ]] → Byte ≝
722  λs, l, a.
723    match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; register ;
724                                                acc_a ; acc_b ; data ; acc_dptr ;
725                                                acc_pc ; ext_indirect ;
726                                                ext_indirect_dptr ]] x) → ? with
727      [ ACC_A ⇒ λacc_a: True. get_8051_sfr s SFR_ACC_A
728      | ACC_B ⇒ λacc_b: True. get_8051_sfr s SFR_ACC_B
729      | DATA d ⇒ λdata: True. d
730      | REGISTER r1 r2 r3 ⇒ λregister: True. get_register s r1 r2 r3
731      | EXT_INDIRECT_DPTR ⇒
732        λext_indirect_dptr: True.
733          let address ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
734            lookup … sixteen address (external_ram s) (zero eight)
735      | EXT_INDIRECT e ⇒
736        λext_indirect: True.
737          let address ≝ get_register s false false e in
738          let padded_address ≝ pad eight eight address in
739            lookup … sixteen padded_address (external_ram s) (zero eight)
740      | ACC_DPTR ⇒
741        λacc_dptr: True.
742          let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
743          let padded_acc ≝ pad eight eight (get_8051_sfr s SFR_ACC_A) in
744          let 〈 carry, address 〉 ≝ half_add sixteen dptr padded_acc in
745            lookup … sixteen address (external_ram s) (zero eight)
746      | ACC_PC ⇒
747        λacc_pc: True.
748          let padded_acc ≝ pad eight eight (get_8051_sfr s SFR_ACC_A) in
749          let 〈 carry, address 〉 ≝ half_add sixteen (program_counter s) padded_acc in
750            lookup … sixteen address (external_ram s) (zero eight)
751      | DIRECT d ⇒
752        λdirect: True.
753          let 〈 nu, nl 〉 ≝ split … four four d in
754          let bit_one ≝ get_index … nu one ? in
755            match bit_one with
756              [ true ⇒
757                  let 〈 bit_one, three_bits 〉 ≝ split ? one three nu in
758                  let address ≝ three_bits @@ nl in
759                    lookup ? seven address (low_internal_ram s) (zero eight)
760              | false ⇒ get_bit_addressable_sfr s eight d l
761              ]
762      | INDIRECT i ⇒
763        λindirect: True.
764          let 〈 nu, nl 〉 ≝ split ? four four (get_register s false false i) in
765          let 〈 bit_one_v, three_bits 〉 ≝ split ? one three nu in
766          let bit_one ≝ get_index … bit_one_v Z ? in
767          match bit_one with
768            [ true ⇒
769                lookup ? seven (three_bits @@ nl) (low_internal_ram s) (zero eight)
770            | false ⇒
771                lookup ? seven (three_bits @@ nl) (high_internal_ram s) (zero eight)
772            ]
773      | _ ⇒ λother.
774        match other in False with [ ]
775      ] (subaddressing_modein … a).
776      ##[##1,2:
777          nnormalize;
778          nrepeat (napply less_than_or_equal_monotone);
779          napply less_than_or_equal_zero;
780      ##]
781nqed.
782
783ndefinition set_arg_8: Status → [[ direct ; indirect ; register ;
784                                   acc_a ; acc_b ; ext_indirect ;
785                                   ext_indirect_dptr ]] → Byte → Status ≝
786  λs, a, v.
787    match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; register ;
788                                                acc_a ; acc_b ; ext_indirect ;
789                                                ext_indirect_dptr ]] x) → ? with
790      [ DIRECT d ⇒
791        λdirect: True.
792          let 〈 nu, nl 〉 ≝ split … four four d in
793          let bit_one ≝ get_index … nu one ? in
794          let 〈 ignore, three_bits 〉 ≝ split ? one three nu in
795            match bit_one with
796              [ true ⇒ set_bit_addressable_sfr s d v
797              | false ⇒
798                let memory ≝ insert ? seven (three_bits @@ nl) v (low_internal_ram s) in
799                  set_low_internal_ram s memory
800              ]
801      | INDIRECT i ⇒
802        λindirect: True.
803          let register ≝ get_register s false false i in
804          let 〈 nu, nl 〉 ≝ split ? four four register in
805          let bit_one ≝ get_index ? nu one ? in
806          let 〈 ignore, three_bits 〉 ≝ split ? one three nu in
807          match bit_one with
808            [ true ⇒
809              let memory ≝ insert … (three_bits @@ nl) v (low_internal_ram s) in
810                set_low_internal_ram s memory
811            | false ⇒
812              let memory ≝ insert … (three_bits @@ nl) v (high_internal_ram s) in
813                set_high_internal_ram s memory
814            ]
815      | REGISTER r1 r2 r3 ⇒ λregister: True. set_register s r1 r2 r3 v
816      | ACC_A ⇒ λacc_a: True. set_8051_sfr s SFR_ACC_A v
817      | ACC_B ⇒ λacc_b: True. set_8051_sfr s SFR_ACC_B v
818      | EXT_INDIRECT e ⇒
819        λext_indirect: True.
820          let address ≝ get_register s false false e in
821          let padded_address ≝ pad eight eight address in
822          let memory ≝ insert ? sixteen padded_address v (external_ram s) in
823            set_external_ram s memory
824      | EXT_INDIRECT_DPTR ⇒
825        λext_indirect_dptr: True.
826          let address ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
827          let memory ≝ insert ? sixteen address v (external_ram s) in
828            set_external_ram s memory
829      | _ ⇒
830        λother: False.
831          match other in False with [ ]
832      ] (subaddressing_modein … a).
833      ##[##1,2:
834          nnormalize;
835          nrepeat (napply less_than_or_equal_monotone);
836          napply less_than_or_equal_zero
837      ##]
838nqed.
839
840naxiom modulus_less_than:
841  ∀m,n: Nat.
842    (m mod n) < n.
843
844ndefinition get_arg_1: Status → [[ bit_addr ; n_bit_addr ; carry ]] →
845                       Bool → Bool ≝
846  λs, a, l.
847    match a return λx. bool_to_Prop (is_in ? [[ bit_addr ;
848                                                 n_bit_addr ;
849                                                 carry ]] x) → ? with
850      [ BIT_ADDR b ⇒
851        λbit_addr: True.
852          let 〈 nu, nl 〉 ≝ split … four four b in
853          let bit_one ≝ get_index … nu one ? in
854          let 〈 bit_one_v, three_bits 〉 ≝ split ? one three nu in
855            match bit_one with
856              [ true ⇒
857                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
858                let d ≝ address ÷ eight in
859                let m ≝ address mod eight in
860                let trans ≝ bitvector_of_nat eight ((d * eight) + one_hundred_and_twenty_eight) in
861                let sfr ≝ get_bit_addressable_sfr s ? trans l in
862                  get_index ? sfr m ?
863              | false ⇒
864                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
865                let address' ≝ bitvector_of_nat seven ((address ÷ eight) + thirty_two) in
866                let t ≝ lookup … seven address' (low_internal_ram s) (zero eight) in
867                  get_index ? t (modulus address eight) ?
868              ]
869      | N_BIT_ADDR n ⇒
870        λn_bit_addr: True.
871          let 〈 nu, nl 〉 ≝ split … four four n in
872          let bit_one ≝ get_index … nu one ? in
873          let 〈 bit_one_v, three_bits 〉 ≝ split ? one three nu in
874            match bit_one with
875              [ true ⇒
876                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
877                let d ≝ address ÷ eight in
878                let m ≝ address mod eight in
879                let trans ≝ bitvector_of_nat eight ((d * eight) + one_hundred_and_twenty_eight) in
880                let sfr ≝ get_bit_addressable_sfr s ? trans l in
881                  negation (get_index ? sfr m ?)
882              | false ⇒
883                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
884                let address' ≝ bitvector_of_nat seven ((address ÷ eight) + thirty_two) in
885                let trans ≝ lookup … seven address' (low_internal_ram s) (zero eight) in
886                  negation (get_index ? trans (modulus address eight) ?)
887              ]
888      | CARRY ⇒ λcarry: True. get_cy_flag s
889      | _ ⇒ λother.
890        match other in False with [ ]
891      ] (subaddressing_modein … a).
892      ##[##3,6:
893          nnormalize;
894          nrepeat (napply less_than_or_equal_monotone);
895          napply less_than_or_equal_zero;
896      ##|##1,2,4,5:
897          napply modulus_less_than;
898      ##]
899nqed.
900     
901ndefinition set_arg_1: Status → [[ bit_addr ; carry ]] →
902                       Bit → Status ≝
903  λs, a, v.
904    match a return λx. bool_to_Prop (is_in ? [[ bit_addr ; carry ]] x) → ? with
905      [ BIT_ADDR b ⇒ λbit_addr: True.
906          let 〈 nu, nl 〉 ≝ split ? four four (get_8051_sfr s SFR_PSW) in
907          let bit_one ≝ get_index ? nu one ? in
908          let 〈 ignore, three_bits 〉 ≝ split ? one three nu in
909          match bit_one with
910            [ true ⇒
911                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
912                let d ≝ address ÷ eight in
913                let m ≝ address mod eight in
914                let t ≝ bitvector_of_nat eight ((d * eight) + one_hundred_and_twenty_eight) in
915                let sfr ≝ get_bit_addressable_sfr s ? t true in
916                let new_sfr ≝ set_index … sfr m v ? in
917                  set_bit_addressable_sfr s new_sfr t
918            | false ⇒
919                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
920                let address' ≝ bitvector_of_nat seven ((address ÷ eight) + thirty_two) in
921                let t ≝ lookup … seven address' (low_internal_ram s) (zero eight) in
922                let n_bit ≝ set_index … t (modulus address eight) v ? in
923                let memory ≝ insert ? seven address' n_bit (low_internal_ram s) in
924                  set_low_internal_ram s memory
925            ]
926      | CARRY ⇒
927        λcarry: True.
928          let 〈 nu, nl 〉 ≝ split ? four four (get_8051_sfr s SFR_PSW) in
929          let bit_one ≝ get_index … nu one ? in
930          let bit_two ≝ get_index … nu two ? in
931          let bit_three ≝ get_index … nu three ? in
932          let new_psw ≝ [[ v; bit_one ; bit_two; bit_three ]] @@ nl in
933            set_8051_sfr s SFR_PSW new_psw
934      | _ ⇒
935        λother: False.
936          match other in False with
937            [ ]
938      ] (subaddressing_modein … a).
939      ##[##1,2,3,6:
940          nnormalize;
941          nrepeat (napply less_than_or_equal_monotone);
942          napply less_than_or_equal_zero;
943      ##|##4,5:
944          napply (modulus_less_than address eight);
945      ##]
946nqed.
Note: See TracBrowser for help on using the repository browser.