[698] | 1 | include "ASM/BitVectorTrie.ma". |
---|
| 2 | include "ASM/Arithmetic.ma". |
---|
| 3 | include "ASM/ASM.ma". |
---|
[475] | 4 | |
---|
| 5 | definition 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 | |
---|
| 13 | definition 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 | %. |
---|
| 391 | qed. |
---|