source: src/ASM/Status.ma @ 762

Last change on this file since 762 was 757, checked in by mulligan, 10 years ago

Lots more fixing to get both front and backends using same conventions and types.

File size: 34.4 KB
Line 
1(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
2(* Interpret.ma: Operational semantics for the 8051/8052 processor.           *)
3(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
4
5include "ASM/ASM.ma".
6include "ASM/Arithmetic.ma".
7include "ASM/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 〉 ≝ 〈 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 ; registr ;
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 ; registr ;
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 ; registr ;
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 ; registr ;
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.