source: src/ASM/Fetch.ma @ 828

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

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