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

Last change on this file since 283 was 281, checked in by mulligan, 10 years ago

Resolved conflicts.
File size: 15.1 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 get_8051_sfr ≝
112  λs: Status.
113  λi: SFR8051.
114    let sfr ≝ special_function_registers_8051 s in
115    let index ≝ sfr_8051_index i in
116      get_index … sfr index ?.
117    napply (sfr8051_index_nineteen i).
118nqed.
119
120ndefinition get_8052_sfr ≝
121  λs: Status.
122  λi: SFR8052.
123    let sfr ≝ special_function_registers_8052 s in
124    let index ≝ sfr_8052_index i in
125      get_index … sfr index ?.
126    napply (sfr8052_index_five i).
127nqed.
128
129ndefinition set_8051_sfr ≝
130  λs: Status.
131  λi: SFR8051.
132  λb: Byte.
133    let index ≝ sfr_8051_index i in
134    let old_code_memory ≝ code_memory s in
135    let old_low_internal_ram ≝ low_internal_ram s in
136    let old_high_internal_ram ≝ high_internal_ram s in
137    let old_external_ram ≝ external_ram s in
138    let old_program_counter ≝ program_counter s in
139    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
140    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
141    let new_special_function_registers_8051 ≝
142      cic:/matita/ng/Vector/set_index.fix(0,3,2) Byte nineteen old_special_function_registers_8051 index b ? 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                new_special_function_registers_8051
149                old_special_function_registers_8052.
150    napply (sfr8051_index_nineteen i).
151nqed.
152
153ndefinition set_8052_sfr ≝
154  λs: Status.
155  λi: SFR8052.
156  λb: Byte.
157    let index ≝ sfr_8052_index i in
158    let old_code_memory ≝ code_memory s in
159    let old_low_internal_ram ≝ low_internal_ram s in
160    let old_high_internal_ram ≝ high_internal_ram s in
161    let old_external_ram ≝ external_ram s in
162    let old_program_counter ≝ program_counter s in
163    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
164    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
165    let new_special_function_registers_8052 ≝
166      cic:/matita/ng/Vector/set_index.fix(0,3,2) Byte five old_special_function_registers_8052 index b ? in
167      mk_Status old_code_memory
168                old_low_internal_ram
169                old_high_internal_ram
170                old_external_ram
171                old_program_counter
172                old_special_function_registers_8051
173                new_special_function_registers_8052.
174    napply (sfr8052_index_five i).
175nqed.
176
177ndefinition set_program_counter ≝
178  λs: Status.
179  λw: Word.
180    let old_code_memory ≝ code_memory s in
181    let old_low_internal_ram ≝ low_internal_ram s in
182    let old_high_internal_ram ≝ high_internal_ram s in
183    let old_external_ram ≝ external_ram s in
184    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
185    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
186      mk_Status old_code_memory
187                old_low_internal_ram
188                old_high_internal_ram
189                old_external_ram
190                w
191                old_special_function_registers_8051
192                old_special_function_registers_8052.
193               
194ndefinition set_code_memory ≝
195  λs: Status.
196  λi: SFR8052.
197  λr: BitVectorTrie Byte sixteen.
198    let index ≝ sfr_8052_index i in
199    let old_low_internal_ram ≝ low_internal_ram s in
200    let old_high_internal_ram ≝ high_internal_ram s in
201    let old_external_ram ≝ external_ram s in
202    let old_program_counter ≝ program_counter s in
203    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
204    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
205      mk_Status r
206                old_low_internal_ram
207                old_high_internal_ram
208                old_external_ram
209                old_program_counter
210                old_special_function_registers_8051
211                old_special_function_registers_8052.
212               
213ndefinition set_low_internal_ram ≝
214  λs: Status.
215  λi: SFR8052.
216  λr: BitVectorTrie Byte seven.
217    let index ≝ sfr_8052_index i in
218    let old_code_memory ≝ code_memory 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      mk_Status old_code_memory
225                r
226                old_high_internal_ram
227                old_external_ram
228                old_program_counter
229                old_special_function_registers_8051
230                old_special_function_registers_8052.
231               
232naxiom less_than_or_equal_monotone:
233  ∀m, n: Nat.
234    m ≤ n → S m ≤ S n.
235   
236alias id "get_index" = "cic:/matita/ng/Vector/get_index.fix(0,3,2)".
237               
238ndefinition get_cy_flag ≝
239  λs: Status.
240    let sfr ≝ special_function_registers_8051 s in
241    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
242      get_index Bool eight psw Z ?.
243    nnormalize.
244    napply (less_than_or_equal_monotone ? ?).
245    napply (less_than_or_equal_zero).
246    nrepeat (napply (less_than_or_equal_monotone ? ?)).
247    napply (less_than_or_equal_zero).
248nqed.
249
250ndefinition get_ac_flag ≝
251  λs: Status.
252    let sfr ≝ special_function_registers_8051 s in
253    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
254      get_index Bool eight psw (S Z) ?.
255    nnormalize.
256    nrepeat (napply (less_than_or_equal_monotone ? ?)).
257    napply (less_than_or_equal_zero).
258    nrepeat (napply (less_than_or_equal_monotone ? ?)).
259    napply (less_than_or_equal_zero).
260nqed.
261
262ndefinition get_fo_flag ≝
263  λs: Status.
264    let sfr ≝ special_function_registers_8051 s in
265    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
266      get_index Bool eight psw two ?.
267    nnormalize.
268    nrepeat (napply (less_than_or_equal_monotone ? ?)).
269    napply (less_than_or_equal_zero).
270    nrepeat (napply (less_than_or_equal_monotone ? ?)).
271    napply (less_than_or_equal_zero).
272nqed.
273
274ndefinition get_rs1_flag ≝
275  λs: Status.
276    let sfr ≝ special_function_registers_8051 s in
277    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
278      get_index Bool eight psw three ?.
279    nnormalize.
280    nrepeat (napply (less_than_or_equal_monotone ? ?)).
281    napply (less_than_or_equal_zero).
282    nrepeat (napply (less_than_or_equal_monotone ? ?)).
283    napply (less_than_or_equal_zero).
284nqed.
285
286ndefinition get_rs0_flag ≝
287  λs: Status.
288    let sfr ≝ special_function_registers_8051 s in
289    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
290      get_index Bool eight psw four ?.
291    nnormalize.
292    nrepeat (napply (less_than_or_equal_monotone ? ?)).
293    napply (less_than_or_equal_zero).
294    nrepeat (napply (less_than_or_equal_monotone ? ?)).
295    napply (less_than_or_equal_zero).
296nqed.
297
298ndefinition get_ov_flag ≝
299  λs: Status.
300    let sfr ≝ special_function_registers_8051 s in
301    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
302      get_index Bool eight psw five ?.
303    nnormalize.
304    nrepeat (napply (less_than_or_equal_monotone ? ?)).
305    napply (less_than_or_equal_zero).
306    nrepeat (napply (less_than_or_equal_monotone ? ?)).
307    napply (less_than_or_equal_zero).
308nqed.
309
310ndefinition get_ud_flag ≝
311  λs: Status.
312    let sfr ≝ special_function_registers_8051 s in
313    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
314      get_index Bool eight psw six ?.
315    nnormalize.
316    nrepeat (napply (less_than_or_equal_monotone ? ?)).
317    napply (less_than_or_equal_zero).
318    nrepeat (napply (less_than_or_equal_monotone ? ?)).
319    napply (less_than_or_equal_zero).
320nqed.
321
322ndefinition get_p_flag ≝
323  λs: Status.
324    let sfr ≝ special_function_registers_8051 s in
325    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
326      get_index Bool eight psw seven ?.
327    nnormalize.
328    nrepeat (napply (less_than_or_equal_monotone ? ?)).
329    napply (less_than_or_equal_zero).
330    nrepeat (napply (less_than_or_equal_monotone ? ?)).
331    napply (less_than_or_equal_zero).
332nqed.
333               
334ndefinition set_high_internal_ram ≝
335  λs: Status.
336  λi: SFR8052.
337  λr: BitVectorTrie Byte seven.
338    let index ≝ sfr_8052_index i in
339    let old_code_memory ≝ code_memory s in
340    let old_low_internal_ram ≝ low_internal_ram s in
341    let old_high_internal_ram ≝ high_internal_ram s in
342    let old_external_ram ≝ external_ram s in
343    let old_program_counter ≝ program_counter s in
344    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
345    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
346      mk_Status old_code_memory
347                old_low_internal_ram
348                r
349                old_external_ram
350                old_program_counter
351                old_special_function_registers_8051
352                old_special_function_registers_8052.
353
354ndefinition initialise_status ≝
355  let status ≝ mk_Status (Stub Byte sixteen)
356                         (Stub Byte seven)
357                         (Stub Byte seven)
358                         (Stub Byte sixteen)
359                         (zero sixteen)
360                         (replicate Byte nineteen (zero eight))
361                         (replicate Byte five (zero eight))
362                         (zero eight)
363                         (zero eight) in
364  set_program_counter status (bitvector_of_nat sixteen seven).
365 
366naxiom not_implemented: False.
367 
368include "Arithmetic.ma".
369 
370ndefinition get_bit_addressable_sfr ≝
371  λs: Status.
372  λn: Nat.
373  λb: BitVector n.
374  λl: Bool.
375    let address ≝ nat_of_bitvector … b in
376      if (decidable_equality address one_hundred_and_twenty_eight) then
377        ?
378      else if (decidable_equality address one_hundred_and_forty_four) then
379        if l then
380          (p1_latch s)
381        else
382          (get_8051_sfr s SFR_P1)
383      else if (decidable_equality address one_hundred_and_sixty) then
384        ?
385      else if (decidable_equality address one_hundred_and_seventy_six) then
386        if l then
387          (p3_latch s)
388        else
389          (get_8051_sfr s SFR_P3)
390      else if (decidable_equality address one_hundred_and_fifty_three) then
391        get_8051_sfr s SFR_SBUF
392      else if (decidable_equality address one_hundred_and_thirty_eight) then
393        get_8051_sfr s SFR_TL0
394      else if (decidable_equality address one_hundred_and_thirty_nine) then
395        get_8051_sfr s SFR_TL1
396      else if (decidable_equality address one_hundred_and_forty) then
397        get_8051_sfr s SFR_TH0
398      else if (decidable_equality address one_hundred_and_forty_one) then
399        get_8051_sfr s SFR_TH1
400      else if (decidable_equality address two_hundred) then
401        get_8052_sfr s SFR_T2CON
402      else if (decidable_equality address two_hundred_and_two) then
403        get_8052_sfr s SFR_RCAP2L
404      else if (decidable_equality address two_hundred_and_three) then
405        get_8052_sfr s SFR_RCAP2H
406      else if (decidable_equality address two_hundred_and_four) then
407        get_8052_sfr s SFR_TL2
408      else if (decidable_equality address two_hundred_and_five) then
409        get_8052_sfr s SFR_TH2
410      else if (decidable_equality address one_hundred_and_thirty_five) then
411        get_8051_sfr s SFR_PCON
412      else if (decidable_equality address one_hundred_and_thirty_six) then
413        get_8051_sfr s SFR_TCON
414      else if (decidable_equality address one_hundred_and_thirty_seven) then
415        get_8051_sfr s SFR_TMOD
416      else if (decidable_equality address one_hundred_and_fifty_two) then
417        get_8051_sfr s SFR_SCON
418      else if (decidable_equality address one_hundred_and_sixty_eight) then
419        get_8051_sfr s SFR_IE
420      else if (decidable_equality address one_hundred_and_eighty_four) then
421        get_8051_sfr s SFR_IP
422      else if (decidable_equality address one_hundred_and_twenty_nine) then
423        get_8051_sfr s SFR_SP
424      else if (decidable_equality address one_hundred_and_thirty) then
425        get_8051_sfr s SFR_DPL
426      else if (decidable_equality address one_hundred_and_thirty_one) then
427        get_8051_sfr s SFR_DPH
428      else if (decidable_equality address two_hundred_and_eight) then
429        get_8051_sfr s SFR_PSW
430      else if (decidable_equality address two_hundred_and_twenty_four) then
431        get_8051_sfr s SFR_ACC_A
432      else if (decidable_equality address two_hundred_and_forty) then
433        get_8051_sfr s SFR_ACC_B
434      else
435        ?.
436      ncases not_implemented.
437nqed.
Note: See TracBrowser for help on using the repository browser.