source: src/ASM/Fetch.ma @ 1109

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

Fetch function fixed: alla AJMPS were ACALL (and the other way around) and
all the bits of every ADDR11 address were flipped :-)

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