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

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

Undefined value singled out: what to do with it?

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