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

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

less axioms

File size: 37.7 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  clock: Time
103}.
104
105naxiom sfr8051_index_nineteen:
106  ∀i: SFR8051.
107    sfr_8051_index i < nineteen.
108   
109naxiom sfr8052_index_five:
110  ∀i: SFR8052.
111    sfr_8052_index i < five.
112   
113ndefinition set_clock ≝
114  λs: Status.
115  λt: Time.
116    let old_code_memory ≝ code_memory s in
117    let old_low_internal_ram ≝ low_internal_ram s in
118    let old_high_internal_ram ≝ high_internal_ram s in
119    let old_external_ram ≝ external_ram s in
120    let old_program_counter ≝ program_counter s in
121    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
122    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
123    let old_p1_latch ≝ p1_latch s in   
124    let old_p3_latch ≝ p3_latch s in
125      mk_Status old_code_memory
126                old_low_internal_ram
127                old_high_internal_ram
128                old_external_ram
129                old_program_counter
130                old_special_function_registers_8051
131                old_special_function_registers_8052
132                old_p1_latch
133                old_p3_latch
134                t.
135   
136ndefinition set_p1_latch ≝
137  λs: Status.
138  λb: Byte.
139    let old_code_memory ≝ code_memory s in
140    let old_low_internal_ram ≝ low_internal_ram s in
141    let old_high_internal_ram ≝ high_internal_ram s in
142    let old_external_ram ≝ external_ram s in
143    let old_program_counter ≝ program_counter s in
144    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
145    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
146    let old_p3_latch ≝ p3_latch s in
147    let old_clock ≝ clock s in
148      mk_Status old_code_memory
149                old_low_internal_ram
150                old_high_internal_ram
151                old_external_ram
152                old_program_counter
153                old_special_function_registers_8051
154                old_special_function_registers_8052
155                b
156                old_p3_latch
157                old_clock.
158
159ndefinition set_p3_latch ≝
160  λs: Status.
161  λb: Byte.
162    let old_code_memory ≝ code_memory s in
163    let old_low_internal_ram ≝ low_internal_ram s in
164    let old_high_internal_ram ≝ high_internal_ram s in
165    let old_external_ram ≝ external_ram s in
166    let old_program_counter ≝ program_counter s in
167    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
168    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
169    let old_p1_latch ≝ p1_latch s in
170    let old_clock ≝ clock s in
171      mk_Status old_code_memory
172                old_low_internal_ram
173                old_high_internal_ram
174                old_external_ram
175                old_program_counter
176                old_special_function_registers_8051
177                old_special_function_registers_8052
178                old_p1_latch
179                b
180                old_clock.
181
182alias id "get_index" = "cic:/matita/ng/Vector/get_index.fix(0,3,2)".
183ndefinition get_8051_sfr ≝
184  λs: Status.
185  λi: SFR8051.
186    let sfr ≝ special_function_registers_8051 s in
187    let index ≝ sfr_8051_index i in
188      get_index … sfr index ?.
189    napply (sfr8051_index_nineteen i).
190nqed.
191
192ndefinition get_8052_sfr ≝
193  λs: Status.
194  λi: SFR8052.
195    let sfr ≝ special_function_registers_8052 s in
196    let index ≝ sfr_8052_index i in
197      get_index … sfr index ?.
198    napply (sfr8052_index_five i).
199nqed.
200
201ndefinition set_8051_sfr ≝
202  λs: Status.
203  λi: SFR8051.
204  λb: Byte.
205    let index ≝ sfr_8051_index i in
206    let old_code_memory ≝ code_memory s in
207    let old_low_internal_ram ≝ low_internal_ram s in
208    let old_high_internal_ram ≝ high_internal_ram s in
209    let old_external_ram ≝ external_ram s in
210    let old_program_counter ≝ program_counter s in
211    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
212    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
213    let new_special_function_registers_8051 ≝
214      cic:/matita/ng/Vector/set_index.fix(0,3,2) Byte nineteen old_special_function_registers_8051 index b ? in
215    let old_p1_latch ≝ p1_latch s in
216    let old_p3_latch ≝ p3_latch s in
217    let old_clock ≝ clock s in
218      mk_Status old_code_memory
219                old_low_internal_ram
220                old_high_internal_ram
221                old_external_ram
222                old_program_counter
223                new_special_function_registers_8051
224                old_special_function_registers_8052
225                old_p1_latch
226                old_p3_latch
227                old_clock.
228    napply (sfr8051_index_nineteen i).
229nqed.
230
231ndefinition set_8052_sfr ≝
232  λs: Status.
233  λi: SFR8052.
234  λb: Byte.
235    let index ≝ sfr_8052_index i in
236    let old_code_memory ≝ code_memory s in
237    let old_low_internal_ram ≝ low_internal_ram s in
238    let old_high_internal_ram ≝ high_internal_ram s in
239    let old_external_ram ≝ external_ram s in
240    let old_program_counter ≝ program_counter s in
241    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
242    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
243    let new_special_function_registers_8052 ≝
244      cic:/matita/ng/Vector/set_index.fix(0,3,2) Byte five old_special_function_registers_8052 index b ? in
245    let old_p1_latch ≝ p1_latch s in
246    let old_p3_latch ≝ p3_latch s in
247    let old_clock ≝ clock s in
248      mk_Status old_code_memory
249                old_low_internal_ram
250                old_high_internal_ram
251                old_external_ram
252                old_program_counter
253                old_special_function_registers_8051
254                new_special_function_registers_8052
255                old_p1_latch
256                old_p3_latch
257                old_clock.
258    napply (sfr8052_index_five i).
259nqed.
260
261ndefinition set_program_counter ≝
262  λs: Status.
263  λw: Word.
264    let old_code_memory ≝ code_memory s in
265    let old_low_internal_ram ≝ low_internal_ram s in
266    let old_high_internal_ram ≝ high_internal_ram s in
267    let old_external_ram ≝ external_ram s in
268    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
269    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
270    let old_p1_latch ≝ p1_latch s in
271    let old_p3_latch ≝ p3_latch s in
272    let old_clock ≝ clock s in
273      mk_Status old_code_memory
274                old_low_internal_ram
275                old_high_internal_ram
276                old_external_ram
277                w
278                old_special_function_registers_8051
279                old_special_function_registers_8052
280                old_p1_latch
281                old_p3_latch
282                old_clock.
283               
284ndefinition set_code_memory ≝
285  λs: Status.
286  λr: BitVectorTrie Byte sixteen.
287    let old_low_internal_ram ≝ low_internal_ram s in
288    let old_high_internal_ram ≝ high_internal_ram s in
289    let old_external_ram ≝ external_ram s in
290    let old_program_counter ≝ program_counter s in
291    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
292    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
293    let old_p1_latch ≝ p1_latch s in
294    let old_p3_latch ≝ p3_latch s in
295    let old_clock ≝ clock s in
296      mk_Status r
297                old_low_internal_ram
298                old_high_internal_ram
299                old_external_ram
300                old_program_counter
301                old_special_function_registers_8051
302                old_special_function_registers_8052
303                old_p1_latch
304                old_p3_latch
305                old_clock.
306               
307ndefinition set_low_internal_ram ≝
308  λs: Status.
309  λr: BitVectorTrie Byte seven.
310    let old_code_memory ≝ code_memory s in
311    let old_high_internal_ram ≝ high_internal_ram s in
312    let old_external_ram ≝ external_ram s in
313    let old_program_counter ≝ program_counter s in
314    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
315    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
316    let old_p1_latch ≝ p1_latch s in
317    let old_p3_latch ≝ p3_latch s in
318    let old_clock ≝ clock s in
319      mk_Status old_code_memory
320                r
321                old_high_internal_ram
322                old_external_ram
323                old_program_counter
324                old_special_function_registers_8051
325                old_special_function_registers_8052
326                old_p1_latch
327                old_p3_latch
328                old_clock.
329               
330ndefinition set_high_internal_ram ≝
331  λs: Status.
332  λr: BitVectorTrie Byte seven.
333    let old_code_memory ≝ code_memory s in
334    let old_low_internal_ram ≝ low_internal_ram s in
335    let old_high_internal_ram ≝ high_internal_ram s in
336    let old_external_ram ≝ external_ram s in
337    let old_program_counter ≝ program_counter s in
338    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
339    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
340    let old_p1_latch ≝ p1_latch s in
341    let old_p3_latch ≝ p3_latch s in
342    let old_clock ≝ clock s in
343      mk_Status old_code_memory
344                old_low_internal_ram
345                r
346                old_external_ram
347                old_program_counter
348                old_special_function_registers_8051
349                old_special_function_registers_8052
350                old_p1_latch
351                old_p3_latch
352                old_clock.
353               
354ndefinition set_external_ram ≝
355  λs: Status.
356  λr: BitVectorTrie Byte sixteen.
357    let old_code_memory ≝ code_memory s in
358    let old_low_internal_ram ≝ low_internal_ram s in
359    let old_high_internal_ram ≝ high_internal_ram s in
360    let old_program_counter ≝ program_counter s in
361    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
362    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
363    let old_p1_latch ≝ p1_latch s in
364    let old_p3_latch ≝ p3_latch s in
365    let old_clock ≝ clock s in
366      mk_Status old_code_memory
367                old_low_internal_ram
368                old_high_internal_ram
369                r
370                old_program_counter
371                old_special_function_registers_8051
372                old_special_function_registers_8052
373                old_p1_latch
374                old_p3_latch
375                old_clock.
376               
377naxiom less_than_or_equal_monotone:
378  ∀m, n: Nat.
379    m ≤ n → S m ≤ S n.
380   
381alias id "get_index" = "cic:/matita/ng/Vector/get_index.fix(0,3,2)".
382               
383ndefinition get_cy_flag ≝
384  λs: Status.
385    let sfr ≝ special_function_registers_8051 s in
386    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
387      get_index Bool eight psw Z ?.
388    nnormalize.
389    napply (less_than_or_equal_monotone ? ?).
390    napply (less_than_or_equal_zero).
391    nrepeat (napply (less_than_or_equal_monotone ? ?)).
392    napply (less_than_or_equal_zero).
393nqed.
394
395ndefinition get_ac_flag ≝
396  λs: Status.
397    let sfr ≝ special_function_registers_8051 s in
398    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
399      get_index Bool eight psw (S Z) ?.
400    nnormalize.
401    nrepeat (napply (less_than_or_equal_monotone ? ?)).
402    napply (less_than_or_equal_zero).
403    nrepeat (napply (less_than_or_equal_monotone ? ?)).
404    napply (less_than_or_equal_zero).
405nqed.
406
407ndefinition get_fo_flag ≝
408  λs: Status.
409    let sfr ≝ special_function_registers_8051 s in
410    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
411      get_index Bool eight psw two ?.
412    nnormalize.
413    nrepeat (napply (less_than_or_equal_monotone ? ?)).
414    napply (less_than_or_equal_zero).
415    nrepeat (napply (less_than_or_equal_monotone ? ?)).
416    napply (less_than_or_equal_zero).
417nqed.
418
419ndefinition get_rs1_flag ≝
420  λs: Status.
421    let sfr ≝ special_function_registers_8051 s in
422    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
423      get_index Bool eight psw three ?.
424    nnormalize.
425    nrepeat (napply (less_than_or_equal_monotone ? ?)).
426    napply (less_than_or_equal_zero).
427    nrepeat (napply (less_than_or_equal_monotone ? ?)).
428    napply (less_than_or_equal_zero).
429nqed.
430
431ndefinition get_rs0_flag ≝
432  λs: Status.
433    let sfr ≝ special_function_registers_8051 s in
434    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
435      get_index Bool eight psw four ?.
436    nnormalize.
437    nrepeat (napply (less_than_or_equal_monotone ? ?)).
438    napply (less_than_or_equal_zero).
439    nrepeat (napply (less_than_or_equal_monotone ? ?)).
440    napply (less_than_or_equal_zero).
441nqed.
442
443ndefinition get_ov_flag ≝
444  λs: Status.
445    let sfr ≝ special_function_registers_8051 s in
446    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
447      get_index Bool eight psw five ?.
448    nnormalize.
449    nrepeat (napply (less_than_or_equal_monotone ? ?)).
450    napply (less_than_or_equal_zero).
451    nrepeat (napply (less_than_or_equal_monotone ? ?)).
452    napply (less_than_or_equal_zero).
453nqed.
454
455ndefinition get_ud_flag ≝
456  λs: Status.
457    let sfr ≝ special_function_registers_8051 s in
458    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
459      get_index Bool eight psw six ?.
460    nnormalize.
461    nrepeat (napply (less_than_or_equal_monotone ? ?)).
462    napply (less_than_or_equal_zero).
463    nrepeat (napply (less_than_or_equal_monotone ? ?)).
464    napply (less_than_or_equal_zero).
465nqed.
466
467ndefinition get_p_flag ≝
468  λs: Status.
469    let sfr ≝ special_function_registers_8051 s in
470    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
471      get_index Bool eight psw seven ?.
472    nnormalize.
473    nrepeat (napply (less_than_or_equal_monotone ? ?)).
474    napply (less_than_or_equal_zero).
475    nrepeat (napply (less_than_or_equal_monotone ? ?)).
476    napply (less_than_or_equal_zero).
477nqed.
478
479ndefinition set_flags ≝
480  λs: Status.
481  λcy: Bit.
482  λac: Maybe Bit.
483  λov: Bit.
484    let 〈 nu, nl 〉 ≝ split … four four (get_8051_sfr s SFR_PSW) in
485    let old_cy ≝ get_index … nu Z ? in
486    let old_ac ≝ get_index … nu one ? in
487    let old_fo ≝ get_index … nu two ? in
488    let old_rs1 ≝ get_index … nu three ? in
489    let old_rs0 ≝ get_index … nl Z ? in
490    let old_ov ≝ get_index … nl one ? in
491    let old_ud ≝ get_index … nl two ? in
492    let old_p ≝ get_index … nl three ? in
493    let new_ac ≝ match ac with [ Nothing ⇒ old_ac | Just j ⇒ j ] in
494    let new_psw ≝ [[ old_cy ; new_ac ; old_fo ; old_rs1 ;
495                     old_rs0 ; old_ov ; old_ud ; old_p ]] in
496      set_8051_sfr s SFR_PSW new_psw.
497    ##[##1,2,3,4,5,6,7,8:
498        nnormalize;
499        nrepeat (napply less_than_or_equal_monotone);
500        napply (less_than_or_equal_zero);
501    ##]
502nqed.
503
504ndefinition initialise_status ≝
505  let status ≝ mk_Status (Stub Byte sixteen)                    (* Code mem. *)
506                         (Stub Byte seven)                      (* Low mem.  *)
507                         (Stub Byte seven)                      (* High mem. *)
508                         (Stub Byte sixteen)                    (* Ext mem.  *)
509                         (zero sixteen)                         (* PC.       *)
510                         (replicate Byte nineteen (zero eight)) (* 8051 SFR. *)
511                         (replicate Byte five (zero eight))     (* 8052 SFR. *)
512                         (zero eight)                           (* P1 latch. *)
513                         (zero eight)                           (* P3 latch. *)
514                         Z                                      (* Clock.    *)
515  in
516    set_program_counter status (bitvector_of_nat sixteen seven).
517 
518naxiom not_implemented: False.
519 
520include "Arithmetic.ma".
521 
522ndefinition get_bit_addressable_sfr ≝
523  λs: Status.
524  λn: Nat.
525  λb: BitVector n.
526  λl: Bool.
527    let address ≝ nat_of_bitvector … b in
528      if (eq_n address one_hundred_and_twenty_eight) then
529        ?
530      else if (eq_n address one_hundred_and_forty_four) then
531        if l then
532          (p1_latch s)
533        else
534          (get_8051_sfr s SFR_P1)
535      else if (eq_n address one_hundred_and_sixty) then
536        ?
537      else if (eq_n address one_hundred_and_seventy_six) then
538        if l then
539          (p3_latch s)
540        else
541          (get_8051_sfr s SFR_P3)
542      else if (eq_n address one_hundred_and_fifty_three) then
543        get_8051_sfr s SFR_SBUF
544      else if (eq_n address one_hundred_and_thirty_eight) then
545        get_8051_sfr s SFR_TL0
546      else if (eq_n address one_hundred_and_thirty_nine) then
547        get_8051_sfr s SFR_TL1
548      else if (eq_n address one_hundred_and_forty) then
549        get_8051_sfr s SFR_TH0
550      else if (eq_n address one_hundred_and_forty_one) then
551        get_8051_sfr s SFR_TH1
552      else if (eq_n address two_hundred) then
553        get_8052_sfr s SFR_T2CON
554      else if (eq_n address two_hundred_and_two) then
555        get_8052_sfr s SFR_RCAP2L
556      else if (eq_n address two_hundred_and_three) then
557        get_8052_sfr s SFR_RCAP2H
558      else if (eq_n address two_hundred_and_four) then
559        get_8052_sfr s SFR_TL2
560      else if (eq_n address two_hundred_and_five) then
561        get_8052_sfr s SFR_TH2
562      else if (eq_n address one_hundred_and_thirty_five) then
563        get_8051_sfr s SFR_PCON
564      else if (eq_n address one_hundred_and_thirty_six) then
565        get_8051_sfr s SFR_TCON
566      else if (eq_n address one_hundred_and_thirty_seven) then
567        get_8051_sfr s SFR_TMOD
568      else if (eq_n address one_hundred_and_fifty_two) then
569        get_8051_sfr s SFR_SCON
570      else if (eq_n address one_hundred_and_sixty_eight) then
571        get_8051_sfr s SFR_IE
572      else if (eq_n address one_hundred_and_eighty_four) then
573        get_8051_sfr s SFR_IP
574      else if (eq_n address one_hundred_and_twenty_nine) then
575        get_8051_sfr s SFR_SP
576      else if (eq_n address one_hundred_and_thirty) then
577        get_8051_sfr s SFR_DPL
578      else if (eq_n address one_hundred_and_thirty_one) then
579        get_8051_sfr s SFR_DPH
580      else if (eq_n address two_hundred_and_eight) then
581        get_8051_sfr s SFR_PSW
582      else if (eq_n address two_hundred_and_twenty_four) then
583        get_8051_sfr s SFR_ACC_A
584      else if (eq_n address two_hundred_and_forty) then
585        get_8051_sfr s SFR_ACC_B
586      else
587        ?.
588      ncases not_implemented.
589nqed.
590
591ndefinition set_bit_addressable_sfr ≝
592  λs: Status.
593  λb: Byte.
594  λv: Byte.
595    let address ≝ nat_of_bitvector … b in
596      if (eq_n address one_hundred_and_twenty_eight) then
597        ?
598      else if (eq_n address one_hundred_and_forty_four) then
599        let status_1 ≝ set_8051_sfr s SFR_P1 v in
600        let status_2 ≝ set_p1_latch s v in
601          status_2
602      else if (eq_n address one_hundred_and_sixty) then
603        ?
604      else if (eq_n address one_hundred_and_seventy_six) then
605        let status_1 ≝ set_8051_sfr s SFR_P3 v in
606        let status_2 ≝ set_p3_latch s v in
607          status_2
608      else if (eq_n address one_hundred_and_fifty_three) then
609        set_8051_sfr s SFR_SBUF v
610      else if (eq_n address one_hundred_and_thirty_eight) then
611        set_8051_sfr s SFR_TL0 v
612      else if (eq_n address one_hundred_and_thirty_nine) then
613        set_8051_sfr s SFR_TL1 v
614      else if (eq_n address one_hundred_and_forty) then
615        set_8051_sfr s SFR_TH0 v
616      else if (eq_n address one_hundred_and_forty_one) then
617        set_8051_sfr s SFR_TH1 v
618      else if (eq_n address two_hundred) then
619        set_8052_sfr s SFR_T2CON v
620      else if (eq_n address two_hundred_and_two) then
621        set_8052_sfr s SFR_RCAP2L v
622      else if (eq_n address two_hundred_and_three) then
623        set_8052_sfr s SFR_RCAP2H v
624      else if (eq_n address two_hundred_and_four) then
625        set_8052_sfr s SFR_TL2 v
626      else if (eq_n address two_hundred_and_five) then
627        set_8052_sfr s SFR_TH2 v
628      else if (eq_n address one_hundred_and_thirty_five) then
629        set_8051_sfr s SFR_PCON v
630      else if (eq_n address one_hundred_and_thirty_six) then
631        set_8051_sfr s SFR_TCON v
632      else if (eq_n address one_hundred_and_thirty_seven) then
633        set_8051_sfr s SFR_TMOD v
634      else if (eq_n address one_hundred_and_fifty_two) then
635        set_8051_sfr s SFR_SCON v
636      else if (eq_n address one_hundred_and_sixty_eight) then
637        set_8051_sfr s SFR_IE v
638      else if (eq_n address one_hundred_and_eighty_four) then
639        set_8051_sfr s SFR_IP v
640      else if (eq_n address one_hundred_and_twenty_nine) then
641        set_8051_sfr s SFR_SP v
642      else if (eq_n address one_hundred_and_thirty) then
643        set_8051_sfr s SFR_DPL v
644      else if (eq_n address one_hundred_and_thirty_one) then
645        set_8051_sfr s SFR_DPH v
646      else if (eq_n address two_hundred_and_eight) then
647        set_8051_sfr s SFR_PSW v
648      else if (eq_n address two_hundred_and_twenty_four) then
649        set_8051_sfr s SFR_ACC_A v
650      else if (eq_n address two_hundred_and_forty) then
651        set_8051_sfr s SFR_ACC_B v
652      else
653        ?.
654      ncases not_implemented.
655nqed.
656
657ndefinition bit_address_of_register ≝
658  λs: Status.
659  λr: BitVector three.
660    let b ≝ get_index_bv ? r Z ? in
661    let c ≝ get_index_bv ? r one ? in
662    let d ≝ get_index_bv ? r two ? in
663    let 〈 un, ln 〉 ≝ split ? four four (get_8051_sfr s SFR_PSW) in
664    let 〈 r1, r0 〉 ≝ mk_Cartesian … (get_index_bv four un two ?) (get_index_bv four un three ?) in
665    let offset ≝
666      if conjunction (negation r1) (negation r0) then
667        Z
668      else if conjunction (negation r1) r0 then
669        eight
670      else if conjunction r1 r0 then
671        twenty_four
672      else
673        sixteen
674    in
675      bitvector_of_nat seven (offset + (nat_of_bitvector ? [[ false ; b ; c ; d ]])).
676  ##[##1,2,3,4,5:
677      nnormalize;
678      nrepeat (napply less_than_or_equal_monotone);
679      napply less_than_or_equal_zero;
680  ##]
681nqed.
682
683ndefinition get_register ≝
684  λs: Status.
685  λr: BitVector three.
686    let address ≝ bit_address_of_register s r in
687      lookup … address (low_internal_ram s) (zero eight).
688     
689ndefinition set_register ≝
690  λs: Status.
691  λr: BitVector three.
692  λv: Byte.
693    let address ≝ bit_address_of_register s r in
694    let old_low_internal_ram ≝ low_internal_ram s in
695    let new_low_internal_ram ≝ insert … address v old_low_internal_ram in
696      set_low_internal_ram s new_low_internal_ram.
697     
698ndefinition read_at_stack_pointer ≝
699  λs: Status.
700    let 〈 nu, nl 〉 ≝ split … four four (get_8051_sfr s SFR_SP) in
701    let m ≝ get_index_bv … nu Z ? in
702    let r1 ≝ get_index_bv … nu one ? in
703    let r2 ≝ get_index_bv … nu two ? in
704    let r3 ≝ get_index_bv … nu three ? in
705    let address ≝ [[ r1 ; r2 ; r3 ]] @@ nl in
706    let memory ≝
707      if m then
708        (low_internal_ram s)
709      else
710        (high_internal_ram s)
711    in
712      lookup … address memory (zero eight).
713    ##[##1,2,3,4:
714        nnormalize;
715        nrepeat (napply less_than_or_equal_monotone);
716        napply less_than_or_equal_zero;
717    ##]
718nqed.
719
720ndefinition write_at_stack_pointer ≝
721  λs: Status.
722  λv: Byte.
723    let 〈 nu, nl 〉 ≝ split … four four (get_8051_sfr s SFR_SP) in
724    let bit_zero ≝ get_index … nu Z ? in
725    let bit_one ≝ get_index … nu one ? in
726    let bit_two ≝ get_index … nu two ? in
727    let bit_three ≝ get_index … nu three ? in
728      if bit_zero then
729        let memory ≝ insert … ([[ bit_one ; bit_two ; bit_three ]] @@ nl)
730                              v (low_internal_ram s) in
731          set_low_internal_ram s memory
732      else
733        let memory ≝ insert … ([[ bit_one ; bit_two ; bit_three ]] @@ nl)
734                              v (high_internal_ram s) in
735          set_high_internal_ram s memory.
736    ##[##1,2,3,4:
737        nnormalize;
738        nrepeat (napply less_than_or_equal_monotone);
739        napply less_than_or_equal_zero;
740    ##]
741nqed.
742
743ndefinition set_arg_16: Status → Word → [[ dptr ]] → Status ≝
744  λs,v,a.
745   match a return λx. bool_to_Prop (is_in ? [[ dptr ]] x) → ? with
746     [ DPTR ⇒ λ_:True.
747       let 〈 bu, bl 〉 ≝ split … eight eight v in
748       let status ≝ set_8051_sfr s SFR_DPH bu in
749       let status ≝ set_8051_sfr status SFR_DPL bl in
750         status
751     | _ ⇒ λK.
752       match K in False with
753       [
754       ]
755     ] (subaddressing_modein … a).
756   
757ndefinition get_arg_16: Status → [[ data16 ]] → Word ≝
758  λs, a.
759    match a return λx. bool_to_Prop (is_in ? [[ data16 ]] x) → ? with
760      [ DATA16 d ⇒ λ_:True. d
761      | _ ⇒ λK.
762        match K in False with
763        [
764        ]
765      ] (subaddressing_modein … a).
766     
767ndefinition get_arg_8: Status → Bool → [[ direct ; indirect ; register ;
768                                          acc_a ; acc_b ; data ; acc_dptr ;
769                                          acc_pc ; ext_indirect ;
770                                          ext_indirect_dptr ]] → Byte ≝
771  λs, l, a.
772    match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; register ;
773                                                acc_a ; acc_b ; data ; acc_dptr ;
774                                                acc_pc ; ext_indirect ;
775                                                ext_indirect_dptr ]] x) → ? with
776      [ ACC_A ⇒ λacc_a: True. get_8051_sfr s SFR_ACC_A
777      | ACC_B ⇒ λacc_b: True. get_8051_sfr s SFR_ACC_B
778      | DATA d ⇒ λdata: True. d
779      | REGISTER r ⇒ λregister: True. get_register s r
780      | EXT_INDIRECT_DPTR ⇒
781        λext_indirect_dptr: True.
782          let address ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
783            lookup … sixteen address (external_ram s) (zero eight)
784      | EXT_INDIRECT e ⇒
785        λext_indirect: True.
786          let address ≝ get_register s [[ false; false; e ]]  in
787          let padded_address ≝ pad eight eight address in
788            lookup … sixteen padded_address (external_ram s) (zero eight)
789      | ACC_DPTR ⇒
790        λacc_dptr: True.
791          let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
792          let padded_acc ≝ pad eight eight (get_8051_sfr s SFR_ACC_A) in
793          let 〈 carry, address 〉 ≝ half_add sixteen dptr padded_acc in
794            lookup … sixteen address (external_ram s) (zero eight)
795      | ACC_PC ⇒
796        λacc_pc: True.
797          let padded_acc ≝ pad eight eight (get_8051_sfr s SFR_ACC_A) in
798          let 〈 carry, address 〉 ≝ half_add sixteen (program_counter s) padded_acc in
799            lookup … sixteen address (external_ram s) (zero eight)
800      | DIRECT d ⇒
801        λdirect: True.
802          let 〈 nu, nl 〉 ≝ split … four four d in
803          let bit_one ≝ get_index_bv … nu one ? in
804            match bit_one with
805              [ true ⇒
806                  let 〈 bit_one, three_bits 〉 ≝ split ? one three nu in
807                  let address ≝ three_bits @@ nl in
808                    lookup ? seven address (low_internal_ram s) (zero eight)
809              | false ⇒ get_bit_addressable_sfr s eight d l
810              ]
811      | INDIRECT i ⇒
812        λindirect: True.
813          let 〈 nu, nl 〉 ≝ split ? four four (get_register s [[ false; false; i]]) in
814          let 〈 bit_one_v, three_bits 〉 ≝ split ? one three nu in
815          let bit_one ≝ get_index_bv … bit_one_v Z ? in
816          match bit_one with
817            [ true ⇒
818                lookup ? seven (three_bits @@ nl) (low_internal_ram s) (zero eight)
819            | false ⇒
820                lookup ? seven (three_bits @@ nl) (high_internal_ram s) (zero eight)
821            ]
822      | _ ⇒ λother.
823        match other in False with [ ]
824      ] (subaddressing_modein … a).
825      ##[##1,2:
826          nnormalize;
827          nrepeat (napply less_than_or_equal_monotone);
828          napply less_than_or_equal_zero;
829      ##]
830nqed.
831
832ndefinition set_arg_8: Status → [[ direct ; indirect ; register ;
833                                   acc_a ; acc_b ; ext_indirect ;
834                                   ext_indirect_dptr ]] → Byte → Status ≝
835  λs, a, v.
836    match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; register ;
837                                                acc_a ; acc_b ; ext_indirect ;
838                                                ext_indirect_dptr ]] x) → ? with
839      [ DIRECT d ⇒
840        λdirect: True.
841          let 〈 nu, nl 〉 ≝ split … four four d in
842          let bit_one ≝ get_index_bv … nu one ? in
843          let 〈 ignore, three_bits 〉 ≝ split ? one three nu in
844            match bit_one with
845              [ true ⇒ set_bit_addressable_sfr s d v
846              | false ⇒
847                let memory ≝ insert ? seven (three_bits @@ nl) v (low_internal_ram s) in
848                  set_low_internal_ram s memory
849              ]
850      | INDIRECT i ⇒
851        λindirect: True.
852          let register ≝ get_register s [[ false; false; i ]] in
853          let 〈 nu, nl 〉 ≝ split ? four four register in
854          let bit_one ≝ get_index_bv ? nu one ? in
855          let 〈 ignore, three_bits 〉 ≝ split ? one three nu in
856          match bit_one with
857            [ true ⇒
858              let memory ≝ insert … (three_bits @@ nl) v (low_internal_ram s) in
859                set_low_internal_ram s memory
860            | false ⇒
861              let memory ≝ insert … (three_bits @@ nl) v (high_internal_ram s) in
862                set_high_internal_ram s memory
863            ]
864      | REGISTER r ⇒ λregister: True. set_register s r v
865      | ACC_A ⇒ λacc_a: True. set_8051_sfr s SFR_ACC_A v
866      | ACC_B ⇒ λacc_b: True. set_8051_sfr s SFR_ACC_B v
867      | EXT_INDIRECT e ⇒
868        λext_indirect: True.
869          let address ≝ get_register s [[ false; false; e ]] in
870          let padded_address ≝ pad eight eight address in
871          let memory ≝ insert ? sixteen padded_address v (external_ram s) in
872            set_external_ram s memory
873      | EXT_INDIRECT_DPTR ⇒
874        λext_indirect_dptr: True.
875          let address ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
876          let memory ≝ insert ? sixteen address v (external_ram s) in
877            set_external_ram s memory
878      | _ ⇒
879        λother: False.
880          match other in False with [ ]
881      ] (subaddressing_modein … a).
882      ##[##1,2:
883          nnormalize;
884          nrepeat (napply less_than_or_equal_monotone);
885          napply less_than_or_equal_zero
886      ##]
887nqed.
888
889naxiom modulus_less_than:
890  ∀m,n: Nat.
891    (m mod n) < n.
892
893ndefinition get_arg_1: Status → [[ bit_addr ; n_bit_addr ; carry ]] →
894                       Bool → Bool ≝
895  λs, a, l.
896    match a return λx. bool_to_Prop (is_in ? [[ bit_addr ;
897                                                 n_bit_addr ;
898                                                 carry ]] x) → ? with
899      [ BIT_ADDR b ⇒
900        λbit_addr: True.
901          let 〈 nu, nl 〉 ≝ split … four four b in
902          let bit_one ≝ get_index_bv … nu one ? in
903          let 〈 bit_one_v, three_bits 〉 ≝ split ? one three nu in
904            match bit_one with
905              [ true ⇒
906                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
907                let d ≝ address ÷ eight in
908                let m ≝ address mod eight in
909                let trans ≝ bitvector_of_nat eight ((d * eight) + one_hundred_and_twenty_eight) in
910                let sfr ≝ get_bit_addressable_sfr s ? trans l in
911                  get_index_bv ? sfr m ?
912              | false ⇒
913                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
914                let address' ≝ bitvector_of_nat seven ((address ÷ eight) + thirty_two) in
915                let t ≝ lookup … seven address' (low_internal_ram s) (zero eight) in
916                  get_index_bv ? t (modulus address eight) ?
917              ]
918      | N_BIT_ADDR n ⇒
919        λn_bit_addr: True.
920          let 〈 nu, nl 〉 ≝ split … four four n in
921          let bit_one ≝ get_index_bv … nu one ? in
922          let 〈 bit_one_v, three_bits 〉 ≝ split ? one three nu in
923            match bit_one with
924              [ true ⇒
925                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
926                let d ≝ address ÷ eight in
927                let m ≝ address mod eight in
928                let trans ≝ bitvector_of_nat eight ((d * eight) + one_hundred_and_twenty_eight) in
929                let sfr ≝ get_bit_addressable_sfr s ? trans l in
930                  negation (get_index_bv ? sfr m ?)
931              | false ⇒
932                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
933                let address' ≝ bitvector_of_nat seven ((address ÷ eight) + thirty_two) in
934                let trans ≝ lookup … seven address' (low_internal_ram s) (zero eight) in
935                  negation (get_index_bv ? trans (modulus address eight) ?)
936              ]
937      | CARRY ⇒ λcarry: True. get_cy_flag s
938      | _ ⇒ λother.
939        match other in False with [ ]
940      ] (subaddressing_modein … a).
941      ##[##3,6:
942          nnormalize;
943          nrepeat (napply less_than_or_equal_monotone);
944          napply less_than_or_equal_zero;
945      ##|##1,2,4,5:
946          napply modulus_less_than;
947      ##]
948nqed.
949     
950ndefinition set_arg_1: Status → [[ bit_addr ; carry ]] →
951                       Bit → Status ≝
952  λs, a, v.
953    match a return λx. bool_to_Prop (is_in ? [[ bit_addr ; carry ]] x) → ? with
954      [ BIT_ADDR b ⇒ λbit_addr: True.
955          let 〈 nu, nl 〉 ≝ split ? four four (get_8051_sfr s SFR_PSW) in
956          let bit_one ≝ get_index_bv ? nu one ? in
957          let 〈 ignore, three_bits 〉 ≝ split ? one three nu in
958          match bit_one with
959            [ true ⇒
960                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
961                let d ≝ address ÷ eight in
962                let m ≝ address mod eight in
963                let t ≝ bitvector_of_nat eight ((d * eight) + one_hundred_and_twenty_eight) in
964                let sfr ≝ get_bit_addressable_sfr s ? t true in
965                let new_sfr ≝ set_index … sfr m v ? in
966                  set_bit_addressable_sfr s new_sfr t
967            | false ⇒
968                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
969                let address' ≝ bitvector_of_nat seven ((address ÷ eight) + thirty_two) in
970                let t ≝ lookup … seven address' (low_internal_ram s) (zero eight) in
971                let n_bit ≝ set_index … t (modulus address eight) v ? in
972                let memory ≝ insert ? seven address' n_bit (low_internal_ram s) in
973                  set_low_internal_ram s memory
974            ]
975      | CARRY ⇒
976        λcarry: True.
977          let 〈 nu, nl 〉 ≝ split ? four four (get_8051_sfr s SFR_PSW) in
978          let bit_one ≝ get_index … nu one ? in
979          let bit_two ≝ get_index … nu two ? in
980          let bit_three ≝ get_index … nu three ? in
981          let new_psw ≝ [[ v; bit_one ; bit_two; bit_three ]] @@ nl in
982            set_8051_sfr s SFR_PSW new_psw
983      | _ ⇒
984        λother: False.
985          match other in False with
986            [ ]
987      ] (subaddressing_modein … a).
988      ##[##1,2,3,6:
989          nnormalize;
990          nrepeat (napply less_than_or_equal_monotone);
991          napply less_than_or_equal_zero;
992      ##|##4,5:
993          napply (modulus_less_than address eight);
994      ##]
995nqed.
996
997ndefinition load_code_memory ≝
998 fold_left_i … (λi,mem,v. insert … (bitvector_of_nat … i) v mem) (Stub Byte sixteen).
999
1000ndefinition load ≝
1001 λl,status. set_code_memory status (load_code_memory l).
Note: See TracBrowser for help on using the repository browser.