source: src/ASM/Fetch.ma @ 827

Last change on this file since 827 was 820, checked in by mulligan, 9 years ago

changes to get the semantics of pseudoassembly working

File size: 21.9 KB
RevLine 
[698]1include "ASM/BitVectorTrie.ma".
2include "ASM/Arithmetic.ma".
3include "ASM/ASM.ma".
[475]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
[820]22        〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,ACC_A〉)))))), pc〉, 1〉
[475]23       else
24        let 〈b,v〉≝  head … v in if b then
25         let 〈b,v〉≝  head … v in if b then
[820]26          〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),ACC_A〉)))))), pc〉, 1〉
[475]27         else
28          let 〈b,v〉≝  head … v in if b then
[820]29           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,ACC_A〉))))), pc〉, 1〉
[475]30          else
31           〈〈CPL … ACC_A, pc〉, 1〉
32        else
33         let 〈b,v〉≝  head … v in if b then
[820]34          〈〈RealInstruction (MOVX … (inr … 〈EXT_INDIRECT (from_singl … v),ACC_A〉)), pc〉, 2〉
[475]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
[820]39           〈〈RealInstruction (MOVX … (inr … 〈EXT_INDIRECT_DPTR,ACC_A〉)), pc〉, 2〉
[475]40      else
41       let 〈b,v〉≝  head … v in if b then
[820]42        〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,REGISTER v〉)))))), pc〉, 1〉
[475]43       else
44        let 〈b,v〉≝  head … v in if b then
45         let 〈b,v〉≝  head … v in if b then
[820]46          〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉)))))), pc〉, 1〉
[475]47         else
48          let 〈b,v〉≝  head … v in if b then
[820]49           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DIRECT b1〉)))))), pc〉, 1〉
[475]50          else
[820]51           〈〈RealInstruction (CLR … ACC_A), pc〉, 1〉
[475]52        else
53         let 〈b,v〉≝  head … v in if b then
[820]54          〈〈RealInstruction (MOVX … (inl … 〈ACC_A,EXT_INDIRECT (from_singl … v)〉)), pc〉, 2〉
[475]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
[820]59           〈〈RealInstruction (MOVX … (inl … 〈ACC_A,EXT_INDIRECT_DPTR〉)), pc〉, 2〉
[475]60     else
61      let 〈b,v〉≝  head … v in if b then
62       let 〈b,v〉≝  head … v in if b then
[820]63        let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (DJNZ … (REGISTER v) (RELATIVE b1)), pc〉, 2〉
[475]64       else
65        let 〈b,v〉≝  head … v in if b then
66         let 〈b,v〉≝  head … v in if b then
[820]67          〈〈RealInstruction (XCHD … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉
[475]68         else
69          let 〈b,v〉≝  head … v in if b then
[820]70           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (DJNZ … (DIRECT b1) (RELATIVE b2)), pc〉, 2〉
[475]71          else
[820]72           〈〈RealInstruction (DA … ACC_A), pc〉, 1〉
[475]73        else
74         let 〈b,v〉≝  head … v in if b then
75          let 〈b,v〉≝  head … v in if b then
[820]76           〈〈RealInstruction (SETB … CARRY), pc〉, 1〉
[475]77          else
[820]78           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (SETB … (BIT_ADDR b1)), pc〉, 1〉
[475]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
[820]83           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (POP … (DIRECT b1)), pc〉, 2〉
[475]84      else
85       let 〈b,v〉≝  head … v in if b then
[820]86        〈〈RealInstruction (XCH … ACC_A (REGISTER v)), pc〉, 1〉
[475]87       else
88        let 〈b,v〉≝  head … v in if b then
89         let 〈b,v〉≝  head … v in if b then
[820]90          〈〈RealInstruction (XCH … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉
[475]91         else
92          let 〈b,v〉≝  head … v in if b then
[820]93           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (XCH … ACC_A (DIRECT b1)), pc〉, 1〉
[475]94          else
[820]95           〈〈RealInstruction (SWAP … ACC_A), pc〉, 1〉
[475]96        else
97         let 〈b,v〉≝  head … v in if b then
98          let 〈b,v〉≝  head … v in if b then
[820]99           〈〈RealInstruction (CLR … CARRY), pc〉, 1〉
[475]100          else
[820]101           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (CLR … (BIT_ADDR b1)), pc〉, 1〉
[475]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
[820]106           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (PUSH … (DIRECT b1)), pc〉, 2〉
[475]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
[820]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〉
[475]112       else
113        let 〈b,v〉≝  head … v in if b then
114         let 〈b,v〉≝  head … v in if b then
[820]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〉
[475]116         else
117          let 〈b,v〉≝  head … v in if b then
[820]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〉
[475]119          else
[820]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〉
[475]121        else
122         let 〈b,v〉≝  head … v in if b then
123          let 〈b,v〉≝  head … v in if b then
[820]124           〈〈RealInstruction (CPL … CARRY), pc〉, 1〉
[475]125          else
[820]126           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (CPL … (BIT_ADDR b1)), pc〉, 1〉
[475]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
[820]131           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ANL … (inr … 〈CARRY,N_BIT_ADDR b1〉)), pc〉, 2〉
[475]132      else
133       let 〈b,v〉≝  head … v in if b then
[820]134        let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DIRECT b1〉)))))), pc〉, 2〉
[475]135       else
136        let 〈b,v〉≝  head … v in if b then
137         let 〈b,v〉≝  head … v in if b then
[820]138          let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DIRECT b1〉)))))), pc〉, 2〉
[475]139         else
[820]140          〈〈RealInstruction (MUL … ACC_A ACC_B), pc〉, 4〉
[475]141        else
142         let 〈b,v〉≝  head … v in if b then
143          let 〈b,v〉≝  head … v in if b then
[820]144           〈〈RealInstruction (INC … DPTR), pc〉, 2〉
[475]145          else
[820]146           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inr … 〈CARRY,BIT_ADDR b1〉))), pc〉, 1〉
[475]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
[820]151           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ORL … (inr … 〈CARRY,N_BIT_ADDR b1〉)), pc〉, 2〉
[475]152     else
153      let 〈b,v〉≝  head … v in if b then
154       let 〈b,v〉≝  head … v in if b then
[820]155        〈〈RealInstruction (SUBB … ACC_A (REGISTER v)), pc〉, 1〉
[475]156       else
157        let 〈b,v〉≝  head … v in if b then
158         let 〈b,v〉≝  head … v in if b then
[820]159          〈〈RealInstruction (SUBB … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉
[475]160         else
161          let 〈b,v〉≝  head … v in if b then
[820]162           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (SUBB … ACC_A (DIRECT b1)), pc〉, 1〉
[475]163          else
[820]164           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (SUBB … ACC_A (DATA b1)), pc〉, 1〉
[475]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
[820]170           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inr … 〈BIT_ADDR b1,CARRY〉)), pc〉, 2〉
[475]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
[820]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〉
[475]176      else
177       let 〈b,v〉≝  head … v in if b then
[820]178        let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,REGISTER v〉))))), pc〉, 2〉
[475]179       else
180        let 〈b,v〉≝  head … v in if b then
181         let 〈b,v〉≝  head … v in if b then
[820]182          let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,INDIRECT (from_singl … v)〉))))), pc〉, 2〉
[475]183         else
184          let 〈b,v〉≝  head … v in if b then
[820]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〉
[475]186          else
[820]187           〈〈RealInstruction (DIV … ACC_A ACC_B), pc〉, 4〉
[475]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
[820]193           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ANL … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 2〉
[475]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
[820]204        let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DATA b1〉)))))), pc〉, 1〉
[475]205       else
206        let 〈b,v〉≝  head … v in if b then
207         let 〈b,v〉≝  head … v in if b then
[820]208          let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DATA b1〉)))))), pc〉, 1〉
[475]209         else
210          let 〈b,v〉≝  head … v in if b then
[820]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〉
[475]212          else
[820]213           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DATA b1〉)))))), pc〉, 1〉
[475]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
[820]219           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ORL … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 2〉
[475]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
[820]224           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (JNZ … (RELATIVE b1)), pc〉, 2〉
[475]225      else
226       let 〈b,v〉≝  head … v in if b then
[820]227        〈〈RealInstruction (XRL … (inl … 〈ACC_A,REGISTER v〉)), pc〉, 1〉
[475]228       else
229        let 〈b,v〉≝  head … v in if b then
230         let 〈b,v〉≝  head … v in if b then
[820]231          〈〈RealInstruction (XRL … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉)), pc〉, 1〉
[475]232         else
233          let 〈b,v〉≝  head … v in if b then
[820]234           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (XRL … (inl … 〈ACC_A,DIRECT b1〉)), pc〉, 1〉
[475]235          else
[820]236           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (XRL … (inl … 〈ACC_A,DATA b1〉)), pc〉, 1〉
[475]237        else
238         let 〈b,v〉≝  head … v in if b then
239          let 〈b,v〉≝  head … v in if b then
[820]240           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,DATA b2〉)), pc〉, 2〉
[475]241          else
[820]242           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,ACC_A〉)), pc〉, 1〉
[475]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
[820]247           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (JZ … (RELATIVE b1)), pc〉, 2〉
[475]248     else
249      let 〈b,v〉≝  head … v in if b then
250       let 〈b,v〉≝  head … v in if b then
[820]251        〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,REGISTER v〉))), pc〉, 1〉
[475]252       else
253        let 〈b,v〉≝  head … v in if b then
254         let 〈b,v〉≝  head … v in if b then
[820]255          〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉))), pc〉, 1〉
[475]256         else
257          let 〈b,v〉≝  head … v in if b then
[820]258           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,DIRECT b1〉))), pc〉, 1〉
[475]259          else
[820]260           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,DATA b1〉))), pc〉, 1〉
[475]261        else
262         let 〈b,v〉≝  head … v in if b then
263          let 〈b,v〉≝  head … v in if b then
[820]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〉
[475]265          else
[820]266           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉
[475]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
[820]271           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (JNC … (RELATIVE b1)), pc〉, 2〉
[475]272      else
273       let 〈b,v〉≝  head … v in if b then
[820]274        〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,REGISTER v〉))), pc〉, 1〉
[475]275       else
276        let 〈b,v〉≝  head … v in if b then
277         let 〈b,v〉≝  head … v in if b then
[820]278          〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉))), pc〉, 1〉
[475]279         else
280          let 〈b,v〉≝  head … v in if b then
[820]281           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,DIRECT b1〉))), pc〉, 1〉
[475]282          else
[820]283           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,DATA b1〉))), pc〉, 1〉
[475]284        else
285         let 〈b,v〉≝  head … v in if b then
286          let 〈b,v〉≝  head … v in if b then
[820]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〉
[475]288          else
[820]289           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉
[475]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
[820]294           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (JC … (RELATIVE b1)), pc〉, 2〉
[475]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
[820]299        〈〈RealInstruction (ADDC … ACC_A (REGISTER v)), pc〉, 1〉
[475]300       else
301        let 〈b,v〉≝  head … v in if b then
302         let 〈b,v〉≝  head … v in if b then
[820]303          〈〈RealInstruction (ADDC … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉
[475]304         else
305          let 〈b,v〉≝  head … v in if b then
[820]306           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ADDC … ACC_A (DIRECT b1)), pc〉, 1〉
[475]307          else
[820]308           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ADDC … ACC_A (DATA b1)), pc〉, 1〉
[475]309        else
310         let 〈b,v〉≝  head … v in if b then
311          let 〈b,v〉≝  head … v in if b then
[820]312           〈〈RealInstruction (RLC … ACC_A), pc〉, 1〉
[475]313          else
[820]314           〈〈RealInstruction (RETI …), pc〉, 2〉
[475]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
[820]319           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (JNB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
[475]320      else
321       let 〈b,v〉≝  head … v in if b then
[820]322        〈〈RealInstruction (ADD … ACC_A (REGISTER v)), pc〉, 1〉
[475]323       else
324        let 〈b,v〉≝  head … v in if b then
325         let 〈b,v〉≝  head … v in if b then
[820]326          〈〈RealInstruction (ADD … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉
[475]327         else
328          let 〈b,v〉≝  head … v in if b then
[820]329           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ADD … ACC_A (DIRECT b1)), pc〉, 1〉
[475]330          else
[820]331           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ADD … ACC_A (DATA b1)), pc〉, 1〉
[475]332        else
333         let 〈b,v〉≝  head … v in if b then
334          let 〈b,v〉≝  head … v in if b then
[820]335           〈〈RealInstruction (RL … ACC_A), pc〉, 1〉
[475]336          else
[820]337           〈〈RealInstruction (RET …), pc〉, 2〉
[475]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
[820]342           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (JB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
[475]343     else
344      let 〈b,v〉≝  head … v in if b then
345       let 〈b,v〉≝  head … v in if b then
[820]346        〈〈RealInstruction (DEC … (REGISTER v)), pc〉, 1〉
[475]347       else
348        let 〈b,v〉≝  head … v in if b then
349         let 〈b,v〉≝  head … v in if b then
[820]350          〈〈RealInstruction (DEC … (INDIRECT (from_singl … v))), pc〉, 1〉
[475]351         else
352          let 〈b,v〉≝  head … v in if b then
[820]353           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (DEC … (DIRECT b1)), pc〉, 1〉
[475]354          else
[820]355           〈〈RealInstruction (DEC … ACC_A), pc〉, 1〉
[475]356        else
357         let 〈b,v〉≝  head … v in if b then
358          let 〈b,v〉≝  head … v in if b then
[820]359           〈〈RealInstruction (RRC … ACC_A), pc〉, 1〉
[475]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
[820]366           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (JBC … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
[475]367      else
368       let 〈b,v〉≝  head … v in if b then
[820]369        〈〈RealInstruction (INC … (REGISTER v)), pc〉, 1〉
[475]370       else
371        let 〈b,v〉≝  head … v in if b then
372         let 〈b,v〉≝  head … v in if b then
[820]373          〈〈RealInstruction (INC … (INDIRECT (from_singl … v))), pc〉, 1〉
[475]374         else
375          let 〈b,v〉≝  head … v in if b then
[820]376           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (INC … (DIRECT b1)), pc〉, 1〉
[475]377          else
[820]378           〈〈RealInstruction (INC … ACC_A), pc〉, 1〉
[475]379        else
380         let 〈b,v〉≝  head … v in if b then
381          let 〈b,v〉≝  head … v in if b then
[820]382           〈〈RealInstruction (RR … ACC_A), pc〉, 1〉
[475]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
[820]389           〈〈RealInstruction (NOP …), pc〉, 1〉.
[475]390  %.
391qed.
Note: See TracBrowser for help on using the repository browser.