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

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

Moved over to standard library.

File size: 34.8 KB
Line 
1(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
2(* Interpret.ma: Operational semantics for the 8051/8052 processor.           *)
3(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
4
5include "ASM.ma".
6include "Arithmetic.ma".
7include "BitVectorTrie.ma".
8
9ndefinition Time ≝ nat.
10
11ninductive SerialBufferType: Type[0] ≝
12  Eight: Byte → SerialBufferType
13| Nine: Bit → Byte → SerialBufferType.
14
15ninductive LineType: Type[0] ≝
16  P1: Byte → LineType
17| P3: Byte → LineType
18| SerialBuffer: SerialBufferType → LineType.
19
20(* What is a continuation, now? *)
21
22ninductive SFR8051: Type[0] ≝
23  SFR_SP: SFR8051
24| SFR_DPL: SFR8051
25| SFR_DPH: SFR8051
26| SFR_PCON: SFR8051
27| SFR_TCON: SFR8051
28| SFR_TMOD: SFR8051
29| SFR_TL0: SFR8051
30| SFR_TL1: SFR8051
31| SFR_TH0: SFR8051
32| SFR_TH1: SFR8051
33| SFR_P1: SFR8051
34| SFR_SCON: SFR8051
35| SFR_SBUF: SFR8051
36| SFR_IE: SFR8051
37| SFR_P3: SFR8051
38| SFR_IP: SFR8051
39| SFR_PSW: SFR8051
40| SFR_ACC_A: SFR8051
41| SFR_ACC_B: SFR8051.
42
43ndefinition sfr_8051_index ≝
44  λs: SFR8051.
45    match s with
46      [ SFR_SP ⇒ 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     
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 ⇒ O
78      | SFR_RCAP2L ⇒ 1
79      | SFR_RCAP2H ⇒ 2
80      | SFR_TL2 ⇒ 3
81      | SFR_TH2 ⇒ 4
82      ].
83
84(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
85(* Processor status.                                                          *)
86(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
87nrecord 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
105nlemma sfr8051_index_19:
106  ∀i: SFR8051.
107    sfr_8051_index i < 19.
108 #i; ncases i; nnormalize; nrepeat (napply le_S_S);
109 napply le_O_n.
110nqed.
111   
112nlemma sfr8052_index_5:
113  ∀i: SFR8052.
114    sfr_8052_index i < 5.
115 #i; ncases i; nnormalize; nrepeat (napply le_S_S);
116 napply le_O_n.
117nqed.
118   
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   
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
153    let old_clock ≝ clock s in
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
162                old_p3_latch
163                old_clock.
164
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
176    let old_clock ≝ clock s in
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
185                b
186                old_clock.
187
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
193      get_index_v … sfr index ?.
194    napply sfr8051_index_19.
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
202      get_index_v … sfr index ?.
203    napply sfr8052_index_5.
204nqed.
205
206ndefinition set_8051_sfr ≝
207  λs: Status.
208  λi: SFR8051.
209  λb: Byte.
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 ≝
219      set_index Byte 19 old_special_function_registers_8051 index b ? in
220    let old_p1_latch ≝ p1_latch s in
221    let old_p3_latch ≝ p3_latch s in
222    let old_clock ≝ clock s in
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
229                old_special_function_registers_8052
230                old_p1_latch
231                old_p3_latch
232                old_clock.
233    napply (sfr8051_index_19 i).
234nqed.
235
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 ≝
249      set_index Byte 5 old_special_function_registers_8052 index b ? in
250    let old_p1_latch ≝ p1_latch s in
251    let old_p3_latch ≝ p3_latch s in
252    let old_clock ≝ clock s in
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
259                new_special_function_registers_8052
260                old_p1_latch
261                old_p3_latch
262                old_clock.
263    napply (sfr8052_index_5 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
275    let old_p1_latch ≝ p1_latch s in
276    let old_p3_latch ≝ p3_latch s in
277    let old_clock ≝ clock s in
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
284                old_special_function_registers_8052
285                old_p1_latch
286                old_p3_latch
287                old_clock.
288               
289ndefinition set_code_memory ≝
290  λs: Status.
291  λr: BitVectorTrie Byte 16.
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
298    let old_p1_latch ≝ p1_latch s in
299    let old_p3_latch ≝ p3_latch s in
300    let old_clock ≝ clock s in
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
307                old_special_function_registers_8052
308                old_p1_latch
309                old_p3_latch
310                old_clock.
311               
312ndefinition set_low_internal_ram ≝
313  λs: Status.
314  λr: BitVectorTrie Byte 7.
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
321    let old_p1_latch ≝ p1_latch s in
322    let old_p3_latch ≝ p3_latch s in
323    let old_clock ≝ clock s in
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
330                old_special_function_registers_8052
331                old_p1_latch
332                old_p3_latch
333                old_clock.
334               
335ndefinition set_high_internal_ram ≝
336  λs: Status.
337  λr: BitVectorTrie Byte 7.
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
347    let old_clock ≝ clock s in
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
356                old_p3_latch
357                old_clock.
358               
359ndefinition set_external_ram ≝
360  λs: Status.
361  λr: BitVectorTrie Byte 16.
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
370    let old_clock ≝ clock s in
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
379                old_p3_latch
380                old_clock.
381               
382ndefinition get_cy_flag ≝
383  λs: Status.
384    let sfr ≝ special_function_registers_8051 s in
385    let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
386      get_index_v bool 8 psw O ?.
387    nnormalize;
388    napply (le_S_S ? ?);
389    ##[ napply le_O_n;
390    ##| nrepeat (napply (le_S_S));
391        //;
392    ##]
393nqed.
394
395ndefinition get_ac_flag ≝
396  λs: Status.
397    let sfr ≝ special_function_registers_8051 s in
398    let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
399      get_index_v bool 8 psw (S O) ?.
400    nnormalize;
401    nrepeat (napply (le_S_S ? ?));
402    napply le_O_n;
403nqed.
404
405ndefinition get_fo_flag ≝
406  λs: Status.
407    let sfr ≝ special_function_registers_8051 s in
408    let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
409      get_index_v bool 8 psw 2 ?.
410    nnormalize;
411    nrepeat (napply (le_S_S ? ?));
412    napply le_O_n;
413nqed.
414
415ndefinition get_rs1_flag ≝
416  λs: Status.
417    let sfr ≝ special_function_registers_8051 s in
418    let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
419      get_index_v bool 8 psw 3 ?.
420    nnormalize;
421    nrepeat (napply (le_S_S ? ?));
422    napply le_O_n;
423nqed.
424
425ndefinition get_rs0_flag ≝
426  λs: Status.
427    let sfr ≝ special_function_registers_8051 s in
428    let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
429      get_index_v bool 8 psw 4 ?.
430    nnormalize;
431    nrepeat (napply (le_S_S ? ?));
432    napply le_O_n;
433nqed.
434
435ndefinition get_ov_flag ≝
436  λs: Status.
437    let sfr ≝ special_function_registers_8051 s in
438    let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
439      get_index_v bool 8 psw 5 ?.
440    nnormalize;
441    nrepeat (napply (le_S_S ? ?));
442    napply le_O_n;
443nqed.
444
445ndefinition get_ud_flag ≝
446  λs: Status.
447    let sfr ≝ special_function_registers_8051 s in
448    let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
449      get_index_v bool 8 psw 6 ?.
450    nnormalize;
451    nrepeat (napply (le_S_S ? ?));
452    napply le_O_n;
453nqed.
454
455ndefinition get_p_flag ≝
456  λs: Status.
457    let sfr ≝ special_function_registers_8051 s in
458    let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
459      get_index_v bool 8 psw 7 ?.
460    nnormalize;
461    nrepeat (napply (le_S_S ? ?));
462    napply le_O_n;
463nqed.
464
465ndefinition set_flags ≝
466  λs: Status.
467  λcy: Bit.
468  λac: option Bit.
469  λov: Bit.
470    let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr s SFR_PSW) in
471    let old_cy ≝ get_index_v… nu O ? in
472    let old_ac ≝ get_index_v… nu 1 ? in
473    let old_fo ≝ get_index_v… nu 2 ? in
474    let old_rs1 ≝ get_index_v… nu 3 ? in
475    let old_rs0 ≝ get_index_v… nl O ? in
476    let old_ov ≝ get_index_v… nl 1 ? in
477    let old_ud ≝ get_index_v… nl 2 ? in
478    let old_p ≝ get_index_v… nl 3 ? in
479    let new_ac ≝ match ac with [ None ⇒ old_ac | Some j ⇒ j ] in
480    let new_psw ≝ [[ old_cy ; new_ac ; old_fo ; old_rs1 ;
481                     old_rs0 ; old_ov ; old_ud ; old_p ]] in
482      set_8051_sfr s SFR_PSW new_psw.
483    ##[##1,2,3,4,5,6,7,8:
484        nnormalize;
485        nrepeat (napply le_S_S);
486        napply (le_O_n);
487    ##]
488nqed.
489
490ndefinition initialise_status ≝
491  let status ≝ mk_Status (Stub Byte 16)                    (* Code mem. *)
492                         (Stub Byte 7)                      (* Low mem.  *)
493                         (Stub Byte 7)                      (* High mem. *)
494                         (Stub Byte 16)                    (* Ext mem.  *)
495                         (zero 16)                         (* PC.       *)
496                         (replicate Byte 19 (zero 8)) (* 8051 SFR. *)
497                         (replicate Byte 5 (zero 8))     (* 8052 SFR. *)
498                         (zero 8)                           (* P1 latch. *)
499                         (zero 8)                           (* P3 latch. *)
500                         O                                      (* Clock.    *)
501  in
502    set_8051_sfr status SFR_SP (bitvector_of_nat 8 7).
503 
504naxiom not_implemented: False.
505 
506ndefinition get_bit_addressable_sfr ≝
507  λs: Status.
508  λn: nat.
509  λb: BitVector n.
510  λl: bool.
511    let address ≝ nat_of_bitvector … b in
512      if (eqb address 128) then
513        ?
514      else if (eqb address 144) then
515        if l then
516          (p1_latch s)
517        else
518          (get_8051_sfr s SFR_P1)
519      else if (eqb address 160) then
520        ?
521      else if (eqb address 176) then
522        if l then
523          (p3_latch s)
524        else
525          (get_8051_sfr s SFR_P3)
526      else if (eqb address 153) then
527        get_8051_sfr s SFR_SBUF
528      else if (eqb address 138) then
529        get_8051_sfr s SFR_TL0
530      else if (eqb address 139) then
531        get_8051_sfr s SFR_TL1
532      else if (eqb address 140) then
533        get_8051_sfr s SFR_TH0
534      else if (eqb address 141) then
535        get_8051_sfr s SFR_TH1
536      else if (eqb address 200) then
537        get_8052_sfr s SFR_T2CON
538      else if (eqb address 202) then
539        get_8052_sfr s SFR_RCAP2L
540      else if (eqb address 203) then
541        get_8052_sfr s SFR_RCAP2H
542      else if (eqb address 204) then
543        get_8052_sfr s SFR_TL2
544      else if (eqb address 205) then
545        get_8052_sfr s SFR_TH2
546      else if (eqb address 135) then
547        get_8051_sfr s SFR_PCON
548      else if (eqb address 136) then
549        get_8051_sfr s SFR_TCON
550      else if (eqb address 137) then
551        get_8051_sfr s SFR_TMOD
552      else if (eqb address 152) then
553        get_8051_sfr s SFR_SCON
554      else if (eqb address 168) then
555        get_8051_sfr s SFR_IE
556      else if (eqb address 184) then
557        get_8051_sfr s SFR_IP
558      else if (eqb address 129) then
559        get_8051_sfr s SFR_SP
560      else if (eqb address 130) then
561        get_8051_sfr s SFR_DPL
562      else if (eqb address 131) then
563        get_8051_sfr s SFR_DPH
564      else if (eqb address 208) then
565        get_8051_sfr s SFR_PSW
566      else if (eqb address 224) then
567        get_8051_sfr s SFR_ACC_A
568      else if (eqb address 240) then
569        get_8051_sfr s SFR_ACC_B
570      else
571        ?.
572      ncases not_implemented.
573nqed.
574
575ndefinition set_bit_addressable_sfr ≝
576  λs: Status.
577  λb: Byte.
578  λv: Byte.
579    let address ≝ nat_of_bitvector … b in
580      if (eqb address 128) then
581        ?
582      else if (eqb address 144) then
583        let status_1 ≝ set_8051_sfr s SFR_P1 v in
584        let status_2 ≝ set_p1_latch s v in
585          status_2
586      else if (eqb address 160) then
587        ?
588      else if (eqb address 176) then
589        let status_1 ≝ set_8051_sfr s SFR_P3 v in
590        let status_2 ≝ set_p3_latch s v in
591          status_2
592      else if (eqb address 153) then
593        set_8051_sfr s SFR_SBUF v
594      else if (eqb address 138) then
595        set_8051_sfr s SFR_TL0 v
596      else if (eqb address 139) then
597        set_8051_sfr s SFR_TL1 v
598      else if (eqb address 140) then
599        set_8051_sfr s SFR_TH0 v
600      else if (eqb address 141) then
601        set_8051_sfr s SFR_TH1 v
602      else if (eqb address 200) then
603        set_8052_sfr s SFR_T2CON v
604      else if (eqb address 202) then
605        set_8052_sfr s SFR_RCAP2L v
606      else if (eqb address 203) then
607        set_8052_sfr s SFR_RCAP2H v
608      else if (eqb address 204) then
609        set_8052_sfr s SFR_TL2 v
610      else if (eqb address 205) then
611        set_8052_sfr s SFR_TH2 v
612      else if (eqb address 135) then
613        set_8051_sfr s SFR_PCON v
614      else if (eqb address 136) then
615        set_8051_sfr s SFR_TCON v
616      else if (eqb address 137) then
617        set_8051_sfr s SFR_TMOD v
618      else if (eqb address 152) then
619        set_8051_sfr s SFR_SCON v
620      else if (eqb address 168) then
621        set_8051_sfr s SFR_IE v
622      else if (eqb address 184) then
623        set_8051_sfr s SFR_IP v
624      else if (eqb address 129) then
625        set_8051_sfr s SFR_SP v
626      else if (eqb address 130) then
627        set_8051_sfr s SFR_DPL v
628      else if (eqb address 131) then
629        set_8051_sfr s SFR_DPH v
630      else if (eqb address 208) then
631        set_8051_sfr s SFR_PSW v
632      else if (eqb address 224) then
633        set_8051_sfr s SFR_ACC_A v
634      else if (eqb address 240) then
635        set_8051_sfr s SFR_ACC_B v
636      else
637        ?.
638      ncases not_implemented.
639nqed.
640
641ndefinition bit_address_of_register ≝
642  λs: Status.
643  λr: BitVector 3.
644    let b ≝ get_index_v … r O ? in
645    let c ≝ get_index_v … r 1 ? in
646    let d ≝ get_index_v … r 2 ? in
647    let 〈 un, ln 〉 ≝ split ? 4 4 (get_8051_sfr s SFR_PSW) in
648    let 〈 r1, r0 〉 ≝ mk_pair … (get_index_v … 4 un 2 ?) (get_index_v … 4 un 3 ?) in
649    let offset ≝
650      if ¬r1 ∧ ¬r0 then
651        O
652      else if ¬r1 ∧ r0 then
653        8
654      else if r1 ∧ r0 then
655        24
656      else
657        16
658    in
659      bitvector_of_nat 7 (offset + (nat_of_bitvector ? [[ false ; b ; c ; d ]])).
660  ##[##1,2,3,4,5:
661      nnormalize;
662      nrepeat (napply le_S_S);
663      napply le_O_n;
664  ##]
665nqed.
666
667ndefinition get_register ≝
668  λs: Status.
669  λr: BitVector 3.
670    let address ≝ bit_address_of_register s r in
671      lookup … address (low_internal_ram s) (zero 8).
672     
673ndefinition set_register ≝
674  λs: Status.
675  λr: BitVector 3.
676  λv: Byte.
677    let address ≝ bit_address_of_register s r in
678    let old_low_internal_ram ≝ low_internal_ram s in
679    let new_low_internal_ram ≝ insert … address v old_low_internal_ram in
680      set_low_internal_ram s new_low_internal_ram.
681     
682ndefinition read_at_stack_pointer ≝
683  λs: Status.
684    let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr s SFR_SP) in
685    let m ≝ get_index_v … nu O ? in
686    let r1 ≝ get_index_v … nu 1 ? in
687    let r2 ≝ get_index_v … nu 2 ? in
688    let r3 ≝ get_index_v … nu 3 ? in
689    let address ≝ [[ r1 ; r2 ; r3 ]] @@ nl in
690    let memory ≝
691      if m then
692        (low_internal_ram s)
693      else
694        (high_internal_ram s)
695    in
696      lookup … address memory (zero 8).
697  ##[##1,2,3,4:
698      nnormalize;
699      nrepeat (napply le_S_S);
700      napply le_O_n;
701  ##]
702nqed.
703
704ndefinition write_at_stack_pointer ≝
705  λs: Status.
706  λv: Byte.
707    let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr s SFR_SP) in
708    let bit_zero ≝ get_index_v… nu O ? in
709    let bit_1 ≝ get_index_v… nu 1 ? in
710    let bit_2 ≝ get_index_v… nu 2 ? in
711    let bit_3 ≝ get_index_v… nu 3 ? in
712      if bit_zero then
713        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
714                              v (low_internal_ram s) in
715          set_low_internal_ram s memory
716      else
717        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
718                              v (high_internal_ram s) in
719          set_high_internal_ram s memory.
720  ##[##1,2,3,4:
721      nnormalize;
722      nrepeat (napply le_S_S);
723      napply le_O_n;
724  ##]
725nqed.
726
727ndefinition set_arg_16: Status → Word → [[ dptr ]] → Status ≝
728  λs,v,a.
729   match a return λx. bool_to_Prop (is_in ? [[ dptr ]] x) → ? with
730     [ DPTR ⇒ λ_:True.
731       let 〈 bu, bl 〉 ≝ split … 8 8 v in
732       let status ≝ set_8051_sfr s SFR_DPH bu in
733       let status ≝ set_8051_sfr status SFR_DPL bl in
734         status
735     | _ ⇒ λK.
736       match K in False with
737       [
738       ]
739     ] (subaddressing_modein … a).
740   
741ndefinition get_arg_16: Status → [[ data16 ]] → Word ≝
742  λs, a.
743    match a return λx. bool_to_Prop (is_in ? [[ data16 ]] x) → ? with
744      [ DATA16 d ⇒ λ_:True. d
745      | _ ⇒ λK.
746        match K in False with
747        [
748        ]
749      ] (subaddressing_modein … a).
750     
751ndefinition get_arg_8: Status → bool → [[ direct ; indirect ; register ;
752                                          acc_a ; acc_b ; data ; acc_dptr ;
753                                          acc_pc ; ext_indirect ;
754                                          ext_indirect_dptr ]] → Byte ≝
755  λs, l, a.
756    match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; register ;
757                                                acc_a ; acc_b ; data ; acc_dptr ;
758                                                acc_pc ; ext_indirect ;
759                                                ext_indirect_dptr ]] x) → ? with
760      [ ACC_A ⇒ λacc_a: True. get_8051_sfr s SFR_ACC_A
761      | ACC_B ⇒ λacc_b: True. get_8051_sfr s SFR_ACC_B
762      | DATA d ⇒ λdata: True. d
763      | REGISTER r ⇒ λregister: True. get_register s r
764      | EXT_INDIRECT_DPTR ⇒
765        λext_indirect_dptr: True.
766          let address ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
767            lookup … 16 address (external_ram s) (zero 8)
768      | EXT_INDIRECT e ⇒
769        λext_indirect: True.
770          let address ≝ get_register s [[ false; false; e ]]  in
771          let padded_address ≝ pad 8 8 address in
772            lookup … 16 padded_address (external_ram s) (zero 8)
773      | ACC_DPTR ⇒
774        λacc_dptr: True.
775          let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
776          let padded_acc ≝ pad 8 8 (get_8051_sfr s SFR_ACC_A) in
777          let 〈 carry, address 〉 ≝ half_add 16 dptr padded_acc in
778            lookup … 16 address (external_ram s) (zero 8)
779      | ACC_PC ⇒
780        λacc_pc: True.
781          let padded_acc ≝ pad 8 8 (get_8051_sfr s SFR_ACC_A) in
782          let 〈 carry, address 〉 ≝ half_add 16 (program_counter s) padded_acc in
783            lookup … 16 address (external_ram s) (zero 8)
784      | DIRECT d ⇒
785        λdirect: True.
786          let 〈 nu, nl 〉 ≝ split … 4 4 d in
787          let bit_1 ≝ get_index_v … nu 1 ? in
788            match bit_1 with
789              [ true ⇒
790                  let 〈 bit_one, three_bits 〉 ≝ split ? 1 3 nu in
791                  let address ≝ three_bits @@ nl in
792                    lookup ? 7 address (low_internal_ram s) (zero 8)
793              | false ⇒ get_bit_addressable_sfr s 8 d l
794              ]
795      | INDIRECT i ⇒
796        λindirect: True.
797          let 〈 nu, nl 〉 ≝ split ? 4 4 (get_register s [[ false; false; i]]) in
798          let 〈 bit_one_v, three_bits 〉 ≝ split ? 1 3 nu in
799          let bit_1 ≝ get_index_v … bit_one_v O ? in
800          match bit_1 with
801            [ true ⇒
802                lookup ? 7 (three_bits @@ nl) (low_internal_ram s) (zero 8)
803            | false ⇒
804                lookup ? 7 (three_bits @@ nl) (high_internal_ram s) (zero 8)
805            ]
806      | _ ⇒ λother.
807        match other in False with [ ]
808      ] (subaddressing_modein … a).
809      ##[##1,2:
810          nnormalize;
811          nrepeat (napply le_S_S);
812          napply le_O_n;
813      ##]
814nqed.
815
816ndefinition set_arg_8: Status → [[ direct ; indirect ; register ;
817                                   acc_a ; acc_b ; ext_indirect ;
818                                   ext_indirect_dptr ]] → Byte → Status ≝
819  λs, a, v.
820    match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; register ;
821                                                acc_a ; acc_b ; ext_indirect ;
822                                                ext_indirect_dptr ]] x) → ? with
823      [ DIRECT d ⇒
824        λdirect: True.
825          let 〈 nu, nl 〉 ≝ split … 4 4 d in
826          let bit_1 ≝ get_index_v … nu 1 ? in
827          let 〈 ignore, three_bits 〉 ≝ split ? 1 3 nu in
828            match bit_1 with
829              [ true ⇒ set_bit_addressable_sfr s d v
830              | false ⇒
831                let memory ≝ insert ? 7 (three_bits @@ nl) v (low_internal_ram s) in
832                  set_low_internal_ram s memory
833              ]
834      | INDIRECT i ⇒
835        λindirect: True.
836          let register ≝ get_register s [[ false; false; i ]] in
837          let 〈nu, nl〉 ≝ split ? 4 4 register in
838          let bit_1 ≝ get_index_v … nu 1 ? in
839          let 〈ignore, three_bits〉 ≝ split ? 1 3 nu in
840            match bit_1 with
841              [ true ⇒
842                let memory ≝ insert … (three_bits @@ nl) v (low_internal_ram s) in
843                  set_low_internal_ram s memory
844              | false ⇒
845                let memory ≝ insert … (three_bits @@ nl) v (high_internal_ram s) in
846                  set_high_internal_ram s memory
847              ]
848      | REGISTER r ⇒ λregister: True. set_register s r v
849      | ACC_A ⇒ λacc_a: True. set_8051_sfr s SFR_ACC_A v
850      | ACC_B ⇒ λacc_b: True. set_8051_sfr s SFR_ACC_B v
851      | EXT_INDIRECT e ⇒
852        λext_indirect: True.
853          let address ≝ get_register s [[ false; false; e ]] in
854          let padded_address ≝ pad 8 8 address in
855          let memory ≝ insert ? 16 padded_address v (external_ram s) in
856            set_external_ram s memory
857      | EXT_INDIRECT_DPTR ⇒
858        λext_indirect_dptr: True.
859          let address ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
860          let memory ≝ insert ? 16 address v (external_ram s) in
861            set_external_ram s memory
862      | _ ⇒
863        λother: False.
864          match other in False with [ ]
865      ] (subaddressing_modein … a).
866      ##[##1,2:
867          nnormalize;
868          nrepeat (napply le_S_S);
869          napply le_O_n
870      ##]
871nqed.
872
873ntheorem modulus_less_than:
874  ∀m,n: nat. (m mod (S n)) < S n.
875 #n m; nnormalize; napply le_S_S;
876 nlapply (le_n n);
877 ngeneralize in ⊢ (?%? → ?(??%?)?);
878 nelim n in ⊢ (∀_:?. ??% → ?(?%??)?)
879  [ nnormalize; #n; napply (less_than_or_equal_b_elim n m); nnormalize
880     [ // | #H K; ninversion K [ #H1; nrewrite < H1; // | #x H1 H2 H3; ndestruct ]##]
881##| nnormalize; #y H1 n H2; napply (less_than_or_equal_b_elim n m); nnormalize
882     [ // | #K; napply H1; ncut (n ≤ S y → n - S m ≤ y); /2/;
883       ncases n; nnormalize; //;
884       #x K1; nlapply (le_S_S_to_le … K1); ngeneralize in match m;
885       nelim x; nnormalize; //; #w1 H m; ncases m; nnormalize; //;
886       #q K2; napply H; /3/]
887nqed.
888
889ndefinition get_arg_1: Status → [[ bit_addr ; n_bit_addr ; carry ]] →
890                       bool → bool ≝
891  λs, a, l.
892    match a return λx. bool_to_Prop (is_in ? [[ bit_addr ;
893                                                 n_bit_addr ;
894                                                 carry ]] x) → ? with
895      [ BIT_ADDR b ⇒
896        λbit_addr: True.
897          let 〈 nu, nl 〉 ≝ split … 4 4 b in
898          let bit_1 ≝ get_index_v … nu 1 ? in
899          let 〈 bit_one_v, three_bits 〉 ≝ split ? 1 3 nu in
900            match bit_1 with
901              [ true ⇒
902                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
903                let d ≝ address ÷ 8 in
904                let m ≝ address mod 8 in
905                let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in
906                let sfr ≝ get_bit_addressable_sfr s ? trans l in
907                  get_index_v … sfr m ?
908              | false ⇒
909                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
910                let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
911                let t ≝ lookup … 7 address' (low_internal_ram s) (zero 8) in
912                  get_index_v … t (modulus address 8) ?
913              ]
914      | N_BIT_ADDR n ⇒
915        λn_bit_addr: True.
916          let 〈 nu, nl 〉 ≝ split … 4 4 n in
917          let bit_1 ≝ get_index_v … nu 1 ? in
918          let 〈 bit_one_v, three_bits 〉 ≝ split ? 1 3 nu in
919            match bit_1 with
920              [ true ⇒
921                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
922                let d ≝ address ÷ 8 in
923                let m ≝ address mod 8 in
924                let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in
925                let sfr ≝ get_bit_addressable_sfr s ? trans l in
926                  ¬(get_index_v … sfr m ?)
927              | false ⇒
928                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
929                let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
930                let trans ≝ lookup … 7 address' (low_internal_ram s) (zero 8) in
931                  ¬(get_index_v … trans (modulus address 8) ?)
932              ]
933      | CARRY ⇒ λcarry: True. get_cy_flag s
934      | _ ⇒ λother.
935        match other in False with [ ]
936      ] (subaddressing_modein … a).
937      ##[##3,6:
938          nnormalize;
939          nrepeat (napply le_S_S);
940          napply le_O_n;
941      ##|##1,2,4,5:
942          napply modulus_less_than;
943      ##]
944nqed.
945     
946ndefinition set_arg_1: Status → [[ bit_addr ; carry ]] →
947                       Bit → Status ≝
948  λs, a, v.
949    match a return λx. bool_to_Prop (is_in ? [[ bit_addr ; carry ]] x) → ? with
950      [ BIT_ADDR b ⇒ λbit_addr: True.
951          let 〈 nu, nl 〉 ≝ split ? 4 4 (get_8051_sfr s SFR_PSW) in
952          let bit_1 ≝ get_index_v … nu 1 ? in
953          let 〈 ignore, three_bits 〉 ≝ split ? 1 3 nu in
954          match bit_1 with
955            [ true ⇒
956                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
957                let d ≝ address ÷ 8 in
958                let m ≝ address mod 8 in
959                let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in
960                let sfr ≝ get_bit_addressable_sfr s ? t true in
961                let new_sfr ≝ set_index … sfr m v ? in
962                  set_bit_addressable_sfr s new_sfr t
963            | false ⇒
964                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
965                let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
966                let t ≝ lookup … 7 address' (low_internal_ram s) (zero 8) in
967                let n_bit ≝ set_index … t (modulus address 8) v ? in
968                let memory ≝ insert ? 7 address' n_bit (low_internal_ram s) in
969                  set_low_internal_ram s memory
970            ]
971      | CARRY ⇒
972        λcarry: True.
973          let 〈 nu, nl 〉 ≝ split ? 4 4 (get_8051_sfr s SFR_PSW) in
974          let bit_1 ≝ get_index_v… nu 1 ? in
975          let bit_2 ≝ get_index_v… nu 2 ? in
976          let bit_3 ≝ get_index_v… nu 3 ? in
977          let new_psw ≝ [[ v; bit_1 ; bit_2; bit_3 ]] @@ nl in
978            set_8051_sfr s SFR_PSW new_psw
979      | _ ⇒
980        λother: False.
981          match other in False with
982            [ ]
983      ] (subaddressing_modein … a).
984      ##[##1,2,3,6:
985          nnormalize;
986          nrepeat (napply le_S_S);
987          napply le_O_n;
988      ##|##4,5:
989          napply modulus_less_than;
990      ##]
991nqed.
992
993ndefinition load_code_memory ≝
994 fold_left_i … (λi,mem,v. insert … (bitvector_of_nat … i) v mem) (Stub Byte 16).
995
996ndefinition load ≝
997 λl,status. set_code_memory status (load_code_memory l).
Note: See TracBrowser for help on using the repository browser.