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

Last change on this file since 277 was 276, checked in by mulligan, 10 years ago

Messed up a file.

File size: 12.0 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
100naxiom sfr8051_index_nineteen:
101  ∀i: SFR8051.
102    sfr_8051_index i < nineteen.
103   
104naxiom sfr8052_index_five:
105  ∀i: SFR8052.
106    sfr_8052_index i < five.
107
108ndefinition get_8051_sfr ≝
109  λs: Status.
110  λi: SFR8051.
111    let sfr ≝ special_function_registers_8051 s in
112    let index ≝ sfr_8051_index i in
113      get_index … sfr index ?.
114    napply (sfr8051_index_nineteen i).
115nqed.
116
117ndefinition get_8052_sfr ≝
118  λs: Status.
119  λi: SFR8052.
120    let sfr ≝ special_function_registers_8052 s in
121    let index ≝ sfr_8052_index i in
122      get_index … sfr index ?.
123    napply (sfr8052_index_five i).
124nqed.
125
126ndefinition set_8051_sfr ≝
127  λs: Status.
128  λi: SFR8051.
129  λb: Byte.
130    let index ≝ sfr_8051_index i in
131    let old_code_memory ≝ code_memory s in
132    let old_low_internal_ram ≝ low_internal_ram s in
133    let old_high_internal_ram ≝ high_internal_ram s in
134    let old_external_ram ≝ external_ram s in
135    let old_program_counter ≝ program_counter s in
136    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
137    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
138    let new_special_function_registers_8051 ≝
139      cic:/matita/ng/Vector/set_index.fix(0,3,2) Byte nineteen old_special_function_registers_8051 index b ? in
140      mk_Status old_code_memory
141                old_low_internal_ram
142                old_high_internal_ram
143                old_external_ram
144                old_program_counter
145                new_special_function_registers_8051
146                old_special_function_registers_8052.
147    napply (sfr8051_index_nineteen i).
148nqed.
149
150ndefinition set_8052_sfr ≝
151  λs: Status.
152  λi: SFR8052.
153  λb: Byte.
154    let index ≝ sfr_8052_index i in
155    let old_code_memory ≝ code_memory s in
156    let old_low_internal_ram ≝ low_internal_ram s in
157    let old_high_internal_ram ≝ high_internal_ram s in
158    let old_external_ram ≝ external_ram s in
159    let old_program_counter ≝ program_counter s in
160    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
161    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
162    let new_special_function_registers_8052 ≝
163      cic:/matita/ng/Vector/set_index.fix(0,3,2) Byte five old_special_function_registers_8052 index b ? in
164      mk_Status old_code_memory
165                old_low_internal_ram
166                old_high_internal_ram
167                old_external_ram
168                old_program_counter
169                old_special_function_registers_8051
170                new_special_function_registers_8052.
171    napply (sfr8052_index_five i).
172nqed.
173
174ndefinition set_program_counter ≝
175  λs: Status.
176  λi: SFR8052.
177  λw: Word.
178    let index ≝ sfr_8052_index i in
179    let old_code_memory ≝ code_memory s in
180    let old_low_internal_ram ≝ low_internal_ram s in
181    let old_high_internal_ram ≝ high_internal_ram s in
182    let old_external_ram ≝ external_ram s in
183    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
184    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
185      mk_Status old_code_memory
186                old_low_internal_ram
187                old_high_internal_ram
188                old_external_ram
189                w
190                old_special_function_registers_8051
191                old_special_function_registers_8052.
192               
193ndefinition set_code_memory ≝
194  λs: Status.
195  λi: SFR8052.
196  λr: BitVectorTrie Byte sixteen.
197    let index ≝ sfr_8052_index i in
198    let old_low_internal_ram ≝ low_internal_ram s in
199    let old_high_internal_ram ≝ high_internal_ram s in
200    let old_external_ram ≝ external_ram s in
201    let old_program_counter ≝ program_counter s in
202    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
203    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
204      mk_Status r
205                old_low_internal_ram
206                old_high_internal_ram
207                old_external_ram
208                old_program_counter
209                old_special_function_registers_8051
210                old_special_function_registers_8052.
211               
212ndefinition set_low_internal_ram ≝
213  λs: Status.
214  λi: SFR8052.
215  λr: BitVectorTrie Byte seven.
216    let index ≝ sfr_8052_index i in
217    let old_code_memory ≝ code_memory s in
218    let old_high_internal_ram ≝ high_internal_ram s in
219    let old_external_ram ≝ external_ram s in
220    let old_program_counter ≝ program_counter s in
221    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
222    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
223      mk_Status old_code_memory
224                r
225                old_high_internal_ram
226                old_external_ram
227                old_program_counter
228                old_special_function_registers_8051
229                old_special_function_registers_8052.
230               
231naxiom less_than_or_equal_monotone:
232  ∀m, n: Nat.
233    m ≤ n → S m ≤ S n.
234   
235alias id "get_index" = "cic:/matita/ng/Vector/get_index.fix(0,3,2)".
236               
237ndefinition get_cy_flag ≝
238  λs: Status.
239    let sfr ≝ special_function_registers_8051 s in
240    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
241      get_index Bool eight psw Z ?.
242    nnormalize.
243    napply (less_than_or_equal_monotone ? ?).
244    napply (less_than_or_equal_zero).
245    nrepeat (napply (less_than_or_equal_monotone ? ?)).
246    napply (less_than_or_equal_zero).
247nqed.
248
249ndefinition get_ac_flag ≝
250  λs: Status.
251    let sfr ≝ special_function_registers_8051 s in
252    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
253      get_index Bool eight psw (S Z) ?.
254    nnormalize.
255    nrepeat (napply (less_than_or_equal_monotone ? ?)).
256    napply (less_than_or_equal_zero).
257    nrepeat (napply (less_than_or_equal_monotone ? ?)).
258    napply (less_than_or_equal_zero).
259nqed.
260
261ndefinition get_fo_flag ≝
262  λs: Status.
263    let sfr ≝ special_function_registers_8051 s in
264    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
265      get_index Bool eight psw two ?.
266    nnormalize.
267    nrepeat (napply (less_than_or_equal_monotone ? ?)).
268    napply (less_than_or_equal_zero).
269    nrepeat (napply (less_than_or_equal_monotone ? ?)).
270    napply (less_than_or_equal_zero).
271nqed.
272
273ndefinition get_rs1_flag ≝
274  λs: Status.
275    let sfr ≝ special_function_registers_8051 s in
276    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
277      get_index Bool eight psw three ?.
278    nnormalize.
279    nrepeat (napply (less_than_or_equal_monotone ? ?)).
280    napply (less_than_or_equal_zero).
281    nrepeat (napply (less_than_or_equal_monotone ? ?)).
282    napply (less_than_or_equal_zero).
283nqed.
284
285ndefinition get_rs0_flag ≝
286  λs: Status.
287    let sfr ≝ special_function_registers_8051 s in
288    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
289      get_index Bool eight psw four ?.
290    nnormalize.
291    nrepeat (napply (less_than_or_equal_monotone ? ?)).
292    napply (less_than_or_equal_zero).
293    nrepeat (napply (less_than_or_equal_monotone ? ?)).
294    napply (less_than_or_equal_zero).
295nqed.
296
297ndefinition get_ov_flag ≝
298  λs: Status.
299    let sfr ≝ special_function_registers_8051 s in
300    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
301      get_index Bool eight psw five ?.
302    nnormalize.
303    nrepeat (napply (less_than_or_equal_monotone ? ?)).
304    napply (less_than_or_equal_zero).
305    nrepeat (napply (less_than_or_equal_monotone ? ?)).
306    napply (less_than_or_equal_zero).
307nqed.
308
309ndefinition get_ud_flag ≝
310  λs: Status.
311    let sfr ≝ special_function_registers_8051 s in
312    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
313      get_index Bool eight psw six ?.
314    nnormalize.
315    nrepeat (napply (less_than_or_equal_monotone ? ?)).
316    napply (less_than_or_equal_zero).
317    nrepeat (napply (less_than_or_equal_monotone ? ?)).
318    napply (less_than_or_equal_zero).
319nqed.
320
321ndefinition get_p_flag ≝
322  λs: Status.
323    let sfr ≝ special_function_registers_8051 s in
324    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
325      get_index Bool eight psw seven ?.
326    nnormalize.
327    nrepeat (napply (less_than_or_equal_monotone ? ?)).
328    napply (less_than_or_equal_zero).
329    nrepeat (napply (less_than_or_equal_monotone ? ?)).
330    napply (less_than_or_equal_zero).
331nqed.
332               
333ndefinition set_high_internal_ram ≝
334  λs: Status.
335  λi: SFR8052.
336  λr: BitVectorTrie Byte seven.
337    let index ≝ sfr_8052_index i in
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      mk_Status old_code_memory
346                old_low_internal_ram
347                r
348                old_external_ram
349                old_program_counter
350                old_special_function_registers_8051
351                old_special_function_registers_8052.
352
353ndefinition initialise_status ≝
354  let status ≝ mk_Status (Stub Byte sixteen)
355                         (Stub Byte seven)
356                         (Stub Byte seven)
357                         (Stub Byte sixteen)
358                         (zero sixteen)
359                         (replicate Byte nineteen (zero eight))
360                         (replicate Byte five (zero eight)) in
361  status.
Note: See TracBrowser for help on using the repository browser.