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

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

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