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

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

Added bit address lookup for registers.

File size: 21.6 KB
Line 
1(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
2(* Interpret.ma: Operational semantics for the 8051/8052 processor.           *)
3(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
4
5(* include "ASM.ma". *)
6include "Arithmetic.ma".
7include "BitVectorTrie.ma".
8
9ndefinition Time ≝ Nat.
10
11ninductive SerialBufferType: Type[0] ≝
12  Eight: Byte → SerialBufferType
13| Nine: Bit → Byte → SerialBufferType.
14
15ninductive LineType: Type[0] ≝
16  P1: Byte → LineType
17| P3: Byte → LineType
18| SerialBuffer: SerialBufferType → LineType.
19
20(* What is a continuation, now? *)
21
22ninductive SFR8051: Type[0] ≝
23  SFR_SP: SFR8051
24| SFR_DPL: SFR8051
25| SFR_DPH: SFR8051
26| SFR_PCON: SFR8051
27| SFR_TCON: SFR8051
28| SFR_TMOD: SFR8051
29| SFR_TL0: SFR8051
30| SFR_TL1: SFR8051
31| SFR_TH0: SFR8051
32| SFR_TH1: SFR8051
33| SFR_P1: SFR8051
34| SFR_SCON: SFR8051
35| SFR_SBUF: SFR8051
36| SFR_IE: SFR8051
37| SFR_P3: SFR8051
38| SFR_IP: SFR8051
39| SFR_PSW: SFR8051
40| SFR_ACC_A: SFR8051
41| SFR_ACC_B: SFR8051.
42
43ndefinition sfr_8051_index ≝
44  λs: SFR8051.
45    match s with
46      [ SFR_SP ⇒ Z
47      | SFR_DPL ⇒ S Z
48      | SFR_DPH ⇒ two
49      | SFR_PCON ⇒ three
50      | SFR_TCON ⇒ four
51      | SFR_TMOD ⇒ five
52      | SFR_TL0 ⇒ six
53      | SFR_TL1 ⇒ seven
54      | SFR_TH0 ⇒ eight
55      | SFR_TH1 ⇒ nine
56      | SFR_P1 ⇒ ten
57      | SFR_SCON ⇒ eleven
58      | SFR_SBUF ⇒ twelve
59      | SFR_IE ⇒ thirteen
60      | SFR_P3 ⇒ fourteen
61      | SFR_IP ⇒ fifteen
62      | SFR_PSW ⇒ sixteen
63      | SFR_ACC_A ⇒ seventeen
64      | SFR_ACC_B ⇒ eighteen
65      ].
66     
67ninductive SFR8052: Type[0] ≝
68   SFR_T2CON: SFR8052
69|  SFR_RCAP2L: SFR8052
70|  SFR_RCAP2H: SFR8052
71|  SFR_TL2: SFR8052
72|  SFR_TH2: SFR8052.
73
74ndefinition sfr_8052_index ≝
75  λs: SFR8052.
76    match s with
77      [ SFR_T2CON ⇒ Z
78      | SFR_RCAP2L ⇒ S Z
79      | SFR_RCAP2H ⇒ two
80      | SFR_TL2 ⇒ three
81      | SFR_TH2 ⇒ four
82      ].
83
84(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
85(* Processor status.                                                          *)
86(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
87nrecord Status: Type[0] ≝
88{
89  code_memory: BitVectorTrie Byte sixteen;
90  low_internal_ram: BitVectorTrie Byte seven;
91  high_internal_ram: BitVectorTrie Byte seven;
92  external_ram: BitVectorTrie Byte sixteen;
93 
94  program_counter: Word;
95 
96  special_function_registers_8051: Vector Byte nineteen;
97  special_function_registers_8052: Vector Byte five;
98 
99  p1_latch: Byte;
100  p3_latch: Byte
101}.
102
103naxiom sfr8051_index_nineteen:
104  ∀i: SFR8051.
105    sfr_8051_index i < nineteen.
106   
107naxiom sfr8052_index_five:
108  ∀i: SFR8052.
109    sfr_8052_index i < five.
110   
111ndefinition set_p1_latch ≝
112  λs: Status.
113  λb: Byte.
114    let old_code_memory ≝ code_memory s in
115    let old_low_internal_ram ≝ low_internal_ram s in
116    let old_high_internal_ram ≝ high_internal_ram s in
117    let old_external_ram ≝ external_ram s in
118    let old_program_counter ≝ program_counter s in
119    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
120    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
121    let old_p3_latch ≝ p3_latch s in
122      mk_Status old_code_memory
123                old_low_internal_ram
124                old_high_internal_ram
125                old_external_ram
126                old_program_counter
127                old_special_function_registers_8051
128                old_special_function_registers_8052
129                b
130                old_p3_latch.
131
132ndefinition set_p3_latch ≝
133  λs: Status.
134  λb: Byte.
135    let old_code_memory ≝ code_memory s in
136    let old_low_internal_ram ≝ low_internal_ram s in
137    let old_high_internal_ram ≝ high_internal_ram s in
138    let old_external_ram ≝ external_ram s in
139    let old_program_counter ≝ program_counter s in
140    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
141    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
142    let old_p1_latch ≝ p1_latch s in
143      mk_Status old_code_memory
144                old_low_internal_ram
145                old_high_internal_ram
146                old_external_ram
147                old_program_counter
148                old_special_function_registers_8051
149                old_special_function_registers_8052
150                old_p1_latch
151                b.
152
153ndefinition get_8051_sfr ≝
154  λs: Status.
155  λi: SFR8051.
156    let sfr ≝ special_function_registers_8051 s in
157    let index ≝ sfr_8051_index i in
158      get_index … sfr index ?.
159    napply (sfr8051_index_nineteen i).
160nqed.
161
162ndefinition get_8052_sfr ≝
163  λs: Status.
164  λi: SFR8052.
165    let sfr ≝ special_function_registers_8052 s in
166    let index ≝ sfr_8052_index i in
167      get_index … sfr index ?.
168    napply (sfr8052_index_five i).
169nqed.
170
171ndefinition set_8051_sfr ≝
172  λs: Status.
173  λi: SFR8051.
174  λb: Byte.
175    let index ≝ sfr_8051_index i in
176    let old_code_memory ≝ code_memory s in
177    let old_low_internal_ram ≝ low_internal_ram s in
178    let old_high_internal_ram ≝ high_internal_ram s in
179    let old_external_ram ≝ external_ram s in
180    let old_program_counter ≝ program_counter s in
181    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
182    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
183    let new_special_function_registers_8051 ≝
184      cic:/matita/ng/Vector/set_index.fix(0,3,2) Byte nineteen old_special_function_registers_8051 index b ? in
185    let old_p1_latch ≝ p1_latch s in
186    let old_p3_latch ≝ p3_latch s in
187      mk_Status old_code_memory
188                old_low_internal_ram
189                old_high_internal_ram
190                old_external_ram
191                old_program_counter
192                new_special_function_registers_8051
193                old_special_function_registers_8052
194                old_p1_latch
195                old_p3_latch.
196    napply (sfr8051_index_nineteen i).
197nqed.
198
199ndefinition set_8052_sfr ≝
200  λs: Status.
201  λi: SFR8052.
202  λb: Byte.
203    let index ≝ sfr_8052_index i in
204    let old_code_memory ≝ code_memory s in
205    let old_low_internal_ram ≝ low_internal_ram s in
206    let old_high_internal_ram ≝ high_internal_ram s in
207    let old_external_ram ≝ external_ram s in
208    let old_program_counter ≝ program_counter s in
209    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
210    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
211    let new_special_function_registers_8052 ≝
212      cic:/matita/ng/Vector/set_index.fix(0,3,2) Byte five old_special_function_registers_8052 index b ? in
213    let old_p1_latch ≝ p1_latch s in
214    let old_p3_latch ≝ p3_latch s in
215      mk_Status old_code_memory
216                old_low_internal_ram
217                old_high_internal_ram
218                old_external_ram
219                old_program_counter
220                old_special_function_registers_8051
221                new_special_function_registers_8052
222                old_p1_latch
223                old_p3_latch.
224    napply (sfr8052_index_five i).
225nqed.
226
227ndefinition set_program_counter ≝
228  λs: Status.
229  λw: Word.
230    let old_code_memory ≝ code_memory s in
231    let old_low_internal_ram ≝ low_internal_ram s in
232    let old_high_internal_ram ≝ high_internal_ram s in
233    let old_external_ram ≝ external_ram s in
234    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
235    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
236    let old_p1_latch ≝ p1_latch s in
237    let old_p3_latch ≝ p3_latch s in
238      mk_Status old_code_memory
239                old_low_internal_ram
240                old_high_internal_ram
241                old_external_ram
242                w
243                old_special_function_registers_8051
244                old_special_function_registers_8052
245                old_p1_latch
246                old_p3_latch.
247               
248ndefinition set_code_memory ≝
249  λs: Status.
250  λi: SFR8052.
251  λr: BitVectorTrie Byte sixteen.
252    let index ≝ sfr_8052_index i in
253    let old_low_internal_ram ≝ low_internal_ram s in
254    let old_high_internal_ram ≝ high_internal_ram s in
255    let old_external_ram ≝ external_ram s in
256    let old_program_counter ≝ program_counter s in
257    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
258    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
259    let old_p1_latch ≝ p1_latch s in
260    let old_p3_latch ≝ p3_latch s in
261      mk_Status r
262                old_low_internal_ram
263                old_high_internal_ram
264                old_external_ram
265                old_program_counter
266                old_special_function_registers_8051
267                old_special_function_registers_8052
268                old_p1_latch
269                old_p3_latch.
270               
271ndefinition set_low_internal_ram ≝
272  λs: Status.
273  λi: SFR8052.
274  λr: BitVectorTrie Byte seven.
275    let index ≝ sfr_8052_index i in
276    let old_code_memory ≝ code_memory 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_program_counter ≝ program_counter s in
280    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
281    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
282    let old_p1_latch ≝ p1_latch s in
283    let old_p3_latch ≝ p3_latch s in
284      mk_Status old_code_memory
285                r
286                old_high_internal_ram
287                old_external_ram
288                old_program_counter
289                old_special_function_registers_8051
290                old_special_function_registers_8052
291                old_p1_latch
292                old_p3_latch.
293               
294ndefinition set_high_internal_ram ≝
295  λs: Status.
296  λi: SFR8052.
297  λr: BitVectorTrie Byte seven.
298    let index ≝ sfr_8052_index i in
299    let old_code_memory ≝ code_memory s in
300    let old_low_internal_ram ≝ low_internal_ram s in
301    let old_high_internal_ram ≝ high_internal_ram s in
302    let old_external_ram ≝ external_ram s in
303    let old_program_counter ≝ program_counter s in
304    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
305    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
306    let old_p1_latch ≝ p1_latch s in
307    let old_p3_latch ≝ p3_latch s in
308      mk_Status old_code_memory
309                old_low_internal_ram
310                r
311                old_external_ram
312                old_program_counter
313                old_special_function_registers_8051
314                old_special_function_registers_8052
315                old_p1_latch
316                old_p3_latch.
317               
318naxiom less_than_or_equal_monotone:
319  ∀m, n: Nat.
320    m ≤ n → S m ≤ S n.
321   
322alias id "get_index" = "cic:/matita/ng/Vector/get_index.fix(0,3,2)".
323               
324ndefinition get_cy_flag ≝
325  λs: Status.
326    let sfr ≝ special_function_registers_8051 s in
327    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
328      get_index Bool eight psw Z ?.
329    nnormalize.
330    napply (less_than_or_equal_monotone ? ?).
331    napply (less_than_or_equal_zero).
332    nrepeat (napply (less_than_or_equal_monotone ? ?)).
333    napply (less_than_or_equal_zero).
334nqed.
335
336ndefinition get_ac_flag ≝
337  λs: Status.
338    let sfr ≝ special_function_registers_8051 s in
339    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
340      get_index Bool eight psw (S Z) ?.
341    nnormalize.
342    nrepeat (napply (less_than_or_equal_monotone ? ?)).
343    napply (less_than_or_equal_zero).
344    nrepeat (napply (less_than_or_equal_monotone ? ?)).
345    napply (less_than_or_equal_zero).
346nqed.
347
348ndefinition get_fo_flag ≝
349  λs: Status.
350    let sfr ≝ special_function_registers_8051 s in
351    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
352      get_index Bool eight psw two ?.
353    nnormalize.
354    nrepeat (napply (less_than_or_equal_monotone ? ?)).
355    napply (less_than_or_equal_zero).
356    nrepeat (napply (less_than_or_equal_monotone ? ?)).
357    napply (less_than_or_equal_zero).
358nqed.
359
360ndefinition get_rs1_flag ≝
361  λs: Status.
362    let sfr ≝ special_function_registers_8051 s in
363    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
364      get_index Bool eight psw three ?.
365    nnormalize.
366    nrepeat (napply (less_than_or_equal_monotone ? ?)).
367    napply (less_than_or_equal_zero).
368    nrepeat (napply (less_than_or_equal_monotone ? ?)).
369    napply (less_than_or_equal_zero).
370nqed.
371
372ndefinition get_rs0_flag ≝
373  λs: Status.
374    let sfr ≝ special_function_registers_8051 s in
375    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
376      get_index Bool eight psw four ?.
377    nnormalize.
378    nrepeat (napply (less_than_or_equal_monotone ? ?)).
379    napply (less_than_or_equal_zero).
380    nrepeat (napply (less_than_or_equal_monotone ? ?)).
381    napply (less_than_or_equal_zero).
382nqed.
383
384ndefinition get_ov_flag ≝
385  λs: Status.
386    let sfr ≝ special_function_registers_8051 s in
387    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
388      get_index Bool eight psw five ?.
389    nnormalize.
390    nrepeat (napply (less_than_or_equal_monotone ? ?)).
391    napply (less_than_or_equal_zero).
392    nrepeat (napply (less_than_or_equal_monotone ? ?)).
393    napply (less_than_or_equal_zero).
394nqed.
395
396ndefinition get_ud_flag ≝
397  λs: Status.
398    let sfr ≝ special_function_registers_8051 s in
399    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
400      get_index Bool eight psw six ?.
401    nnormalize.
402    nrepeat (napply (less_than_or_equal_monotone ? ?)).
403    napply (less_than_or_equal_zero).
404    nrepeat (napply (less_than_or_equal_monotone ? ?)).
405    napply (less_than_or_equal_zero).
406nqed.
407
408ndefinition get_p_flag ≝
409  λs: Status.
410    let sfr ≝ special_function_registers_8051 s in
411    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
412      get_index Bool eight psw seven ?.
413    nnormalize.
414    nrepeat (napply (less_than_or_equal_monotone ? ?)).
415    napply (less_than_or_equal_zero).
416    nrepeat (napply (less_than_or_equal_monotone ? ?)).
417    napply (less_than_or_equal_zero).
418nqed.
419
420ndefinition initialise_status ≝
421  let status ≝ mk_Status (Stub Byte sixteen)                    (* Code mem. *)
422                         (Stub Byte seven)                      (* Low mem.  *)
423                         (Stub Byte seven)                      (* High mem. *)
424                         (Stub Byte sixteen)                    (* Ext mem.  *)
425                         (zero sixteen)                         (* PC.       *)
426                         (replicate Byte nineteen (zero eight)) (* 8051 SFR. *)
427                         (replicate Byte five (zero eight))     (* 8052 SFR. *)
428                         (zero eight)                           (* P1 latch. *)
429                         (zero eight) in                        (* P3 latch. *)
430  set_program_counter status (bitvector_of_nat sixteen seven).
431 
432naxiom not_implemented: False.
433 
434include "Arithmetic.ma".
435 
436ndefinition get_bit_addressable_sfr ≝
437  λs: Status.
438  λn: Nat.
439  λb: BitVector n.
440  λl: Bool.
441    let address ≝ nat_of_bitvector … b in
442      if (decidable_equality address one_hundred_and_twenty_eight) then
443        ?
444      else if (decidable_equality address one_hundred_and_forty_four) then
445        if l then
446          (p1_latch s)
447        else
448          (get_8051_sfr s SFR_P1)
449      else if (decidable_equality address one_hundred_and_sixty) then
450        ?
451      else if (decidable_equality address one_hundred_and_seventy_six) then
452        if l then
453          (p3_latch s)
454        else
455          (get_8051_sfr s SFR_P3)
456      else if (decidable_equality address one_hundred_and_fifty_three) then
457        get_8051_sfr s SFR_SBUF
458      else if (decidable_equality address one_hundred_and_thirty_eight) then
459        get_8051_sfr s SFR_TL0
460      else if (decidable_equality address one_hundred_and_thirty_nine) then
461        get_8051_sfr s SFR_TL1
462      else if (decidable_equality address one_hundred_and_forty) then
463        get_8051_sfr s SFR_TH0
464      else if (decidable_equality address one_hundred_and_forty_one) then
465        get_8051_sfr s SFR_TH1
466      else if (decidable_equality address two_hundred) then
467        get_8052_sfr s SFR_T2CON
468      else if (decidable_equality address two_hundred_and_two) then
469        get_8052_sfr s SFR_RCAP2L
470      else if (decidable_equality address two_hundred_and_three) then
471        get_8052_sfr s SFR_RCAP2H
472      else if (decidable_equality address two_hundred_and_four) then
473        get_8052_sfr s SFR_TL2
474      else if (decidable_equality address two_hundred_and_five) then
475        get_8052_sfr s SFR_TH2
476      else if (decidable_equality address one_hundred_and_thirty_five) then
477        get_8051_sfr s SFR_PCON
478      else if (decidable_equality address one_hundred_and_thirty_six) then
479        get_8051_sfr s SFR_TCON
480      else if (decidable_equality address one_hundred_and_thirty_seven) then
481        get_8051_sfr s SFR_TMOD
482      else if (decidable_equality address one_hundred_and_fifty_two) then
483        get_8051_sfr s SFR_SCON
484      else if (decidable_equality address one_hundred_and_sixty_eight) then
485        get_8051_sfr s SFR_IE
486      else if (decidable_equality address one_hundred_and_eighty_four) then
487        get_8051_sfr s SFR_IP
488      else if (decidable_equality address one_hundred_and_twenty_nine) then
489        get_8051_sfr s SFR_SP
490      else if (decidable_equality address one_hundred_and_thirty) then
491        get_8051_sfr s SFR_DPL
492      else if (decidable_equality address one_hundred_and_thirty_one) then
493        get_8051_sfr s SFR_DPH
494      else if (decidable_equality address two_hundred_and_eight) then
495        get_8051_sfr s SFR_PSW
496      else if (decidable_equality address two_hundred_and_twenty_four) then
497        get_8051_sfr s SFR_ACC_A
498      else if (decidable_equality address two_hundred_and_forty) then
499        get_8051_sfr s SFR_ACC_B
500      else
501        ?.
502      ncases not_implemented.
503nqed.
504
505ndefinition set_bit_addressable_sfr ≝
506  λs: Status.
507  λb: Byte.
508    let address ≝ nat_of_bitvector … b in
509      if (decidable_equality address one_hundred_and_twenty_eight) then
510        ?
511      else if (decidable_equality address one_hundred_and_forty_four) then
512        let status_1 ≝ set_8051_sfr s SFR_P1 b in
513        let status_2 ≝ set_p1_latch s b in
514          status_2
515      else if (decidable_equality address one_hundred_and_sixty) then
516        ?
517      else if (decidable_equality address one_hundred_and_seventy_six) then
518        let status_1 ≝ set_8051_sfr s SFR_P3 b in
519        let status_2 ≝ set_p3_latch s b in
520          status_2
521      else if (decidable_equality address one_hundred_and_fifty_three) then
522        set_8051_sfr s SFR_SBUF b
523      else if (decidable_equality address one_hundred_and_thirty_eight) then
524        set_8051_sfr s SFR_TL0 b
525      else if (decidable_equality address one_hundred_and_thirty_nine) then
526        set_8051_sfr s SFR_TL1 b
527      else if (decidable_equality address one_hundred_and_forty) then
528        set_8051_sfr s SFR_TH0 b
529      else if (decidable_equality address one_hundred_and_forty_one) then
530        set_8051_sfr s SFR_TH1 b
531      else if (decidable_equality address two_hundred) then
532        set_8052_sfr s SFR_T2CON b
533      else if (decidable_equality address two_hundred_and_two) then
534        set_8052_sfr s SFR_RCAP2L b
535      else if (decidable_equality address two_hundred_and_three) then
536        set_8052_sfr s SFR_RCAP2H b
537      else if (decidable_equality address two_hundred_and_four) then
538        set_8052_sfr s SFR_TL2 b
539      else if (decidable_equality address two_hundred_and_five) then
540        set_8052_sfr s SFR_TH2 b
541      else if (decidable_equality address one_hundred_and_thirty_five) then
542        set_8051_sfr s SFR_PCON b
543      else if (decidable_equality address one_hundred_and_thirty_six) then
544        set_8051_sfr s SFR_TCON b
545      else if (decidable_equality address one_hundred_and_thirty_seven) then
546        set_8051_sfr s SFR_TMOD b
547      else if (decidable_equality address one_hundred_and_fifty_two) then
548        set_8051_sfr s SFR_SCON b
549      else if (decidable_equality address one_hundred_and_sixty_eight) then
550        set_8051_sfr s SFR_IE b
551      else if (decidable_equality address one_hundred_and_eighty_four) then
552        set_8051_sfr s SFR_IP b
553      else if (decidable_equality address one_hundred_and_twenty_nine) then
554        set_8051_sfr s SFR_SP b
555      else if (decidable_equality address one_hundred_and_thirty) then
556        set_8051_sfr s SFR_DPL b
557      else if (decidable_equality address one_hundred_and_thirty_one) then
558        set_8051_sfr s SFR_DPH b
559      else if (decidable_equality address two_hundred_and_eight) then
560        set_8051_sfr s SFR_PSW b
561      else if (decidable_equality address two_hundred_and_twenty_four) then
562        set_8051_sfr s SFR_ACC_A b
563      else if (decidable_equality address two_hundred_and_forty) then
564        set_8051_sfr s SFR_ACC_B b
565      else
566        ?.
567      ncases not_implemented.
568nqed.
569
570ndefinition bit_address_of_register ≝
571  λs: Status.
572  λb, c, d: Bit.
573    let 〈 un, ln 〉 ≝ split ? four four (get_8051_sfr s SFR_PSW) in
574    let 〈 r1, r0 〉 ≝ mk_Cartesian … (get_index four un two ?) (get_index four un three ?) in
575    let offset ≝
576      if conjunction (negation r1) (negation r0) then
577        Z
578      else if conjunction (negation r1) r0 then
579        eight
580      else if conjunction r1 r0 then
581        twenty_four
582      else
583        sixteen
584    in
585      bitvector_of_nat seven (offset + (nat_of_bitvector ? [[ false ; b ; c ; d ]])).
586    nnormalize.
587    nrepeat (napply less_than_or_equal_monotone).
588    napply less_than_or_equal_zero.
589    nrepeat (napply less_than_or_equal_monotone).
590    napply less_than_or_equal_zero.
591nqed.
Note: See TracBrowser for help on using the repository browser.