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

Last change on this file since 322 was 322, checked in by sacerdot, 9 years ago

More work on fetch.

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