source: Deliverables/D4.1/Matita/Assembly.ma @ 281

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

Resolved conflicts.

File size: 15.3 KB
Line 
1include "ASM.ma".
2
3ndefinition assembly1 ≝
4 λA.λi: preinstruction A.match i with
5  [ ACALL addr ⇒
6     match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
7      [ ADDR11 w ⇒ λ_.
8         let 〈v1,v2〉 ≝ split ? (S (S (S (S (S (S (S (S Z)))))))) (S (S (S Z))) w in
9          [ (v1 @@ [[true; false; false; false; true]]) ; v2 ]
10      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
11  | ADD addr1 addr2 ⇒
12     match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with
13      [ REGISTER r1 r2 r3 ⇒ λ_.[ ([[false;false;true;false;true;r1;r2;r2]]) ]
14      | DIRECT b1 ⇒ λ_.[ ([[false;false;true;false;false;true;false;true]]); b1 ]
15      | INDIRECT i1 ⇒ λ_. [ ([[false;false;true;false;false;true;true;i1]]) ]
16      | DATA b1 ⇒ λ_. [ ([[false;false;true;false;false;true;false;false]]) ; b1 ]
17      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
18  | _ ⇒ [ ([[false;false;false;false;false;false;false;false]]) ]].
19
20(*
21  | `ADDC (`A, `REG(r1,r2,r3)) ->
22     [mk_byte_from_bits ((false,false,true,true),(true,r1,r2,r3))]
23  | `ADDC (`A, `DIRECT b1) ->
24     [mk_byte_from_bits ((false,false,true,true),(false,true,false,true)); b1]
25  | `ADDC (`A,`INDIRECT i1) ->
26     [mk_byte_from_bits ((false,false,true,true),(false,true,true,i1))]
27  | `ADDC (`A,`DATA b1) ->
28     [mk_byte_from_bits ((false,false,true,true),(false,true,false,false)); b1]
29  | `AJMP (`ADDR11 w) ->
30     let (a10,a9,a8,b1) = from_word11 w in
31       [mk_byte_from_bits ((a10,a9,a8,false),(false,false,false,true))]
32  | `ANL (`U1 (`A, `REG (r1,r2,r3))) ->
33     [mk_byte_from_bits ((false,true,false,true),(true,r1,r2,r3))]
34  | `ANL (`U1 (`A, `DIRECT b1)) ->
35     [mk_byte_from_bits ((false,true,false,true),(false,true,false,true)); b1]
36  | `ANL (`U1 (`A, `INDIRECT i1)) ->
37     [mk_byte_from_bits ((false,true,false,true),(false,true,true,i1))]
38  | `ANL (`U1 (`A, `DATA b1)) ->
39     [mk_byte_from_bits ((false,true,false,true),(false,true,false,false)); b1]
40  | `ANL (`U2 (`DIRECT b1,`A)) ->
41     [mk_byte_from_bits ((false,true,false,true),(false,false,true,false)); b1]
42  | `ANL (`U2 (`DIRECT b1,`DATA b2)) ->
43     [mk_byte_from_bits ((false,true,false,true),(false,false,true,true)); b1; b2]
44  | `ANL (`U3 (`C,`BIT b1)) ->
45     [mk_byte_from_bits ((true,false,false,false),(false,false,true,false)); b1]
46  | `ANL (`U3 (`C,`NBIT b1)) ->
47    [mk_byte_from_bits ((true,false,true,true),(false,false,false,false)); b1]
48  | `CJNE (`U1 (`A, `DIRECT b1), `REL b2) ->
49    [mk_byte_from_bits ((true,false,true,true),(false,true,false,true)); b1; b2]
50  | `CJNE (`U1 (`A, `DATA b1), `REL b2) ->
51    [mk_byte_from_bits ((true,false,true,true),(false,true,false,false)); b1; b2]
52  | `CJNE (`U2 (`REG(r1,r2,r3), `DATA b1), `REL b2) ->
53    [mk_byte_from_bits ((true,false,true,true),(true,r1,r2,r3)); b1; b2]
54  | `CJNE (`U2 (`INDIRECT i1, `DATA b1), `REL b2) ->
55    [mk_byte_from_bits ((true,false,true,true),(false,true,true,i1)); b1; b2]
56  | `CLR `A ->
57    [mk_byte_from_bits ((true,true,true,false),(false,true,false,false))]
58  | `CLR `C ->
59    [mk_byte_from_bits ((true,true,false,false),(false,false,true,true))]
60  | `CLR (`BIT b1) ->
61    [mk_byte_from_bits ((true,true,false,false),(false,false,true,false)); b1]
62  | `CPL `A ->
63    [mk_byte_from_bits ((true,true,true,true),(false,true,false,false))]
64  | `CPL `C ->
65    [mk_byte_from_bits ((true,false,true,true),(false,false,true,true))]
66  | `CPL (`BIT b1) ->
67    [mk_byte_from_bits ((true,false,true,true),(false,false,true,false)); b1]
68  | `DA `A ->
69    [mk_byte_from_bits ((true,true,false,true),(false,true,false,false))]
70  | `DEC `A ->
71    [mk_byte_from_bits ((false,false,false,true),(false,true,false,false))]
72  | `DEC (`REG(r1,r2,r3)) ->
73    [mk_byte_from_bits ((false,false,false,true),(true,r1,r2,r3))]
74  | `DEC (`DIRECT b1) ->
75    [mk_byte_from_bits ((false,false,false,true),(false,true,false,true)); b1]
76  | `DEC (`INDIRECT i1) ->
77    [mk_byte_from_bits ((false,false,false,true),(false,true,true,i1))]
78  | `DIV (`A, `B) ->
79    [mk_byte_from_bits ((true,false,false,false),(false,true,false,false))]
80  | `DJNZ (`REG(r1,r2,r3), `REL b1) ->
81    [mk_byte_from_bits ((true,true,false,true),(true,r1,r2,r3)); b1]
82  | `DJNZ (`DIRECT b1, `REL b2) ->
83    [mk_byte_from_bits ((true,true,false,true),(false,true,false,true)); b1; b2]
84  | `INC `A ->
85    [mk_byte_from_bits ((false,false,false,false),(false,true,false,false))]
86  | `INC (`REG(r1,r2,r3)) ->
87    [mk_byte_from_bits ((false,false,false,false),(true,r1,r2,r3))]
88  | `INC (`DIRECT b1) ->
89    [mk_byte_from_bits ((false,false,false,false),(false,true,false,true)); b1]
90  | `INC (`INDIRECT i1) ->
91    [mk_byte_from_bits ((false,false,false,false),(false,true,true,i1))]
92  | `INC `DPTR ->
93    [mk_byte_from_bits ((true,false,true,false),(false,false,true,true))]
94  | `JB (`BIT b1, `REL b2) ->
95    [mk_byte_from_bits ((false,false,true,false),(false,false,false,false)); b1; b2]
96  | `JBC (`BIT b1, `REL b2) ->
97    [mk_byte_from_bits ((false,false,false,true),(false,false,false,false)); b1; b2]
98  | `JC (`REL b1) ->
99    [mk_byte_from_bits ((false,true,false,false),(false,false,false,false)); b1]
100  | `JMP `IND_DPTR ->
101    [mk_byte_from_bits ((false,true,true,true),(false,false,true,true))]
102  | `JNB (`BIT b1, `REL b2) ->
103    [mk_byte_from_bits ((false,false,true,true),(false,false,false,false)); b1; b2]
104  | `JNC (`REL b1) ->
105    [mk_byte_from_bits ((false,true,false,true),(false,false,false,false)); b1]
106  | `JNZ (`REL b1) ->
107    [mk_byte_from_bits ((false,true,true,true),(false,false,false,false)); b1]
108  | `JZ (`REL b1) ->
109    [mk_byte_from_bits ((false,true,true,false),(false,false,false,false)); b1]
110  | `LCALL (`ADDR16 w) ->
111      let (b1,b2) = from_word w in
112        [mk_byte_from_bits ((false,false,false,true),(false,false,true,false)); b1; b2]
113  | `LJMP (`ADDR16 w) ->
114      let (b1,b2) = from_word w in
115        [mk_byte_from_bits ((false,false,false,false),(false,false,true,false)); b1; b2]
116  | `MOV (`U1 (`A, `REG(r1,r2,r3))) ->
117    [mk_byte_from_bits ((true,true,true,false),(true,r1,r2,r3))]
118  | `MOV (`U1 (`A, `DIRECT b1)) ->
119    [mk_byte_from_bits ((true,true,true,false),(false,true,false,true)); b1]
120  | `MOV (`U1 (`A, `INDIRECT i1)) ->
121    [mk_byte_from_bits ((true,true,true,false),(false,true,true,i1))]
122  | `MOV (`U1 (`A, `DATA b1)) ->
123    [mk_byte_from_bits ((false,true,true,true),(false,true,false,false)); b1]
124  | `MOV (`U2 (`REG(r1,r2,r3), `A)) ->
125    [mk_byte_from_bits ((true,true,true,true),(true,r1,r2,r3))]
126  | `MOV (`U2 (`REG(r1,r2,r3), (`DIRECT b1))) ->
127    [mk_byte_from_bits ((true,false,true,false),(true,r1,r2,r3)); b1]
128  | `MOV (`U2 (`REG(r1,r2,r3), (`DATA b1))) ->
129    [mk_byte_from_bits ((false,true,true,true),(true,r1,r2,r3)); b1]
130  | `MOV (`U3 (`DIRECT b1, `A)) ->
131    [mk_byte_from_bits ((true,true,true,true),(false,true,false,true)); b1]
132  | `MOV (`U3 (`DIRECT b1, `REG(r1,r2,r3))) ->
133    [mk_byte_from_bits ((true,false,false,false),(true,r1,r2,r3)); b1]
134  | `MOV (`U3 (`DIRECT b1, `DIRECT b2)) ->
135    [mk_byte_from_bits ((true,false,false,false),(false,true,false,true)); b1; b2]
136  | `MOV (`U3 (`DIRECT b1, `INDIRECT i1)) ->
137    [mk_byte_from_bits ((true,false,false,false),(false,true,true,i1)); b1]
138  | `MOV (`U3 (`DIRECT b1, `DATA b2)) ->
139    [mk_byte_from_bits ((false,true,true,true),(false,true,false,true)); b1; b2]
140  | `MOV (`U2 (`INDIRECT i1, `A)) ->
141    [mk_byte_from_bits ((true,true,true,true),(false,true,true,i1))]
142  | `MOV (`U2 (`INDIRECT i1, `DIRECT b1)) ->
143    [mk_byte_from_bits ((true,false,true,false),(false,true,true,i1)); b1]
144  | `MOV (`U2 (`INDIRECT i1, `DATA b1)) ->
145    [mk_byte_from_bits ((false,true,true,true),(false,true,true,i1)); b1]
146  | `MOV (`U5 (`C, `BIT b1)) ->
147    [mk_byte_from_bits ((true,false,true,false),(false,false,true,false)); b1]
148  | `MOV (`U6 (`BIT b1, `C)) ->
149    [mk_byte_from_bits ((true,false,false,true),(false,false,true,false)); b1]
150  | `MOV (`U4 (`DPTR, `DATA16 w)) ->
151    let (b1,b2) = from_word w in
152      [mk_byte_from_bits ((true,false,false,true),(false,false,false,false)); b1; b2]
153  | `MOVC (`A, `A_DPTR) ->
154    [mk_byte_from_bits ((true,false,false,true),(false,false,true,true))]
155  | `MOVC (`A, `A_PC) ->
156    [mk_byte_from_bits ((true,false,false,false),(false,false,true,true))]
157  | `MOVX (`U1 (`A, `EXT_INDIRECT i1)) ->
158    [mk_byte_from_bits ((true,true,true,false),(false,false,true,i1))]
159  | `MOVX (`U1 (`A, `EXT_IND_DPTR)) ->
160    [mk_byte_from_bits ((true,true,true,false),(false,false,false,false))]
161  | `MOVX (`U2 (`EXT_INDIRECT i1, `A)) ->
162    [mk_byte_from_bits ((true,true,true,true),(false,false,true,i1))]
163  | `MOVX (`U2 (`EXT_IND_DPTR, `A)) ->
164    [mk_byte_from_bits ((true,true,true,true),(false,false,false,false))]
165  | `MUL(`A, `B) ->
166    [mk_byte_from_bits ((true,false,true,false),(false,true,false,false))]
167  | `NOP ->
168    [mk_byte_from_bits ((false,false,false,false),(false,false,false,false))]
169  | `ORL (`U1(`A, `REG(r1,r2,r3))) ->
170    [mk_byte_from_bits ((false,true,false,false),(true,r1,r2,r3))]
171  | `ORL (`U1(`A, `DIRECT b1)) ->
172    [mk_byte_from_bits ((false,true,false,false),(false,true,false,true)); b1]
173  | `ORL (`U1(`A, `INDIRECT i1)) ->
174    [mk_byte_from_bits ((false,true,false,false),(false,true,true,i1))]
175  | `ORL (`U1(`A, `DATA b1)) ->
176    [mk_byte_from_bits ((false,true,false,false),(false,true,false,false)); b1]
177  | `ORL (`U2(`DIRECT b1, `A)) ->
178    [mk_byte_from_bits ((false,true,false,false),(false,false,true,false)); b1]
179  | `ORL (`U2 (`DIRECT b1, `DATA b2)) ->
180    [mk_byte_from_bits ((false,true,false,false),(false,false,true,true)); b1; b2]
181  | `ORL (`U3 (`C, `BIT b1)) ->
182    [mk_byte_from_bits ((false,true,true,true),(false,false,true,false)); b1]
183  | `ORL (`U3 (`C, `NBIT b1)) ->
184    [mk_byte_from_bits ((true,false,true,false),(false,false,false,false)); b1]
185  | `POP (`DIRECT b1) ->
186    [mk_byte_from_bits ((true,true,false,true),(false,false,false,false)); b1]
187  | `PUSH (`DIRECT b1) ->
188    [mk_byte_from_bits ((true,true,false,false),(false,false,false,false)); b1]
189  | `RET ->
190    [mk_byte_from_bits ((false,false,true,false),(false,false,true,false))]
191  | `RETI ->
192    [mk_byte_from_bits ((false,false,true,true),(false,false,true,false))]
193  | `RL `A ->
194    [mk_byte_from_bits ((false,false,true,false),(false,false,true,true))]
195  | `RLC `A ->
196    [mk_byte_from_bits ((false,false,true,true),(false,false,true,true))]
197  | `RR `A ->
198    [mk_byte_from_bits ((false,false,false,false),(false,false,true,true))]
199  | `RRC `A ->
200    [mk_byte_from_bits ((false,false,false,true),(false,false,true,true))]
201  | `SETB `C ->
202    [mk_byte_from_bits ((true,true,false,true),(false,false,true,true))]
203  | `SETB (`BIT b1) ->
204    [mk_byte_from_bits ((true,true,false,true),(false,false,true,false)); b1]
205  | `SJMP (`REL b1) ->
206    [mk_byte_from_bits ((true,false,false,false),(false,false,false,false)); b1]
207  | `SUBB (`A, `REG(r1,r2,r3)) ->
208    [mk_byte_from_bits ((true,false,false,true),(true,r1,r2,r3))]
209  | `SUBB (`A, `DIRECT b1) ->
210    [mk_byte_from_bits ((true,false,false,true),(false,true,false,true)); b1]
211  | `SUBB (`A, `INDIRECT i1) ->
212    [mk_byte_from_bits ((true,false,false,true),(false,true,true,i1))]
213  | `SUBB (`A, `DATA b1) ->
214    [mk_byte_from_bits ((true,false,false,true),(false,true,false,false)); b1]
215  | `SWAP `A ->
216    [mk_byte_from_bits ((true,true,false,false),(false,true,false,false))]
217  | `XCH (`A, `REG(r1,r2,r3)) ->
218    [mk_byte_from_bits ((true,true,false,false),(true,r1,r2,r3))]
219  | `XCH (`A, `DIRECT b1) ->
220    [mk_byte_from_bits ((true,true,false,false),(false,true,false,true)); b1]
221  | `XCH (`A, `INDIRECT i1) ->
222    [mk_byte_from_bits ((true,true,false,false),(false,true,true,i1))]
223  | `XCHD(`A, `INDIRECT i1) ->
224    [mk_byte_from_bits ((true,true,false,true),(false,true,true,i1))]
225  | `XRL(`U1(`A, `REG(r1,r2,r3))) ->
226    [mk_byte_from_bits ((false,true,true,false),(true,r1,r2,r3))]
227  | `XRL(`U1(`A, `DIRECT b1)) ->
228    [mk_byte_from_bits ((false,true,true,false),(false,true,false,true)); b1]
229  | `XRL(`U1(`A, `INDIRECT i1)) ->
230    [mk_byte_from_bits ((false,true,true,false),(false,true,true,i1))]
231  | `XRL(`U1(`A, `DATA b1)) ->
232    [mk_byte_from_bits ((false,true,true,false),(false,true,false,false)); b1]
233  | `XRL(`U2(`DIRECT b1, `A)) ->
234    [mk_byte_from_bits ((false,true,true,false),(false,false,true,false)); b1]
235  | `XRL(`U2(`DIRECT b1, `DATA b2)) ->
236    [mk_byte_from_bits ((false,true,true,false),(false,false,true,true)); b1; b2]
237;;
238
239
240
241nrecord Sigma (A: Type[0]) (T: A → Type[0]) : Type[0] ≝ {
242   elem:> A;
243   witness: T elem
244}.
245
246interpretation "Sigma" 'sigma T = (Sigma ? T).
247
248naxiom daemon: False.
249
250naxiom decode_register: Vector Bool (S (S (S Z))) → [reg].
251naxiom decode_direct:   Vector Bool (S (S (S Z))) → [direct].
252
253ndefinition decode_tbl0: List ((Σn.Vector Bool n) × (Vector Bool (S (S (S Z))) → Instruction))
254 ≝
255 [mk_Cartesian ??
256   (mk_Sigma ? (λn.Vector Bool n) ? [ false; false; true; false; true])
257     (λl.
258       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
259             (mk_subaddressing_mode ? ?    (decode_register l) ?));
260  mk_Cartesian ??
261   (mk_Sigma ? (λn.Vector Bool n) ? [ false; false; true; false; true])
262     (λl.
263       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
264             (mk_subaddressing_mode ? ? (decode_direct l) ?)) ].
265ncases daemon.
266nqed.
267
268
269naxiom decode_register: List Bool → [reg].
270naxiom decode_direct: List Bool → [direct].
271
272ndefinition decode_tbl0: List (List Bool × (List Bool → Instruction))
273 ≝
274 [mk_Cartesian ??
275   [ false; false; true; false; true]
276     (λl.
277       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
278             (mk_subaddressing_mode ? ?    (decode_register l) ?));
279  mk_Cartesian ??
280   [ false; false; true; false; true]
281     (λl.
282       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
283             (mk_subaddressing_mode ? ? (decode_direct l) ?)) ].
284ncases daemon.
285nqed.
286
287
288ndefinition decode_tbl1:
289 List (List Bool × Σaddr:all_types. [addr] → Instruction)
290 ≝
291 [mk_Cartesian ??
292   [ false; false; true; false; true]
293   (mk_Sigma ? (λaddr:all_types. [addr] → Instruction)
294     reg
295     (λa.
296       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
297             (mk_subaddressing_mode ? ? a ?))) ].
298ncases daemon.
299nqed.
300             
301ndefinition decode_tbl2:
302 List (List Bool × Σaddr:all_types. [addr] → Instruction)
303 ≝
304 [mk_Cartesian ??
305   [ false; false; true; false; false; true; false; true]
306   (mk_Sigma ? (λaddr:all_types. [addr] → Instruction)
307     direct
308     (λa.
309       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
310             (mk_subaddressing_mode ? ?     a ?))) ].
311ncases daemon.
312nqed.
313
314ndefinition decode_tbl ≝ decode_tbl1 @ decode_tbl2.
315
316decode_addr_mode; ∀addr:all_types. List Bool → [addr].
317
318decode ≝
319 λl:List Bit.
320  List.iter
321   (fun l0 addr mk_f →
322     match split_prefix l l0 with
323      [ None ⇒ ...
324      | Some r ⇒ mk_f (decode_addr_mode r) ]
325     
326   ) decode_tbl
327
328encode ≝
329
330ndefinition decode_tbl:
331 List (List Bool × Σaddr:all_types. [addr] → Instruction)
332 ≝
333 [mk_Cartesian ??
334   [ False; False; True; False; True]
335   (mk_Sigma all_types (λaddr:all_types. [addr] → Instruction)
336     reg
337     (λa:subaddressing_mode ? [reg].
338       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
339             (mk_subaddressing_mode ? ?     a ?)));
340  mk_Cartesian ??
341   [ False; False; True; False; False; True; False; True]
342   (mk_Sigma all_types (λaddr:all_types. [addr] → Instruction)
343     direct
344     (λa:subaddressing_mode ? [direct].
345       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
346             (mk_subaddressing_mode ? ?     a ?)))
347 ].
348nnormalize;
349 
350 ].
351*)
Note: See TracBrowser for help on using the repository browser.