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

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

REGISTER now takes a BitVector? 3

File size: 16.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
10ndefinition fetch: BitVectorTrie Byte sixteen → Word → instruction × Word × Nat ≝
11 λpmem,pc.
12  let 〈pc,instr〉 ≝ next pmem pc in
13  let 〈instr1,instr2〉 ≝ split … three five instr in
14   if eqv … instr2 [[true;false;false;false;true]] then
15    let 〈pc,b1〉 ≝ next pmem pc in
16     〈〈ACALL … (ADDR11 (instr1 @@ b1)), pc〉, two〉
17   else
18    〈〈NOP …, pc〉, two〉.
19 @.
20nqed.
21   
22
23(*
24(* timings taken from SIEMENS *)
25
26let fetch pmem pc =
27 let next pc =
28   let _carry, res = half_add pc (vect_of_int 1 `Sixteen) in
29     res, WordMap.find pc pmem
30 in
31 let pc,instr = next pc in
32 let un, ln = from_byte instr in
33 let bits = (from_nibble un, from_nibble ln) in
34  match bits with
35     (a10,a9,a8,true),(false,false,false,true) ->
36      let pc,b1 = next pc in
37       `ACALL (`ADDR11 (mk_word11 a10 a9 a8 b1)), pc, 2
38   | (false,false,true,false),(true,r1,r2,r3) ->
39       `ADD (`A,`REG (r1,r2,r3)), pc, 1
40   | (false,false,true,false),(false,true,false,true) ->
41      let pc,b1 = next pc in
42       `ADD (`A,`DIRECT b1), pc, 1
43   | (false,false,true,false),(false,true,true,i1) ->
44       `ADD (`A,`INDIRECT i1), pc, 1
45   | (false,false,true,false),(false,true,false,false) ->
46      let pc,b1 = next pc in
47       `ADD (`A,`DATA b1), pc, 1
48   | (false,false,true,true),(true,r1,r2,r3) ->
49       `ADDC (`A,`REG (r1,r2,r3)), pc, 1
50   | (false,false,true,true),(false,true,false,true) ->
51      let pc,b1 = next pc in
52       `ADDC (`A,`DIRECT b1), pc, 1
53   | (false,false,true,true),(false,true,true,i1) ->
54       `ADDC (`A,`INDIRECT i1), pc, 1
55   | (false,false,true,true),(false,true,false,false) ->
56      let pc,b1 = next pc in
57       `ADDC (`A,`DATA b1), pc, 1
58   | (a10,a9,a8,false),(false,false,false,true) ->
59      let pc,b1 = next pc in
60       `AJMP (`ADDR11 (mk_word11 a10 a9 a8 b1)), pc, 2
61   | (false,true,false,true),(true,r1,r2,r3) ->
62       `ANL (`U1 (`A, `REG (r1,r2,r3))), pc, 1
63   | (false,true,false,true),(false,true,false,true) ->
64      let pc,b1 = next pc in
65       `ANL (`U1 (`A, `DIRECT b1)), pc, 1
66   | (false,true,false,true),(false,true,true,i1) ->
67       `ANL (`U1 (`A, `INDIRECT i1)), pc, 1
68   | (false,true,false,true),(false,true,false,false) ->
69      let pc,b1 = next pc in
70       `ANL (`U1 (`A, `DATA b1)), pc, 1
71   | (false,true,false,true),(false,false,true,false) ->
72      let pc,b1 = next pc in
73       `ANL (`U2 (`DIRECT b1,`A)), pc, 1
74   | (false,true,false,true),(false,false,true,true) ->
75      let pc,b1 = next pc in
76      let pc,b2 = next pc in
77       `ANL (`U2 (`DIRECT b1,`DATA b2)), pc, 2
78   | (true,false,false,false),(false,false,true,false) ->
79      let pc,b1 = next pc in
80       `ANL (`U3 (`C,`BIT b1)), pc, 2
81   | (true,false,true,true),(false,false,false,false) ->
82      let pc,b1 = next pc in
83       `ANL (`U3 (`C,`NBIT b1)), pc, 2
84   | (true,false,true,true),(false,true,false,true) ->
85      let       pc,b1 = next pc in
86      let pc,b2 = next pc in
87        `CJNE (`U1 (`A, `DIRECT b1), `REL b2), pc, 2
88   | (true,false,true,true),(false,true,false,false) ->
89       let pc,b1 = next pc in
90       let pc,b2 = next pc in
91         `CJNE (`U1 (`A, `DATA b1), `REL b2), pc, 2
92   | (true,false,true,true),(true,r1,r2,r3) ->
93       let pc,b1 = next pc in
94       let pc,b2 = next pc in
95         `CJNE (`U2 (`REG(r1,r2,r3), `DATA b1), `REL b2), pc, 2
96   | (true,false,true,true),(false,true,true,i1) ->
97       let pc,b1 = next pc in
98       let pc,b2 = next pc in
99         `CJNE (`U2 (`INDIRECT i1, `DATA b1), `REL b2), pc, 2
100   | (true,true,true,false),(false,true,false,false) ->
101         `CLR `A, pc, 1
102   | (true,true,false,false),(false,false,true,true) ->
103         `CLR `C, pc, 1
104   | (true,true,false,false),(false,false,true,false) ->
105       let pc,b1 = next pc in
106         `CLR (`BIT b1), pc, 1
107   | (true,true,true,true),(false,true,false,false) ->
108         `CPL `A, pc, 1
109   | (true,false,true,true),(false,false,true,true) ->
110         `CPL `C, pc, 1
111   | (true,false,true,true),(false,false,true,false) ->
112       let pc,b1 = next pc in
113         `CPL (`BIT b1), pc, 1
114   | (true,true,false,true),(false,true,false,false) ->
115         `DA `A, pc, 1
116   | (false,false,false,true),(false,true,false,false) ->
117         `DEC `A, pc, 1
118   | (false,false,false,true),(true,r1,r2,r3) ->
119         `DEC (`REG(r1,r2,r3)), pc, 1
120   | (false,false,false,true),(false,true,false,true) ->
121       let pc,b1 = next pc in
122         `DEC (`DIRECT b1), pc, 1
123   | (false,false,false,true),(false,true,true,i1) ->
124         `DEC (`INDIRECT i1), pc, 1
125   | (true,false,false,false),(false,true,false,false) ->
126         `DIV (`A, `B), pc, 4
127   | (true,true,false,true),(true,r1,r2,r3) ->
128       let pc,b1 = next pc in
129         `DJNZ (`REG(r1,r2,r3), `REL b1), pc, 2
130   | (true,true,false,true),(false,true,false,true) ->
131       let pc,b1 = next pc in
132       let pc,b2 = next pc in
133         `DJNZ (`DIRECT b1, `REL b2), pc, 2
134   | (false,false,false,false),(false,true,false,false) ->
135         `INC `A, pc, 1
136   | (false,false,false,false),(true,r1,r2,r3) ->
137         `INC (`REG(r1,r2,r3)), pc, 1
138   | (false,false,false,false),(false,true,false,true) ->
139       let pc,b1 = next pc in
140         `INC (`DIRECT b1), pc, 1
141   | (false,false,false,false),(false,true,true,i1) ->
142         `INC (`INDIRECT i1), pc, 1
143   | (true,false,true,false),(false,false,true,true) ->
144         `INC `DPTR, pc, 2
145   | (false,false,true,false),(false,false,false,false) ->
146       let pc,b1 = next pc in
147       let pc,b2 = next pc in
148         `JB (`BIT b1, `REL b2), pc, 2
149   | (false,false,false,true),(false,false,false,false) ->
150       let pc,b1 = next pc in
151       let pc,b2 = next pc in
152         `JBC (`BIT b1, `REL b2), pc, 2
153   | (false,true,false,false),(false,false,false,false) ->
154       let pc,b1 = next pc in
155         `JC (`REL b1), pc, 2
156   | (false,true,true,true),(false,false,true,true) ->
157         `JMP `IND_DPTR, pc, 2
158   | (false,false,true,true),(false,false,false,false) ->
159       let pc,b1 = next pc in
160       let pc,b2 = next pc in
161         `JNB (`BIT b1, `REL b2), pc, 2
162   | (false,true,false,true),(false,false,false,false) ->
163       let pc,b1 = next pc in
164         `JNC (`REL b1), pc, 2
165   | (false,true,true,true),(false,false,false,false) ->
166       let pc,b1 = next pc in
167         `JNZ (`REL b1), pc, 2
168   | (false,true,true,false),(false,false,false,false) ->
169       let pc,b1 = next pc in
170         `JZ (`REL b1), pc, 2
171   | (false,false,false,true),(false,false,true,false) ->
172       let pc,b1 = next pc in
173       let pc,b2 = next pc in
174         `LCALL (`ADDR16 (mk_word b1 b2)), pc, 2
175   | (false,false,false,false),(false,false,true,false) ->
176       let pc,b1 = next pc in
177       let pc,b2 = next pc in
178         `LJMP (`ADDR16 (mk_word b1 b2)), pc, 2
179   | (true,true,true,false),(true,r1,r2,r3) ->
180         `MOV (`U1 (`A, `REG(r1,r2,r3))), pc, 1
181   | (true,true,true,false),(false,true,false,true) ->
182       let pc,b1 = next pc in
183         `MOV (`U1 (`A, `DIRECT b1)), pc, 1
184   | (true,true,true,false),(false,true,true,i1) ->
185         `MOV (`U1 (`A, `INDIRECT i1)), pc, 1
186   | (false,true,true,true),(false,true,false,false) ->
187       let pc,b1 = next pc in
188         `MOV (`U1 (`A, `DATA b1)), pc, 1
189   | (true,true,true,true),(true,r1,r2,r3) ->
190         `MOV (`U2 (`REG(r1,r2,r3), `A)), pc, 1
191   | (true,false,true,false),(true,r1,r2,r3) ->
192       let pc,b1 = next pc in
193         `MOV (`U2 (`REG(r1,r2,r3), (`DIRECT b1))), pc, 2
194   | (false,true,true,true),(true,r1,r2,r3) ->
195       let pc,b1 = next pc in
196         `MOV (`U2 (`REG(r1,r2,r3), (`DATA b1))), pc, 1
197   | (true,true,true,true),(false,true,false,true) ->
198       let pc,b1 = next pc in
199         `MOV (`U3 (`DIRECT b1, `A)), pc, 1
200   | (true,false,false,false),(true,r1,r2,r3) ->
201       let pc,b1 = next pc in
202         `MOV (`U3 (`DIRECT b1, `REG(r1,r2,r3))), pc, 2
203   | (true,false,false,false),(false,true,false,true) ->
204       let pc,b1 = next pc in
205       let pc,b2 = next pc in
206         `MOV (`U3 (`DIRECT b1, `DIRECT b2)), pc, 2
207   | (true,false,false,false),(false,true,true,i1) ->
208       let pc,b1 = next pc in
209         `MOV (`U3 (`DIRECT b1, `INDIRECT i1)), pc, 2
210   | (false,true,true,true),(false,true,false,true) ->
211       let pc,b1 = next pc in
212       let pc,b2 = next pc in
213         `MOV (`U3 (`DIRECT b1, `DATA b2)), pc, 3
214   | (true,true,true,true),(false,true,true,i1) ->
215         `MOV (`U2 (`INDIRECT i1, `A)), pc, 1
216   | (true,false,true,false),(false,true,true,i1) ->
217       let pc,b1 = next pc in
218         `MOV (`U2 (`INDIRECT i1, `DIRECT b1)), pc, 2
219   | (false,true,true,true),(false,true,true,i1) ->
220       let pc,b1 = next pc in
221         `MOV (`U2 (`INDIRECT i1, `DATA b1)), pc, 1
222   | (true,false,true,false),(false,false,true,false) ->
223       let pc,b1 = next pc in
224         `MOV (`U5 (`C, `BIT b1)), pc, 1
225   | (true,false,false,true),(false,false,true,false) ->
226       let pc,b1 = next pc in
227         `MOV (`U6 (`BIT b1, `C)), pc, 2
228   | (true,false,false,true),(false,false,false,false) ->
229       let pc,b1 = next pc in
230       let pc,b2 = next pc in
231         `MOV (`U4 (`DPTR, `DATA16(mk_word b1 b2))), pc, 2
232   | (true,false,false,true),(false,false,true,true) ->
233         `MOVC (`A, `A_DPTR), pc, 2
234   | (true,false,false,false),(false,false,true,true) ->
235         `MOVC (`A, `A_PC), pc, 2
236   | (true,true,true,false),(false,false,true,i1) ->
237         `MOVX (`U1 (`A, `EXT_INDIRECT i1)), pc, 2
238   | (true,true,true,false),(false,false,false,false) ->
239         `MOVX (`U1 (`A, `EXT_IND_DPTR)), pc, 2
240   | (true,true,true,true),(false,false,true,i1) ->
241         `MOVX (`U2 (`EXT_INDIRECT i1, `A)), pc, 2
242   | (true,true,true,true),(false,false,false,false) ->
243         `MOVX (`U2 (`EXT_IND_DPTR, `A)), pc, 2
244   | (true,false,true,false),(false,true,false,false) ->
245         `MUL(`A, `B), pc, 4
246   | (false,false,false,false),(false,false,false,false) ->
247         `NOP, pc, 1
248   | (false,true,false,false),(true,r1,r2,r3) ->
249         `ORL (`U1(`A, `REG(r1,r2,r3))), pc, 1
250   | (false,true,false,false),(false,true,false,true) ->
251       let pc,b1 = next pc in
252         `ORL (`U1(`A, `DIRECT b1)), pc, 1
253   | (false,true,false,false),(false,true,true,i1) ->
254         `ORL (`U1(`A, `INDIRECT i1)), pc, 1
255   | (false,true,false,false),(false,true,false,false) ->
256       let pc,b1 = next pc in
257         `ORL (`U1(`A, `DATA b1)), pc, 1
258   | (false,true,false,false),(false,false,true,false) ->
259       let pc,b1 = next pc in
260         `ORL (`U2(`DIRECT b1, `A)), pc, 1
261   | (false,true,false,false),(false,false,true,true) ->
262       let pc,b1 = next pc in
263       let pc,b2 = next pc in
264         `ORL (`U2 (`DIRECT b1, `DATA b2)), pc, 2
265   | (false,true,true,true),(false,false,true,false) ->
266       let pc,b1 = next pc in
267         `ORL (`U3 (`C, `BIT b1)), pc, 2
268   | (true,false,true,false),(false,false,false,false) ->
269       let pc,b1 = next pc in
270         `ORL (`U3 (`C, `NBIT b1)), pc, 2
271   | (true,true,false,true),(false,false,false,false) ->
272       let pc,b1 = next pc in
273         `POP (`DIRECT b1), pc, 2
274   | (true,true,false,false),(false,false,false,false) ->
275       let pc,b1 = next pc in
276         `PUSH (`DIRECT b1), pc, 2
277   | (false,false,true,false),(false,false,true,false) ->
278         `RET, pc, 2
279   | (false,false,true,true),(false,false,true,false) ->
280         `RETI, pc, 2
281   | (false,false,true,false),(false,false,true,true) ->
282         `RL `A, pc, 1
283   | (false,false,true,true),(false,false,true,true) ->
284         `RLC `A, pc, 1
285   | (false,false,false,false),(false,false,true,true) ->
286         `RR `A, pc, 1
287   | (false,false,false,true),(false,false,true,true) ->
288         `RRC `A, pc, 1
289   | (true,true,false,true),(false,false,true,true) ->
290         `SETB `C, pc, 1
291   | (true,true,false,true),(false,false,true,false) ->
292       let pc,b1 = next pc in
293         `SETB (`BIT b1), pc, 1
294   | (true,false,false,false),(false,false,false,false) ->
295       let pc,b1 = next pc in
296         `SJMP (`REL b1), pc, 2
297   | (true,false,false,true),(true,r1,r2,r3) ->
298       `SUBB (`A, `REG(r1,r2,r3)), pc, 1
299   | (true,false,false,true),(false,true,false,true) ->
300       let pc,b1 = next pc in
301         `SUBB (`A, `DIRECT b1), pc, 1
302   | (true,false,false,true),(false,true,true,i1) ->
303         `SUBB (`A, `INDIRECT i1), pc, 1
304   | (true,false,false,true),(false,true,false,false) ->
305       let pc,b1 = next pc in
306         `SUBB (`A, `DATA b1), pc, 1
307   | (true,true,false,false),(false,true,false,false) ->
308         `SWAP `A, pc, 1
309   | (true,true,false,false),(true,r1,r2,r3) ->
310         `XCH (`A, `REG(r1,r2,r3)), pc, 1
311   | (true,true,false,false),(false,true,false,true) ->
312       let pc,b1 = next pc in
313         `XCH (`A, `DIRECT b1), pc, 1
314   | (true,true,false,false),(false,true,true,i1) ->
315         `XCH (`A, `INDIRECT i1), pc, 1
316   | (true,true,false,true),(false,true,true,i1) ->
317         `XCHD(`A, `INDIRECT i1), pc, 1
318   | (false,true,true,false),(true,r1,r2,r3) ->
319         `XRL(`U1(`A, `REG(r1,r2,r3))), pc, 1
320   | (false,true,true,false),(false,true,false,true) ->
321       let pc,b1 = next pc in
322         `XRL(`U1(`A, `DIRECT b1)), pc, 1
323   | (false,true,true,false),(false,true,true,i1) ->
324         `XRL(`U1(`A, `INDIRECT i1)), pc, 1
325   | (false,true,true,false),(false,true,false,false) ->
326       let pc,b1 = next pc in
327         `XRL(`U1(`A, `DATA b1)), pc, 1
328   | (false,true,true,false),(false,false,true,false) ->
329       let pc,b1 = next pc in
330         `XRL(`U2(`DIRECT b1, `A)), pc, 1
331   | (false,true,true,false),(false,false,true,true) ->
332       let pc,b1 = next pc in
333       let pc,b2 = next pc in
334         `XRL(`U2(`DIRECT b1, `DATA b2)), pc, 2
335   | _,_ -> assert false
336;;
337
338
339*)
340
341
342
343(*
344nrecord Sigma (A: Type[0]) (T: A → Type[0]) : Type[0] ≝ {
345   elem:> A;
346   witness: T elem
347}.
348
349interpretation "Sigma" 'sigma T = (Sigma ? T).
350
351naxiom daemon: False.
352
353naxiom decode_register: Vector Bool (S (S (S Z))) → [reg].
354naxiom decode_direct:   Vector Bool (S (S (S Z))) → [direct].
355
356ndefinition decode_tbl0: List ((Σn.Vector Bool n) × (Vector Bool (S (S (S Z))) → Instruction))
357 ≝
358 [mk_Cartesian ??
359   (mk_Sigma ? (λn.Vector Bool n) ? [ false; false; true; false; true])
360     (λl.
361       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
362             (mk_subaddressing_mode ? ?    (decode_register l) ?));
363  mk_Cartesian ??
364   (mk_Sigma ? (λn.Vector Bool n) ? [ false; false; true; false; true])
365     (λl.
366       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
367             (mk_subaddressing_mode ? ? (decode_direct l) ?)) ].
368ncases daemon.
369nqed.
370
371
372naxiom decode_register: List Bool → [reg].
373naxiom decode_direct: List Bool → [direct].
374
375ndefinition decode_tbl0: List (List Bool × (List Bool → Instruction))
376 ≝
377 [mk_Cartesian ??
378   [ false; false; true; false; true]
379     (λl.
380       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
381             (mk_subaddressing_mode ? ?    (decode_register l) ?));
382  mk_Cartesian ??
383   [ false; false; true; false; true]
384     (λl.
385       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
386             (mk_subaddressing_mode ? ? (decode_direct l) ?)) ].
387ncases daemon.
388nqed.
389
390
391ndefinition decode_tbl1:
392 List (List Bool × Σaddr:all_types. [addr] → Instruction)
393 ≝
394 [mk_Cartesian ??
395   [ false; false; true; false; true]
396   (mk_Sigma ? (λaddr:all_types. [addr] → Instruction)
397     reg
398     (λa.
399       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
400             (mk_subaddressing_mode ? ? a ?))) ].
401ncases daemon.
402nqed.
403             
404ndefinition decode_tbl2:
405 List (List Bool × Σaddr:all_types. [addr] → Instruction)
406 ≝
407 [mk_Cartesian ??
408   [ false; false; true; false; false; true; false; true]
409   (mk_Sigma ? (λaddr:all_types. [addr] → Instruction)
410     direct
411     (λa.
412       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
413             (mk_subaddressing_mode ? ?     a ?))) ].
414ncases daemon.
415nqed.
416
417ndefinition decode_tbl ≝ decode_tbl1 @ decode_tbl2.
418
419decode_addr_mode; ∀addr:all_types. List Bool → [addr].
420
421decode ≝
422 λl:List Bit.
423  List.iter
424   (fun l0 addr mk_f →
425     match split_prefix l l0 with
426      [ None ⇒ ...
427      | Some r ⇒ mk_f (decode_addr_mode r) ]
428     
429   ) decode_tbl
430
431encode ≝
432
433ndefinition decode_tbl:
434 List (List Bool × Σaddr:all_types. [addr] → Instruction)
435 ≝
436 [mk_Cartesian ??
437   [ False; False; True; False; True]
438   (mk_Sigma all_types (λaddr:all_types. [addr] → Instruction)
439     reg
440     (λa:subaddressing_mode ? [reg].
441       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
442             (mk_subaddressing_mode ? ?     a ?)));
443  mk_Cartesian ??
444   [ False; False; True; False; False; True; False; True]
445   (mk_Sigma all_types (λaddr:all_types. [addr] → Instruction)
446     direct
447     (λa:subaddressing_mode ? [direct].
448       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
449             (mk_subaddressing_mode ? ?     a ?)))
450 ].
451nnormalize;
452 
453 ].
454*)
455
Note: See TracBrowser for help on using the repository browser.