source: Deliverables/D4.1/Matita/Fetch.ma @ 318

Last change on this file since 318 was 318, checked in by sacerdot, 10 years ago

First version: to be debugged.

File size: 15.7 KB
Line 
1include "BitVectorTrie.ma".
2include "Arithmetic.ma".
3include "ASM.ma".
4
5ndefinition next: BitVectorTrie Byte sixteen → Word → Word × Byte ≝
6 λpmem,pc.
7  let 〈x,res〉 ≝ half_add ? pc (bitvector_of_nat sixteen (S Z)) in
8   〈res, lookup … pc pmem (zero eight)〉.
9
10(* timings taken from SIEMENS *)
11
12ndefinition fetch: BitVectorTrie Byte sixteen → Word → instruction × Word × Nat ≝
13 λpmem,pc.
14  let 〈pc,v〉 ≝ next pmem pc in
15  let 〈v1,v2〉 ≝ split … three five v in
16   if eqv … v2 [[true;false;false;false;true]] then
17    let 〈pc,b1〉 ≝ next pmem pc in
18     〈〈ACALL … (ADDR11 (v1 @@ b1)), pc〉, two〉
19   else if eqv … v2 [[false;false;false;false;true]] then
20    let 〈pc,b1〉 ≝ next pmem pc in
21     〈〈AJMP … (ADDR11 (v1 @@ b1)), pc〉, two〉
22   else
23   let 〈b,v〉≝ head8 v in if b then
24    let 〈b,v〉≝ head8 v in if b then
25     let 〈b,v〉≝ head8 v in if b then
26      let 〈b,v〉≝ head8 v in if b then
27       let 〈b,v〉≝ head8 v in if b then
28        〈〈MOV (U2 (REGISTER v, ACC_A)), pc〉, one〉
29       else
30        let 〈b,v〉≝ head8 v in if b then
31         let 〈b,v〉≝ head8 v in if b then
32          〈〈MOV (U2 (INDIRECT v, ACC_A)), pc〉, one〉
33         else
34          let 〈b,v〉≝ head8 v in if b then
35           let pc,b1 = next pc in 〈〈MOV (U3 (DIRECT b1, ACC_A)), pc〉, one〉
36          else
37           〈〈CPL ACC_A, pc〉, one〉
38        else
39         let 〈b,v〉≝ head8 v in if b then
40          〈〈MOVX (U2 (EXT_INDIRECT v, ACC_A)), pc〉, two〉
41         else
42          let 〈b,v〉≝ head8 v in if b then
43           assert false
44          else
45           〈〈MOVX (U2 (EXT_IND_DPTR, ACC_A)), pc〉, two〉
46      else
47       let 〈b,v〉≝ head8 v in if b then
48        〈〈MOV (U1 (A, REGISTER v)), pc〉, one〉
49       else
50        let 〈b,v〉≝ head8 v in if b then
51         let 〈b,v〉≝ head8 v in if b then
52          〈〈MOV (U1 (A, INDIRECT v)), pc〉, one〉
53         else
54          let 〈b,v〉≝ head8 v in if b then
55           let pc,b1 = next pc in 〈〈MOV (U1 (A, DIRECT b1)), pc〉, one〉
56          else
57           〈〈CLR ACC_A, pc〉, one〉
58        else
59         let 〈b,v〉≝ head8 v in if b then
60          〈〈MOVX (U1 (A, EXT_INDIRECT v)), pc〉, two〉
61         else
62          let 〈b,v〉≝ head8 v in if b then
63           assert false
64          else
65           〈〈MOVX (U1 (A, EXT_IND_DPTR)), pc〉, two〉
66     else
67      let 〈b,v〉≝ head8 v in if b then
68       let 〈b,v〉≝ head8 v in if b then
69        let pc,b1 = next pc in 〈〈DJNZ (REGISTER v, REL b1), pc〉, two〉
70       else
71        let 〈b,v〉≝ head8 v in if b then
72         let 〈b,v〉≝ head8 v in if b then
73          〈〈XCHD(A, INDIRECT v), pc〉, one〉
74         else
75          let 〈b,v〉≝ head8 v in if b then
76           let pc,b1 = next pc in let pc,b2 = next pc in 〈〈DJNZ (DIRECT b1, REL b2), pc〉, two〉
77          else
78           〈〈DA ACC_A, pc〉, one〉
79        else
80         let 〈b,v〉≝ head8 v in if b then
81          let 〈b,v〉≝ head8 v in if b then
82           〈〈SETB C, pc〉, one〉
83          else
84           let pc,b1 = next pc in 〈〈SETB (BIT b1), pc〉, one〉
85         else
86          let 〈b,v〉≝ head8 v in if b then
87           assert false
88          else
89           let pc,b1 = next pc in 〈〈POP (DIRECT b1), pc〉, two〉
90      else
91       let 〈b,v〉≝ head8 v in if b then
92        〈〈XCH (A, REGISTER v), pc〉, one〉
93       else
94        let 〈b,v〉≝ head8 v in if b then
95         let 〈b,v〉≝ head8 v in if b then
96          〈〈XCH (A, INDIRECT v), pc〉, one〉
97         else
98          let 〈b,v〉≝ head8 v in if b then
99           let pc,b1 = next pc in 〈〈XCH (A, DIRECT b1), pc〉, one〉
100          else
101           〈〈SWAP ACC_A, pc〉, one〉
102        else
103         let 〈b,v〉≝ head8 v in if b then
104          let 〈b,v〉≝ head8 v in if b then
105           〈〈CLR C, pc〉, one〉
106          else
107           let pc,b1 = next pc in 〈〈CLR (BIT b1), pc〉, one〉
108         else
109          let 〈b,v〉≝ head8 v in if b then
110           assert false
111          else
112           let pc,b1 = next pc in 〈〈PUSH (DIRECT b1), pc〉, two〉
113    else
114     let 〈b,v〉≝ head8 v in if b then
115      let 〈b,v〉≝ head8 v in if b then
116       let 〈b,v〉≝ head8 v in if b then
117        let pc,b1 = next pc in let pc,b2 = next pc in 〈〈CJNE (U2 (REGISTER v, DATA b1), REL b2), pc〉, two〉
118       else
119        let 〈b,v〉≝ head8 v in if b then
120         let 〈b,v〉≝ head8 v in if b then
121          let pc,b1 = next pc in let pc,b2 = next pc in 〈〈CJNE (U2 (INDIRECT v, DATA b1), REL b2), pc〉, two〉
122         else
123          let 〈b,v〉≝ head8 v in if b then
124           let pc,b1 = next pc in let pc,b2 = next pc in 〈〈CJNE (U1 (A, DIRECT b1), REL b2), pc〉, two〉
125          else
126           let pc,b1 = next pc in let pc,b2 = next pc in 〈〈CJNE (U1 (A, DATA b1), REL b2), pc〉, two〉
127        else
128         let 〈b,v〉≝ head8 v in if b then
129          let 〈b,v〉≝ head8 v in if b then
130           〈〈CPL C, pc〉, one〉
131          else
132           let pc,b1 = next pc in 〈〈CPL (BIT b1), pc〉, one〉
133         else
134          let 〈b,v〉≝ head8 v in if b then
135           assert false
136          else
137           let pc,b1 = next pc in 〈〈ANL (U3 (C,NBIT b1)), pc〉, two〉
138      else
139       let 〈b,v〉≝ head8 v in if b then
140        let pc,b1 = next pc in 〈〈MOV (U2 (REGISTER v, (DIRECT b1))), pc〉, two〉
141       else
142        let 〈b,v〉≝ head8 v in if b then
143         let 〈b,v〉≝ head8 v in if b then
144          let pc,b1 = next pc in 〈〈MOV (U2 (INDIRECT v, DIRECT b1)), pc〉, two〉
145         else
146          〈〈MUL(A, B), pc〉, four〉
147        else
148         let 〈b,v〉≝ head8 v in if b then
149          let 〈b,v〉≝ head8 v in if b then
150           〈〈INC DPTR, pc〉, two〉
151          else
152           let pc,b1 = next pc in 〈〈MOV (U5 (C, BIT b1)), pc〉, one〉
153         else
154          let 〈b,v〉≝ head8 v in if b then
155           assert false
156          else
157           let pc,b1 = next pc in 〈〈ORL (U3 (C, NBIT b1)), pc〉, two〉
158     else
159      let 〈b,v〉≝ head8 v in if b then
160       let 〈b,v〉≝ head8 v in if b then
161        〈〈SUBB (A, REGISTER v), pc〉, one〉
162       else
163        let 〈b,v〉≝ head8 v in if b then
164         let 〈b,v〉≝ head8 v in if b then
165          〈〈SUBB (A, INDIRECT v), pc〉, one〉
166         else
167          let 〈b,v〉≝ head8 v in if b then
168           let pc,b1 = next pc in 〈〈SUBB (A, DIRECT b1), pc〉, one〉
169          else
170           let pc,b1 = next pc in 〈〈SUBB (A, DATA b1), pc〉, one〉
171        else
172         let 〈b,v〉≝ head8 v in if b then
173          let 〈b,v〉≝ head8 v in if b then
174           〈〈MOVC (A, ACC_A_DPTR), pc〉, two〉
175          else
176           let pc,b1 = next pc in 〈〈MOV (U6 (BIT b1, C)), pc〉, two〉
177         else
178          let 〈b,v〉≝ head8 v in if b then
179           assert false
180          else
181           let pc,b1 = next pc in let pc,b2 = next pc in 〈〈MOV (U4 (DPTR, DATA16(mk_word b1 b2))), pc〉, two〉
182      else
183       let 〈b,v〉≝ head8 v in if b then
184        let pc,b1 = next pc in 〈〈MOV (U3 (DIRECT b1, REGISTER v)), pc〉, two〉
185       else
186        let 〈b,v〉≝ head8 v in if b then
187         let 〈b,v〉≝ head8 v in if b then
188          let pc,b1 = next pc in 〈〈MOV (U3 (DIRECT b1, INDIRECT v)), pc〉, two〉
189         else
190          let 〈b,v〉≝ head8 v in if b then
191           let pc,b1 = next pc in let pc,b2 = next pc in 〈〈MOV (U3 (DIRECT b1, DIRECT b2)), pc〉, two〉
192          else
193           〈〈DIV (A, B), pc〉, four〉
194        else
195         let 〈b,v〉≝ head8 v in if b then
196          let 〈b,v〉≝ head8 v in if b then
197           〈〈MOVC (A, ACC_A_PC), pc〉, two〉
198          else
199           let pc,b1 = next pc in 〈〈ANL (U3 (C,BIT b1)), pc〉, two〉
200         else
201          let 〈b,v〉≝ head8 v in if b then
202           assert false
203          else
204           let pc,b1 = next pc in 〈〈SJMP (REL b1), pc〉, two〉
205   else
206    let 〈b,v〉≝ head8 v in if b then
207     let 〈b,v〉≝ head8 v in if b then
208      let 〈b,v〉≝ head8 v in if b then
209       let 〈b,v〉≝ head8 v in if b then
210        let pc,b1 = next pc in 〈〈MOV (U2 (REGISTER v, (DATA b1))), pc〉, one〉
211       else
212        let 〈b,v〉≝ head8 v in if b then
213         let 〈b,v〉≝ head8 v in if b then
214          let pc,b1 = next pc in 〈〈MOV (U2 (INDIRECT v, DATA b1)), pc〉, one〉
215         else
216          let 〈b,v〉≝ head8 v in if b then
217           let pc,b1 = next pc in let pc,b2 = next pc in 〈〈MOV (U3 (DIRECT b1, DATA b2)), pc〉, three〉
218          else
219           let pc,b1 = next pc in 〈〈MOV (U1 (A, DATA b1)), pc〉, one〉
220        else
221         let 〈b,v〉≝ head8 v in if b then
222          let 〈b,v〉≝ head8 v in if b then
223           〈〈JMP IND_DPTR, pc〉, two〉
224          else
225           let pc,b1 = next pc in 〈〈ORL (U3 (C, BIT b1)), pc〉, two〉
226         else
227          let 〈b,v〉≝ head8 v in if b then
228           assert false
229          else
230           let pc,b1 = next pc in 〈〈JNZ (REL b1), pc〉, two〉
231      else
232       let 〈b,v〉≝ head8 v in if b then
233        〈〈XRL(U1(A, REGISTER v)), pc〉, one〉
234       else
235        let 〈b,v〉≝ head8 v in if b then
236         let 〈b,v〉≝ head8 v in if b then
237          〈〈XRL(U1(A, INDIRECT v)), pc〉, one〉
238         else
239          let 〈b,v〉≝ head8 v in if b then
240           let pc,b1 = next pc in 〈〈XRL(U1(A, DIRECT b1)), pc〉, one〉
241          else
242           let pc,b1 = next pc in 〈〈XRL(U1(A, DATA b1)), pc〉, one〉
243        else
244         let 〈b,v〉≝ head8 v in if b then
245          let 〈b,v〉≝ head8 v in if b then
246           let pc,b1 = next pc in let pc,b2 = next pc in 〈〈XRL(U2(DIRECT b1, DATA b2)), pc〉, two〉
247          else
248           let pc,b1 = next pc in 〈〈XRL(U2(DIRECT b1, ACC_A)), pc〉, one〉
249         else
250          let 〈b,v〉≝ head8 v in if b then
251           assert false
252          else
253           let pc,b1 = next pc in 〈〈JZ (REL b1), pc〉, two〉
254     else
255      let 〈b,v〉≝ head8 v in if b then
256       let 〈b,v〉≝ head8 v in if b then
257        〈〈ANL (U1 (A, REGISTER v)), pc〉, one〉
258       else
259        let 〈b,v〉≝ head8 v in if b then
260         let 〈b,v〉≝ head8 v in if b then
261          〈〈ANL (U1 (A, INDIRECT v)), pc〉, one〉
262         else
263          let 〈b,v〉≝ head8 v in if b then
264           let pc,b1 = next pc in 〈〈ANL (U1 (A, DIRECT b1)), pc〉, one〉
265          else
266           let pc,b1 = next pc in 〈〈ANL (U1 (A, DATA b1)), pc〉, one〉
267        else
268         let 〈b,v〉≝ head8 v in if b then
269          let 〈b,v〉≝ head8 v in if b then
270           let pc,b1 = next pc in let pc,b2 = next pc in 〈〈ANL (U2 (DIRECT b1,DATA b2)), pc〉, two〉
271          else
272           let pc,b1 = next pc in 〈〈ANL (U2 (DIRECT b1,A)), pc〉, one〉
273         else
274          let 〈b,v〉≝ head8 v in if b then
275           assert false
276          else
277           let pc,b1 = next pc in 〈〈JNC (REL b1), pc〉, two〉
278      else
279       let 〈b,v〉≝ head8 v in if b then
280        〈〈ORL (U1(A, REGISTER v)), pc〉, one〉
281       else
282        let 〈b,v〉≝ head8 v in if b then
283         let 〈b,v〉≝ head8 v in if b then
284          〈〈ORL (U1(A, INDIRECT v)), pc〉, one〉
285         else
286          let 〈b,v〉≝ head8 v in if b then
287           let pc,b1 = next pc in 〈〈ORL (U1(A, DIRECT b1)), pc〉, one〉
288          else
289           let pc,b1 = next pc in 〈〈ORL (U1(A, DATA b1)), pc〉, one〉
290        else
291         let 〈b,v〉≝ head8 v in if b then
292          let 〈b,v〉≝ head8 v in if b then
293           let pc,b1 = next pc in let pc,b2 = next pc in 〈〈ORL (U2 (DIRECT b1, DATA b2)), pc〉, two〉
294          else
295           let pc,b1 = next pc in 〈〈ORL (U2(DIRECT b1, ACC_A)), pc〉, one〉
296         else
297          let 〈b,v〉≝ head8 v in if b then
298           assert false
299          else
300           let pc,b1 = next pc in 〈〈JC (REL b1), pc〉, two〉
301    else
302     let 〈b,v〉≝ head8 v in if b then
303      let 〈b,v〉≝ head8 v in if b then
304       let 〈b,v〉≝ head8 v in if b then
305        〈〈ADDC (A,REGISTER v), pc〉, one〉
306       else
307        let 〈b,v〉≝ head8 v in if b then
308         let 〈b,v〉≝ head8 v in if b then
309          〈〈ADDC (A,INDIRECT v), pc〉, one〉
310         else
311          let 〈b,v〉≝ head8 v in if b then
312           let pc,b1 = next pc in 〈〈ADDC (A,DIRECT b1), pc〉, one〉
313          else
314           let pc,b1 = next pc in 〈〈ADDC (A,DATA b1), pc〉, one〉
315        else
316         let 〈b,v〉≝ head8 v in if b then
317          let 〈b,v〉≝ head8 v in if b then
318           〈〈RLC ACC_A, pc〉, one〉
319          else
320           〈〈RETI, pc〉, two〉
321         else
322          let 〈b,v〉≝ head8 v in if b then
323           assert false
324          else
325           let pc,b1 = next pc in let pc,b2 = next pc in 〈〈JNB (BIT b1, REL b2), pc〉, two〉
326      else
327       let 〈b,v〉≝ head8 v in if b then
328        〈〈ADD (A,REGISTER v), pc〉, one〉
329       else
330        let 〈b,v〉≝ head8 v in if b then
331         let 〈b,v〉≝ head8 v in if b then
332          〈〈ADD (A,INDIRECT v), pc〉, one〉
333         else
334          let 〈b,v〉≝ head8 v in if b then
335           let pc,b1 = next pc in 〈〈ADD (A,DIRECT b1), pc〉, one〉
336          else
337           let pc,b1 = next pc in 〈〈ADD (A,DATA b1), pc〉, one〉
338        else
339         let 〈b,v〉≝ head8 v in if b then
340          let 〈b,v〉≝ head8 v in if b then
341           〈〈RL ACC_A, pc〉, one〉
342          let 〈b,v〉≝ head8 v in if b then
343          else
344           〈〈RET, pc〉, two〉
345         else
346          let 〈b,v〉≝ head8 v in if b then
347           assert false
348          else
349           let pc,b1 = next pc in let pc,b2 = next pc in 〈〈JB (BIT b1, REL b2), pc〉, two〉
350     else
351      let 〈b,v〉≝ head8 v in if b then
352       let 〈b,v〉≝ head8 v in if b then
353        〈〈DEC (REGISTER v), pc〉, one〉
354       else
355        let 〈b,v〉≝ head8 v in if b then
356         let 〈b,v〉≝ head8 v in if b then
357          〈〈DEC (INDIRECT v), pc〉, one〉
358         else
359          let 〈b,v〉≝ head8 v in if b then
360           let pc,b1 = next pc in 〈〈DEC (DIRECT b1), pc〉, one〉
361          else
362           〈〈DEC ACC_A, pc〉, one〉
363        else
364         let 〈b,v〉≝ head8 v in if b then
365          let 〈b,v〉≝ head8 v in if b then
366           〈〈RRC ACC_A, pc〉, one〉
367          else
368           let pc,b1 = next pc in let pc,b2 = next pc in 〈〈LCALL (ADDR16 (mk_word b1 b2)), pc〉, two〉
369         else
370          let 〈b,v〉≝ head8 v in if b then
371           assert false
372          else
373           let pc,b1 = next pc in let pc,b2 = next pc in 〈〈JBC (BIT b1, REL b2), pc〉, two〉
374      else
375       let 〈b,v〉≝ head8 v in if b then
376        〈〈INC (REGISTER v), pc〉, one〉
377       else
378        let 〈b,v〉≝ head8 v in if b then
379         let 〈b,v〉≝ head8 v in if b then
380          〈〈INC (INDIRECT v), pc〉, one〉
381         else
382          let 〈b,v〉≝ head8 v in if b then
383           let pc,b1 = next pc in 〈〈INC (DIRECT b1), pc〉, one〉
384          else
385           〈〈INC ACC_A, pc〉, one〉
386        else
387         let 〈b,v〉≝ head8 v in if b then
388          let 〈b,v〉≝ head8 v in if b then
389           〈〈RR ACC_A, pc〉, one〉
390          else
391           let pc,b1 = next pc in let pc,b2 = next pc in 〈〈LJMP (ADDR16 (mk_word b1 b2)), pc〉, two〉
392         else
393          let 〈b,v〉≝ head8 v in if b then
394           assert false
395          else
396           〈〈NOP, pc〉, one〉.
397 @.
398nqed.
Note: See TracBrowser for help on using the repository browser.