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

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

Renamed Interpret to Status.

File size: 11.7 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
9ninductive SFR8051: Type[0] ≝
10  SFR_SP: SFR8051
11| SFR_DPL: SFR8051
12| SFR_DPH: SFR8051
13| SFR_PCON: SFR8051
14| SFR_TCON: SFR8051
15| SFR_TMOD: SFR8051
16| SFR_TL0: SFR8051
17| SFR_TL1: SFR8051
18| SFR_TH0: SFR8051
19| SFR_TH1: SFR8051
20| SFR_P1: SFR8051
21| SFR_SCON: SFR8051
22| SFR_SBUF: SFR8051
23| SFR_IE: SFR8051
24| SFR_P3: SFR8051
25| SFR_IP: SFR8051
26| SFR_PSW: SFR8051
27| SFR_ACC_A: SFR8051
28| SFR_ACC_B: SFR8051.
29
30ndefinition sfr_8051_index ≝
31  λs: SFR8051.
32    match s with
33      [ SFR_SP ⇒ Z
34      | SFR_DPL ⇒ S Z
35      | SFR_DPH ⇒ two
36      | SFR_PCON ⇒ three
37      | SFR_TCON ⇒ four
38      | SFR_TMOD ⇒ five
39      | SFR_TL0 ⇒ six
40      | SFR_TL1 ⇒ seven
41      | SFR_TH0 ⇒ eight
42      | SFR_TH1 ⇒ nine
43      | SFR_P1 ⇒ ten
44      | SFR_SCON ⇒ eleven
45      | SFR_SBUF ⇒ twelve
46      | SFR_IE ⇒ thirteen
47      | SFR_P3 ⇒ fourteen
48      | SFR_IP ⇒ fifteen
49      | SFR_PSW ⇒ sixteen
50      | SFR_ACC_A ⇒ seventeen
51      | SFR_ACC_B ⇒ eighteen
52      ].
53     
54ninductive SFR8052: Type[0] ≝
55   SFR_T2CON: SFR8052
56|  SFR_RCAP2L: SFR8052
57|  SFR_RCAP2H: SFR8052
58|  SFR_TL2: SFR8052
59|  SFR_TH2: SFR8052.
60
61ndefinition sfr_8052_index ≝
62  λs: SFR8052.
63    match s with
64      [ SFR_T2CON ⇒ Z
65      | SFR_RCAP2L ⇒ S Z
66      | SFR_RCAP2H ⇒ two
67      | SFR_TL2 ⇒ three
68      | SFR_TH2 ⇒ four
69      ].
70
71(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
72(* Processor status.                                                          *)
73(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
74nrecord Status: Type[0] ≝
75{
76  code_memory: BitVectorTrie Byte sixteen;
77  low_internal_ram: BitVectorTrie Byte seven;
78  high_internal_ram: BitVectorTrie Byte seven;
79  external_ram: BitVectorTrie Byte sixteen;
80 
81  program_counter: Word;
82 
83  special_function_registers_8051: Vector Byte nineteen;
84  special_function_registers_8052: Vector Byte five
85}.
86
87naxiom sfr8051_index_nineteen:
88  ∀i: SFR8051.
89    sfr_8051_index i < nineteen.
90   
91naxiom sfr8052_index_five:
92  ∀i: SFR8052.
93    sfr_8052_index i < five.
94
95ndefinition get_8051_sfr ≝
96  λs: Status.
97  λi: SFR8051.
98    let sfr ≝ special_function_registers_8051 s in
99    let index ≝ sfr_8051_index i in
100      get_index … sfr index ?.
101    napply (sfr8051_index_nineteen i).
102nqed.
103
104ndefinition get_8052_sfr ≝
105  λs: Status.
106  λi: SFR8052.
107    let sfr ≝ special_function_registers_8052 s in
108    let index ≝ sfr_8052_index i in
109      get_index … sfr index ?.
110    napply (sfr8052_index_five i).
111nqed.
112
113ndefinition set_8051_sfr ≝
114  λs: Status.
115  λi: SFR8051.
116  λb: Byte.
117    let index ≝ sfr_8051_index i in
118    let old_code_memory ≝ code_memory s in
119    let old_low_internal_ram ≝ low_internal_ram s in
120    let old_high_internal_ram ≝ high_internal_ram s in
121    let old_external_ram ≝ external_ram s in
122    let old_program_counter ≝ program_counter s in
123    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
124    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
125    let new_special_function_registers_8051 ≝
126      cic:/matita/ng/Vector/set_index.fix(0,3,2) Byte nineteen old_special_function_registers_8051 index b ? in
127      mk_Status old_code_memory
128                old_low_internal_ram
129                old_high_internal_ram
130                old_external_ram
131                old_program_counter
132                new_special_function_registers_8051
133                old_special_function_registers_8052.
134    napply (sfr8051_index_nineteen i).
135nqed.
136
137ndefinition set_8052_sfr ≝
138  λs: Status.
139  λi: SFR8052.
140  λb: Byte.
141    let index ≝ sfr_8052_index i in
142    let old_code_memory ≝ code_memory s in
143    let old_low_internal_ram ≝ low_internal_ram s in
144    let old_high_internal_ram ≝ high_internal_ram s in
145    let old_external_ram ≝ external_ram s in
146    let old_program_counter ≝ program_counter s in
147    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
148    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
149    let new_special_function_registers_8052 ≝
150      cic:/matita/ng/Vector/set_index.fix(0,3,2) Byte five old_special_function_registers_8052 index b ? in
151      mk_Status old_code_memory
152                old_low_internal_ram
153                old_high_internal_ram
154                old_external_ram
155                old_program_counter
156                old_special_function_registers_8051
157                new_special_function_registers_8052.
158    napply (sfr8052_index_five i).
159nqed.
160
161ndefinition set_program_counter ≝
162  λs: Status.
163  λi: SFR8052.
164  λw: Word.
165    let index ≝ sfr_8052_index i in
166    let old_code_memory ≝ code_memory s in
167    let old_low_internal_ram ≝ low_internal_ram s in
168    let old_high_internal_ram ≝ high_internal_ram s in
169    let old_external_ram ≝ external_ram s in
170    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
171    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
172      mk_Status old_code_memory
173                old_low_internal_ram
174                old_high_internal_ram
175                old_external_ram
176                w
177                old_special_function_registers_8051
178                old_special_function_registers_8052.
179               
180ndefinition set_code_memory ≝
181  λs: Status.
182  λi: SFR8052.
183  λr: BitVectorTrie Byte sixteen.
184    let index ≝ sfr_8052_index i in
185    let old_low_internal_ram ≝ low_internal_ram s in
186    let old_high_internal_ram ≝ high_internal_ram s in
187    let old_external_ram ≝ external_ram s in
188    let old_program_counter ≝ program_counter s in
189    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
190    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
191      mk_Status r
192                old_low_internal_ram
193                old_high_internal_ram
194                old_external_ram
195                old_program_counter
196                old_special_function_registers_8051
197                old_special_function_registers_8052.
198               
199ndefinition set_low_internal_ram ≝
200  λs: Status.
201  λi: SFR8052.
202  λr: BitVectorTrie Byte seven.
203    let index ≝ sfr_8052_index i in
204    let old_code_memory ≝ code_memory s in
205    let old_high_internal_ram ≝ high_internal_ram s in
206    let old_external_ram ≝ external_ram s in
207    let old_program_counter ≝ program_counter s in
208    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
209    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
210      mk_Status old_code_memory
211                r
212                old_high_internal_ram
213                old_external_ram
214                old_program_counter
215                old_special_function_registers_8051
216                old_special_function_registers_8052.
217               
218naxiom less_than_or_equal_monotone:
219  ∀m, n: Nat.
220    m ≤ n → S m ≤ S n.
221   
222alias id "get_index" = "cic:/matita/ng/Vector/get_index.fix(0,3,2)".
223               
224ndefinition get_cy_flag ≝
225  λs: Status.
226    let sfr ≝ special_function_registers_8051 s in
227    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
228      get_index Bool eight psw Z ?.
229    nnormalize.
230    napply (less_than_or_equal_monotone ? ?).
231    napply (less_than_or_equal_zero).
232    nrepeat (napply (less_than_or_equal_monotone ? ?)).
233    napply (less_than_or_equal_zero).
234nqed.
235
236ndefinition get_ac_flag ≝
237  λs: Status.
238    let sfr ≝ special_function_registers_8051 s in
239    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
240      get_index Bool eight psw (S Z) ?.
241    nnormalize.
242    nrepeat (napply (less_than_or_equal_monotone ? ?)).
243    napply (less_than_or_equal_zero).
244    nrepeat (napply (less_than_or_equal_monotone ? ?)).
245    napply (less_than_or_equal_zero).
246nqed.
247
248ndefinition get_fo_flag ≝
249  λs: Status.
250    let sfr ≝ special_function_registers_8051 s in
251    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
252      get_index Bool eight psw two ?.
253    nnormalize.
254    nrepeat (napply (less_than_or_equal_monotone ? ?)).
255    napply (less_than_or_equal_zero).
256    nrepeat (napply (less_than_or_equal_monotone ? ?)).
257    napply (less_than_or_equal_zero).
258nqed.
259
260ndefinition get_rs1_flag ≝
261  λs: Status.
262    let sfr ≝ special_function_registers_8051 s in
263    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
264      get_index Bool eight psw three ?.
265    nnormalize.
266    nrepeat (napply (less_than_or_equal_monotone ? ?)).
267    napply (less_than_or_equal_zero).
268    nrepeat (napply (less_than_or_equal_monotone ? ?)).
269    napply (less_than_or_equal_zero).
270nqed.
271
272ndefinition get_rs0_flag ≝
273  λs: Status.
274    let sfr ≝ special_function_registers_8051 s in
275    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
276      get_index Bool eight psw four ?.
277    nnormalize.
278    nrepeat (napply (less_than_or_equal_monotone ? ?)).
279    napply (less_than_or_equal_zero).
280    nrepeat (napply (less_than_or_equal_monotone ? ?)).
281    napply (less_than_or_equal_zero).
282nqed.
283
284ndefinition get_ov_flag ≝
285  λs: Status.
286    let sfr ≝ special_function_registers_8051 s in
287    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
288      get_index Bool eight psw five ?.
289    nnormalize.
290    nrepeat (napply (less_than_or_equal_monotone ? ?)).
291    napply (less_than_or_equal_zero).
292    nrepeat (napply (less_than_or_equal_monotone ? ?)).
293    napply (less_than_or_equal_zero).
294nqed.
295
296ndefinition get_ud_flag ≝
297  λs: Status.
298    let sfr ≝ special_function_registers_8051 s in
299    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
300      get_index Bool eight psw six ?.
301    nnormalize.
302    nrepeat (napply (less_than_or_equal_monotone ? ?)).
303    napply (less_than_or_equal_zero).
304    nrepeat (napply (less_than_or_equal_monotone ? ?)).
305    napply (less_than_or_equal_zero).
306nqed.
307
308ndefinition get_p_flag ≝
309  λs: Status.
310    let sfr ≝ special_function_registers_8051 s in
311    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
312      get_index Bool eight psw seven ?.
313    nnormalize.
314    nrepeat (napply (less_than_or_equal_monotone ? ?)).
315    napply (less_than_or_equal_zero).
316    nrepeat (napply (less_than_or_equal_monotone ? ?)).
317    napply (less_than_or_equal_zero).
318nqed.
319               
320ndefinition set_high_internal_ram ≝
321  λs: Status.
322  λi: SFR8052.
323  λr: BitVectorTrie Byte seven.
324    let index ≝ sfr_8052_index i in
325    let old_code_memory ≝ code_memory s in
326    let old_low_internal_ram ≝ low_internal_ram s in
327    let old_high_internal_ram ≝ high_internal_ram s in
328    let old_external_ram ≝ external_ram s in
329    let old_program_counter ≝ program_counter s in
330    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
331    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
332      mk_Status old_code_memory
333                old_low_internal_ram
334                r
335                old_external_ram
336                old_program_counter
337                old_special_function_registers_8051
338                old_special_function_registers_8052.
339
340ndefinition initialise_status ≝
341  let status ≝ mk_Status (Stub Byte sixteen)
342                         (Stub Byte seven)
343                         (Stub Byte seven)
344                         (Stub Byte sixteen)
345                         (zero sixteen)
346                         (replicate Byte nineteen (zero eight))
347                         (replicate Byte five (zero eight)) in
348  status.
Note: See TracBrowser for help on using the repository browser.