source: Deliverables/D4.1/Matita/Interpret.ma @ 266

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

Changes to bitvector.
File size: 8.5 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
87ncheck special_function_registers_8051.
88
89naxiom sfr8051_index_nineteen:
90  ∀i: SFR8051.
91    sfr_8051_index i < nineteen.
92   
93naxiom sfr8052_index_five:
94  ∀i: SFR8052.
95    sfr_8052_index i < five.
96
97ndefinition get_8051_sfr ≝
98  λs: Status.
99  λi: SFR8051.
100    let sfr ≝ special_function_registers_8051 s in
101    let index ≝ sfr_8051_index i in
102      get_index … sfr index ?.
103    napply (sfr8051_index_nineteen i).
104nqed.
105
106ndefinition get_8052_sfr ≝
107  λs: Status.
108  λi: SFR8052.
109    let sfr ≝ special_function_registers_8052 s in
110    let index ≝ sfr_8052_index i in
111      get_index … sfr index ?.
112    napply (sfr8052_index_five i).
113nqed.
114
115ndefinition set_8051_sfr ≝
116  λs: Status.
117  λi: SFR8051.
118  λb: Byte.
119    let index ≝ sfr_8051_index i in
120    let old_code_memory ≝ code_memory s in
121    let old_low_internal_ram ≝ low_internal_ram s in
122    let old_high_internal_ram ≝ high_internal_ram s in
123    let old_external_ram ≝ external_ram s in
124    let old_program_counter ≝ program_counter s in
125    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
126    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
127    let new_special_function_registers_8051 ≝
128      cic:/matita/ng/Vector/set_index.fix(0,3,2) Byte nineteen old_special_function_registers_8051 index b ? in
129      mk_Status old_code_memory
130                old_low_internal_ram
131                old_high_internal_ram
132                old_external_ram
133                old_program_counter
134                new_special_function_registers_8051
135                old_special_function_registers_8052.
136    napply (sfr8051_index_nineteen i).
137nqed.
138
139ndefinition set_8052_sfr ≝
140  λs: Status.
141  λi: SFR8052.
142  λb: Byte.
143    let index ≝ sfr_8052_index i in
144    let old_code_memory ≝ code_memory s in
145    let old_low_internal_ram ≝ low_internal_ram s in
146    let old_high_internal_ram ≝ high_internal_ram s in
147    let old_external_ram ≝ external_ram s in
148    let old_program_counter ≝ program_counter s in
149    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
150    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
151    let new_special_function_registers_8052 ≝
152      cic:/matita/ng/Vector/set_index.fix(0,3,2) Byte five old_special_function_registers_8052 index b ? in
153      mk_Status old_code_memory
154                old_low_internal_ram
155                old_high_internal_ram
156                old_external_ram
157                old_program_counter
158                old_special_function_registers_8051
159                new_special_function_registers_8052.
160    napply (sfr8052_index_five i).
161nqed.
162
163ndefinition set_program_counter ≝
164  λs: Status.
165  λi: SFR8052.
166  λw: Word.
167    let index ≝ sfr_8052_index i in
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_special_function_registers_8051 ≝ special_function_registers_8051 s in
173    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
174      mk_Status old_code_memory
175                old_low_internal_ram
176                old_high_internal_ram
177                old_external_ram
178                w
179                old_special_function_registers_8051
180                old_special_function_registers_8052.
181               
182ndefinition set_code_memory ≝
183  λs: Status.
184  λi: SFR8052.
185  λr: BitVectorTrie Byte sixteen.
186    let index ≝ sfr_8052_index i in
187    let old_low_internal_ram ≝ low_internal_ram s in
188    let old_high_internal_ram ≝ high_internal_ram s in
189    let old_external_ram ≝ external_ram s in
190    let old_program_counter ≝ program_counter s in
191    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
192    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
193      mk_Status r
194                old_low_internal_ram
195                old_high_internal_ram
196                old_external_ram
197                old_program_counter
198                old_special_function_registers_8051
199                old_special_function_registers_8052.
200               
201ndefinition set_low_internal_ram ≝
202  λs: Status.
203  λi: SFR8052.
204  λr: BitVectorTrie Byte seven.
205    let index ≝ sfr_8052_index i in
206    let old_code_memory ≝ code_memory s in
207    let old_high_internal_ram ≝ high_internal_ram s in
208    let old_external_ram ≝ external_ram s in
209    let old_program_counter ≝ program_counter s in
210    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
211    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
212      mk_Status old_code_memory
213                r
214                old_high_internal_ram
215                old_external_ram
216                old_program_counter
217                old_special_function_registers_8051
218                old_special_function_registers_8052.
219               
220ndefinition get_cy_flag ≝
221  λs: Status.
222    let sfr ≝ special_function_registers_8051 s in
223    let psw ≝ get_index … (sfr_8051_index SFR_PSW) s ? in
224      get_index … Z psw ?.
225               
226ndefinition set_high_internal_ram ≝
227  λs: Status.
228  λi: SFR8052.
229  λr: BitVectorTrie Byte seven.
230    let index ≝ sfr_8052_index i in
231    let old_code_memory ≝ code_memory s in
232    let old_low_internal_ram ≝ low_internal_ram s in
233    let old_high_internal_ram ≝ high_internal_ram s in
234    let old_external_ram ≝ external_ram s in
235    let old_program_counter ≝ program_counter s in
236    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
237    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
238      mk_Status old_code_memory
239                old_low_internal_ram
240                r
241                old_external_ram
242                old_program_counter
243                old_special_function_registers_8051
244                old_special_function_registers_8052.
245
246ndefinition initialise_status ≝
247  let status ≝ mk_Status (Stub Byte sixteen)
248                         (Stub Byte seven)
249                         (Stub Byte seven)
250                         (Stub Byte sixteen)
251                         (zero sixteen)
252                         (replicate Byte nineteen (zero eight))
253                         (replicate Byte five (zero eight)) in
254  status.
Note: See TracBrowser for help on using the repository browser.