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

Last change on this file since 374 was 362, checked in by sacerdot, 9 years ago

Less ambiguous definitions.

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