source: Deliverables/D3.1/C-semantics/cerco/Status.ma @ 535

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

Matita interpreter ported to latest version of matita (the one with the tabs). To use, this directory must be copied into the /lib directory in the matita directory.

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