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

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

Completed!

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