Changeset 318 for Deliverables/D4.1/Matita
 Timestamp:
 Nov 26, 2010, 5:54:01 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Fetch.ma
r316 r318 8 8 〈res, lookup … pc pmem (zero eight)〉. 9 9 10 (* timings taken from SIEMENS *) 11 10 12 ndefinition fetch: BitVectorTrie Byte sixteen → Word → instruction × Word × Nat ≝ 11 13 λpmem,pc. 12 let 〈pc, instr〉 ≝ next pmem pc in13 let 〈 instr1,instr2〉 ≝ split … three five instrin14 if eqv … instr2 [[true;false;false;false;true]] then14 let 〈pc,v〉 ≝ next pmem pc in 15 let 〈v1,v2〉 ≝ split … three five v in 16 if eqv … v2 [[true;false;false;false;true]] then 15 17 let 〈pc,b1〉 ≝ next pmem pc in 16 〈〈ACALL … (ADDR11 (instr1 @@ b1)), pc〉, two〉 18 〈〈ACALL … (ADDR11 (v1 @@ b1)), pc〉, two〉 19 else if eqv … v2 [[false;false;false;false;true]] then 20 let 〈pc,b1〉 ≝ next pmem pc in 21 〈〈AJMP … (ADDR11 (v1 @@ b1)), pc〉, two〉 17 22 else 18 〈〈NOP …, pc〉, two〉. 23 let 〈b,v〉≝ head8 v in if b then 24 let 〈b,v〉≝ head8 v in if b then 25 let 〈b,v〉≝ head8 v in if b then 26 let 〈b,v〉≝ head8 v in if b then 27 let 〈b,v〉≝ head8 v in if b then 28 〈〈MOV (U2 (REGISTER v, ACC_A)), pc〉, one〉 29 else 30 let 〈b,v〉≝ head8 v in if b then 31 let 〈b,v〉≝ head8 v in if b then 32 〈〈MOV (U2 (INDIRECT v, ACC_A)), pc〉, one〉 33 else 34 let 〈b,v〉≝ head8 v in if b then 35 let pc,b1 = next pc in 〈〈MOV (U3 (DIRECT b1, ACC_A)), pc〉, one〉 36 else 37 〈〈CPL ACC_A, pc〉, one〉 38 else 39 let 〈b,v〉≝ head8 v in if b then 40 〈〈MOVX (U2 (EXT_INDIRECT v, ACC_A)), pc〉, two〉 41 else 42 let 〈b,v〉≝ head8 v in if b then 43 assert false 44 else 45 〈〈MOVX (U2 (EXT_IND_DPTR, ACC_A)), pc〉, two〉 46 else 47 let 〈b,v〉≝ head8 v in if b then 48 〈〈MOV (U1 (A, REGISTER v)), pc〉, one〉 49 else 50 let 〈b,v〉≝ head8 v in if b then 51 let 〈b,v〉≝ head8 v in if b then 52 〈〈MOV (U1 (A, INDIRECT v)), pc〉, one〉 53 else 54 let 〈b,v〉≝ head8 v in if b then 55 let pc,b1 = next pc in 〈〈MOV (U1 (A, DIRECT b1)), pc〉, one〉 56 else 57 〈〈CLR ACC_A, pc〉, one〉 58 else 59 let 〈b,v〉≝ head8 v in if b then 60 〈〈MOVX (U1 (A, EXT_INDIRECT v)), pc〉, two〉 61 else 62 let 〈b,v〉≝ head8 v in if b then 63 assert false 64 else 65 〈〈MOVX (U1 (A, EXT_IND_DPTR)), pc〉, two〉 66 else 67 let 〈b,v〉≝ head8 v in if b then 68 let 〈b,v〉≝ head8 v in if b then 69 let pc,b1 = next pc in 〈〈DJNZ (REGISTER v, REL b1), pc〉, two〉 70 else 71 let 〈b,v〉≝ head8 v in if b then 72 let 〈b,v〉≝ head8 v in if b then 73 〈〈XCHD(A, INDIRECT v), pc〉, one〉 74 else 75 let 〈b,v〉≝ head8 v in if b then 76 let pc,b1 = next pc in let pc,b2 = next pc in 〈〈DJNZ (DIRECT b1, REL b2), pc〉, two〉 77 else 78 〈〈DA ACC_A, pc〉, one〉 79 else 80 let 〈b,v〉≝ head8 v in if b then 81 let 〈b,v〉≝ head8 v in if b then 82 〈〈SETB C, pc〉, one〉 83 else 84 let pc,b1 = next pc in 〈〈SETB (BIT b1), pc〉, one〉 85 else 86 let 〈b,v〉≝ head8 v in if b then 87 assert false 88 else 89 let pc,b1 = next pc in 〈〈POP (DIRECT b1), pc〉, two〉 90 else 91 let 〈b,v〉≝ head8 v in if b then 92 〈〈XCH (A, REGISTER v), pc〉, one〉 93 else 94 let 〈b,v〉≝ head8 v in if b then 95 let 〈b,v〉≝ head8 v in if b then 96 〈〈XCH (A, INDIRECT v), pc〉, one〉 97 else 98 let 〈b,v〉≝ head8 v in if b then 99 let pc,b1 = next pc in 〈〈XCH (A, DIRECT b1), pc〉, one〉 100 else 101 〈〈SWAP ACC_A, pc〉, one〉 102 else 103 let 〈b,v〉≝ head8 v in if b then 104 let 〈b,v〉≝ head8 v in if b then 105 〈〈CLR C, pc〉, one〉 106 else 107 let pc,b1 = next pc in 〈〈CLR (BIT b1), pc〉, one〉 108 else 109 let 〈b,v〉≝ head8 v in if b then 110 assert false 111 else 112 let pc,b1 = next pc in 〈〈PUSH (DIRECT b1), pc〉, two〉 113 else 114 let 〈b,v〉≝ head8 v in if b then 115 let 〈b,v〉≝ head8 v in if b then 116 let 〈b,v〉≝ head8 v in if b then 117 let pc,b1 = next pc in let pc,b2 = next pc in 〈〈CJNE (U2 (REGISTER v, DATA b1), REL b2), pc〉, two〉 118 else 119 let 〈b,v〉≝ head8 v in if b then 120 let 〈b,v〉≝ head8 v in if b then 121 let pc,b1 = next pc in let pc,b2 = next pc in 〈〈CJNE (U2 (INDIRECT v, DATA b1), REL b2), pc〉, two〉 122 else 123 let 〈b,v〉≝ head8 v in if b then 124 let pc,b1 = next pc in let pc,b2 = next pc in 〈〈CJNE (U1 (A, DIRECT b1), REL b2), pc〉, two〉 125 else 126 let pc,b1 = next pc in let pc,b2 = next pc in 〈〈CJNE (U1 (A, DATA b1), REL b2), pc〉, two〉 127 else 128 let 〈b,v〉≝ head8 v in if b then 129 let 〈b,v〉≝ head8 v in if b then 130 〈〈CPL C, pc〉, one〉 131 else 132 let pc,b1 = next pc in 〈〈CPL (BIT b1), pc〉, one〉 133 else 134 let 〈b,v〉≝ head8 v in if b then 135 assert false 136 else 137 let pc,b1 = next pc in 〈〈ANL (U3 (C,NBIT b1)), pc〉, two〉 138 else 139 let 〈b,v〉≝ head8 v in if b then 140 let pc,b1 = next pc in 〈〈MOV (U2 (REGISTER v, (DIRECT b1))), pc〉, two〉 141 else 142 let 〈b,v〉≝ head8 v in if b then 143 let 〈b,v〉≝ head8 v in if b then 144 let pc,b1 = next pc in 〈〈MOV (U2 (INDIRECT v, DIRECT b1)), pc〉, two〉 145 else 146 〈〈MUL(A, B), pc〉, four〉 147 else 148 let 〈b,v〉≝ head8 v in if b then 149 let 〈b,v〉≝ head8 v in if b then 150 〈〈INC DPTR, pc〉, two〉 151 else 152 let pc,b1 = next pc in 〈〈MOV (U5 (C, BIT b1)), pc〉, one〉 153 else 154 let 〈b,v〉≝ head8 v in if b then 155 assert false 156 else 157 let pc,b1 = next pc in 〈〈ORL (U3 (C, NBIT b1)), pc〉, two〉 158 else 159 let 〈b,v〉≝ head8 v in if b then 160 let 〈b,v〉≝ head8 v in if b then 161 〈〈SUBB (A, REGISTER v), pc〉, one〉 162 else 163 let 〈b,v〉≝ head8 v in if b then 164 let 〈b,v〉≝ head8 v in if b then 165 〈〈SUBB (A, INDIRECT v), pc〉, one〉 166 else 167 let 〈b,v〉≝ head8 v in if b then 168 let pc,b1 = next pc in 〈〈SUBB (A, DIRECT b1), pc〉, one〉 169 else 170 let pc,b1 = next pc in 〈〈SUBB (A, DATA b1), pc〉, one〉 171 else 172 let 〈b,v〉≝ head8 v in if b then 173 let 〈b,v〉≝ head8 v in if b then 174 〈〈MOVC (A, ACC_A_DPTR), pc〉, two〉 175 else 176 let pc,b1 = next pc in 〈〈MOV (U6 (BIT b1, C)), pc〉, two〉 177 else 178 let 〈b,v〉≝ head8 v in if b then 179 assert false 180 else 181 let pc,b1 = next pc in let pc,b2 = next pc in 〈〈MOV (U4 (DPTR, DATA16(mk_word b1 b2))), pc〉, two〉 182 else 183 let 〈b,v〉≝ head8 v in if b then 184 let pc,b1 = next pc in 〈〈MOV (U3 (DIRECT b1, REGISTER v)), pc〉, two〉 185 else 186 let 〈b,v〉≝ head8 v in if b then 187 let 〈b,v〉≝ head8 v in if b then 188 let pc,b1 = next pc in 〈〈MOV (U3 (DIRECT b1, INDIRECT v)), pc〉, two〉 189 else 190 let 〈b,v〉≝ head8 v in if b then 191 let pc,b1 = next pc in let pc,b2 = next pc in 〈〈MOV (U3 (DIRECT b1, DIRECT b2)), pc〉, two〉 192 else 193 〈〈DIV (A, B), pc〉, four〉 194 else 195 let 〈b,v〉≝ head8 v in if b then 196 let 〈b,v〉≝ head8 v in if b then 197 〈〈MOVC (A, ACC_A_PC), pc〉, two〉 198 else 199 let pc,b1 = next pc in 〈〈ANL (U3 (C,BIT b1)), pc〉, two〉 200 else 201 let 〈b,v〉≝ head8 v in if b then 202 assert false 203 else 204 let pc,b1 = next pc in 〈〈SJMP (REL b1), pc〉, two〉 205 else 206 let 〈b,v〉≝ head8 v in if b then 207 let 〈b,v〉≝ head8 v in if b then 208 let 〈b,v〉≝ head8 v in if b then 209 let 〈b,v〉≝ head8 v in if b then 210 let pc,b1 = next pc in 〈〈MOV (U2 (REGISTER v, (DATA b1))), pc〉, one〉 211 else 212 let 〈b,v〉≝ head8 v in if b then 213 let 〈b,v〉≝ head8 v in if b then 214 let pc,b1 = next pc in 〈〈MOV (U2 (INDIRECT v, DATA b1)), pc〉, one〉 215 else 216 let 〈b,v〉≝ head8 v in if b then 217 let pc,b1 = next pc in let pc,b2 = next pc in 〈〈MOV (U3 (DIRECT b1, DATA b2)), pc〉, three〉 218 else 219 let pc,b1 = next pc in 〈〈MOV (U1 (A, DATA b1)), pc〉, one〉 220 else 221 let 〈b,v〉≝ head8 v in if b then 222 let 〈b,v〉≝ head8 v in if b then 223 〈〈JMP IND_DPTR, pc〉, two〉 224 else 225 let pc,b1 = next pc in 〈〈ORL (U3 (C, BIT b1)), pc〉, two〉 226 else 227 let 〈b,v〉≝ head8 v in if b then 228 assert false 229 else 230 let pc,b1 = next pc in 〈〈JNZ (REL b1), pc〉, two〉 231 else 232 let 〈b,v〉≝ head8 v in if b then 233 〈〈XRL(U1(A, REGISTER v)), pc〉, one〉 234 else 235 let 〈b,v〉≝ head8 v in if b then 236 let 〈b,v〉≝ head8 v in if b then 237 〈〈XRL(U1(A, INDIRECT v)), pc〉, one〉 238 else 239 let 〈b,v〉≝ head8 v in if b then 240 let pc,b1 = next pc in 〈〈XRL(U1(A, DIRECT b1)), pc〉, one〉 241 else 242 let pc,b1 = next pc in 〈〈XRL(U1(A, DATA b1)), pc〉, one〉 243 else 244 let 〈b,v〉≝ head8 v in if b then 245 let 〈b,v〉≝ head8 v in if b then 246 let pc,b1 = next pc in let pc,b2 = next pc in 〈〈XRL(U2(DIRECT b1, DATA b2)), pc〉, two〉 247 else 248 let pc,b1 = next pc in 〈〈XRL(U2(DIRECT b1, ACC_A)), pc〉, one〉 249 else 250 let 〈b,v〉≝ head8 v in if b then 251 assert false 252 else 253 let pc,b1 = next pc in 〈〈JZ (REL b1), pc〉, two〉 254 else 255 let 〈b,v〉≝ head8 v in if b then 256 let 〈b,v〉≝ head8 v in if b then 257 〈〈ANL (U1 (A, REGISTER v)), pc〉, one〉 258 else 259 let 〈b,v〉≝ head8 v in if b then 260 let 〈b,v〉≝ head8 v in if b then 261 〈〈ANL (U1 (A, INDIRECT v)), pc〉, one〉 262 else 263 let 〈b,v〉≝ head8 v in if b then 264 let pc,b1 = next pc in 〈〈ANL (U1 (A, DIRECT b1)), pc〉, one〉 265 else 266 let pc,b1 = next pc in 〈〈ANL (U1 (A, DATA b1)), pc〉, one〉 267 else 268 let 〈b,v〉≝ head8 v in if b then 269 let 〈b,v〉≝ head8 v in if b then 270 let pc,b1 = next pc in let pc,b2 = next pc in 〈〈ANL (U2 (DIRECT b1,DATA b2)), pc〉, two〉 271 else 272 let pc,b1 = next pc in 〈〈ANL (U2 (DIRECT b1,A)), pc〉, one〉 273 else 274 let 〈b,v〉≝ head8 v in if b then 275 assert false 276 else 277 let pc,b1 = next pc in 〈〈JNC (REL b1), pc〉, two〉 278 else 279 let 〈b,v〉≝ head8 v in if b then 280 〈〈ORL (U1(A, REGISTER v)), pc〉, one〉 281 else 282 let 〈b,v〉≝ head8 v in if b then 283 let 〈b,v〉≝ head8 v in if b then 284 〈〈ORL (U1(A, INDIRECT v)), pc〉, one〉 285 else 286 let 〈b,v〉≝ head8 v in if b then 287 let pc,b1 = next pc in 〈〈ORL (U1(A, DIRECT b1)), pc〉, one〉 288 else 289 let pc,b1 = next pc in 〈〈ORL (U1(A, DATA b1)), pc〉, one〉 290 else 291 let 〈b,v〉≝ head8 v in if b then 292 let 〈b,v〉≝ head8 v in if b then 293 let pc,b1 = next pc in let pc,b2 = next pc in 〈〈ORL (U2 (DIRECT b1, DATA b2)), pc〉, two〉 294 else 295 let pc,b1 = next pc in 〈〈ORL (U2(DIRECT b1, ACC_A)), pc〉, one〉 296 else 297 let 〈b,v〉≝ head8 v in if b then 298 assert false 299 else 300 let pc,b1 = next pc in 〈〈JC (REL b1), pc〉, two〉 301 else 302 let 〈b,v〉≝ head8 v in if b then 303 let 〈b,v〉≝ head8 v in if b then 304 let 〈b,v〉≝ head8 v in if b then 305 〈〈ADDC (A,REGISTER v), pc〉, one〉 306 else 307 let 〈b,v〉≝ head8 v in if b then 308 let 〈b,v〉≝ head8 v in if b then 309 〈〈ADDC (A,INDIRECT v), pc〉, one〉 310 else 311 let 〈b,v〉≝ head8 v in if b then 312 let pc,b1 = next pc in 〈〈ADDC (A,DIRECT b1), pc〉, one〉 313 else 314 let pc,b1 = next pc in 〈〈ADDC (A,DATA b1), pc〉, one〉 315 else 316 let 〈b,v〉≝ head8 v in if b then 317 let 〈b,v〉≝ head8 v in if b then 318 〈〈RLC ACC_A, pc〉, one〉 319 else 320 〈〈RETI, pc〉, two〉 321 else 322 let 〈b,v〉≝ head8 v in if b then 323 assert false 324 else 325 let pc,b1 = next pc in let pc,b2 = next pc in 〈〈JNB (BIT b1, REL b2), pc〉, two〉 326 else 327 let 〈b,v〉≝ head8 v in if b then 328 〈〈ADD (A,REGISTER v), pc〉, one〉 329 else 330 let 〈b,v〉≝ head8 v in if b then 331 let 〈b,v〉≝ head8 v in if b then 332 〈〈ADD (A,INDIRECT v), pc〉, one〉 333 else 334 let 〈b,v〉≝ head8 v in if b then 335 let pc,b1 = next pc in 〈〈ADD (A,DIRECT b1), pc〉, one〉 336 else 337 let pc,b1 = next pc in 〈〈ADD (A,DATA b1), pc〉, one〉 338 else 339 let 〈b,v〉≝ head8 v in if b then 340 let 〈b,v〉≝ head8 v in if b then 341 〈〈RL ACC_A, pc〉, one〉 342 let 〈b,v〉≝ head8 v in if b then 343 else 344 〈〈RET, pc〉, two〉 345 else 346 let 〈b,v〉≝ head8 v in if b then 347 assert false 348 else 349 let pc,b1 = next pc in let pc,b2 = next pc in 〈〈JB (BIT b1, REL b2), pc〉, two〉 350 else 351 let 〈b,v〉≝ head8 v in if b then 352 let 〈b,v〉≝ head8 v in if b then 353 〈〈DEC (REGISTER v), pc〉, one〉 354 else 355 let 〈b,v〉≝ head8 v in if b then 356 let 〈b,v〉≝ head8 v in if b then 357 〈〈DEC (INDIRECT v), pc〉, one〉 358 else 359 let 〈b,v〉≝ head8 v in if b then 360 let pc,b1 = next pc in 〈〈DEC (DIRECT b1), pc〉, one〉 361 else 362 〈〈DEC ACC_A, pc〉, one〉 363 else 364 let 〈b,v〉≝ head8 v in if b then 365 let 〈b,v〉≝ head8 v in if b then 366 〈〈RRC ACC_A, pc〉, one〉 367 else 368 let pc,b1 = next pc in let pc,b2 = next pc in 〈〈LCALL (ADDR16 (mk_word b1 b2)), pc〉, two〉 369 else 370 let 〈b,v〉≝ head8 v in if b then 371 assert false 372 else 373 let pc,b1 = next pc in let pc,b2 = next pc in 〈〈JBC (BIT b1, REL b2), pc〉, two〉 374 else 375 let 〈b,v〉≝ head8 v in if b then 376 〈〈INC (REGISTER v), pc〉, one〉 377 else 378 let 〈b,v〉≝ head8 v in if b then 379 let 〈b,v〉≝ head8 v in if b then 380 〈〈INC (INDIRECT v), pc〉, one〉 381 else 382 let 〈b,v〉≝ head8 v in if b then 383 let pc,b1 = next pc in 〈〈INC (DIRECT b1), pc〉, one〉 384 else 385 〈〈INC ACC_A, pc〉, one〉 386 else 387 let 〈b,v〉≝ head8 v in if b then 388 let 〈b,v〉≝ head8 v in if b then 389 〈〈RR ACC_A, pc〉, one〉 390 else 391 let pc,b1 = next pc in let pc,b2 = next pc in 〈〈LJMP (ADDR16 (mk_word b1 b2)), pc〉, two〉 392 else 393 let 〈b,v〉≝ head8 v in if b then 394 assert false 395 else 396 〈〈NOP, pc〉, one〉. 19 397 @. 20 398 nqed. 21 22 23 (*24 (* timings taken from SIEMENS *)25 26 let fetch pmem pc =27 let next pc =28 let _carry, res = half_add pc (vect_of_int 1 `Sixteen) in29 res, WordMap.find pc pmem30 in31 let pc,instr = next pc in32 let un, ln = from_byte instr in33 let bits = (from_nibble un, from_nibble ln) in34 match bits with35 (a10,a9,a8,true),(false,false,false,true) >36 let pc,b1 = next pc in37 `ACALL (`ADDR11 (mk_word11 a10 a9 a8 b1)), pc, 238  (false,false,true,false),(true,r1,r2,r3) >39 `ADD (`A,`REG (r1,r2,r3)), pc, 140  (false,false,true,false),(false,true,false,true) >41 let pc,b1 = next pc in42 `ADD (`A,`DIRECT b1), pc, 143  (false,false,true,false),(false,true,true,i1) >44 `ADD (`A,`INDIRECT i1), pc, 145  (false,false,true,false),(false,true,false,false) >46 let pc,b1 = next pc in47 `ADD (`A,`DATA b1), pc, 148  (false,false,true,true),(true,r1,r2,r3) >49 `ADDC (`A,`REG (r1,r2,r3)), pc, 150  (false,false,true,true),(false,true,false,true) >51 let pc,b1 = next pc in52 `ADDC (`A,`DIRECT b1), pc, 153  (false,false,true,true),(false,true,true,i1) >54 `ADDC (`A,`INDIRECT i1), pc, 155  (false,false,true,true),(false,true,false,false) >56 let pc,b1 = next pc in57 `ADDC (`A,`DATA b1), pc, 158  (a10,a9,a8,false),(false,false,false,true) >59 let pc,b1 = next pc in60 `AJMP (`ADDR11 (mk_word11 a10 a9 a8 b1)), pc, 261  (false,true,false,true),(true,r1,r2,r3) >62 `ANL (`U1 (`A, `REG (r1,r2,r3))), pc, 163  (false,true,false,true),(false,true,false,true) >64 let pc,b1 = next pc in65 `ANL (`U1 (`A, `DIRECT b1)), pc, 166  (false,true,false,true),(false,true,true,i1) >67 `ANL (`U1 (`A, `INDIRECT i1)), pc, 168  (false,true,false,true),(false,true,false,false) >69 let pc,b1 = next pc in70 `ANL (`U1 (`A, `DATA b1)), pc, 171  (false,true,false,true),(false,false,true,false) >72 let pc,b1 = next pc in73 `ANL (`U2 (`DIRECT b1,`A)), pc, 174  (false,true,false,true),(false,false,true,true) >75 let pc,b1 = next pc in76 let pc,b2 = next pc in77 `ANL (`U2 (`DIRECT b1,`DATA b2)), pc, 278  (true,false,false,false),(false,false,true,false) >79 let pc,b1 = next pc in80 `ANL (`U3 (`C,`BIT b1)), pc, 281  (true,false,true,true),(false,false,false,false) >82 let pc,b1 = next pc in83 `ANL (`U3 (`C,`NBIT b1)), pc, 284  (true,false,true,true),(false,true,false,true) >85 let pc,b1 = next pc in86 let pc,b2 = next pc in87 `CJNE (`U1 (`A, `DIRECT b1), `REL b2), pc, 288  (true,false,true,true),(false,true,false,false) >89 let pc,b1 = next pc in90 let pc,b2 = next pc in91 `CJNE (`U1 (`A, `DATA b1), `REL b2), pc, 292  (true,false,true,true),(true,r1,r2,r3) >93 let pc,b1 = next pc in94 let pc,b2 = next pc in95 `CJNE (`U2 (`REG(r1,r2,r3), `DATA b1), `REL b2), pc, 296  (true,false,true,true),(false,true,true,i1) >97 let pc,b1 = next pc in98 let pc,b2 = next pc in99 `CJNE (`U2 (`INDIRECT i1, `DATA b1), `REL b2), pc, 2100  (true,true,true,false),(false,true,false,false) >101 `CLR `A, pc, 1102  (true,true,false,false),(false,false,true,true) >103 `CLR `C, pc, 1104  (true,true,false,false),(false,false,true,false) >105 let pc,b1 = next pc in106 `CLR (`BIT b1), pc, 1107  (true,true,true,true),(false,true,false,false) >108 `CPL `A, pc, 1109  (true,false,true,true),(false,false,true,true) >110 `CPL `C, pc, 1111  (true,false,true,true),(false,false,true,false) >112 let pc,b1 = next pc in113 `CPL (`BIT b1), pc, 1114  (true,true,false,true),(false,true,false,false) >115 `DA `A, pc, 1116  (false,false,false,true),(false,true,false,false) >117 `DEC `A, pc, 1118  (false,false,false,true),(true,r1,r2,r3) >119 `DEC (`REG(r1,r2,r3)), pc, 1120  (false,false,false,true),(false,true,false,true) >121 let pc,b1 = next pc in122 `DEC (`DIRECT b1), pc, 1123  (false,false,false,true),(false,true,true,i1) >124 `DEC (`INDIRECT i1), pc, 1125  (true,false,false,false),(false,true,false,false) >126 `DIV (`A, `B), pc, 4127  (true,true,false,true),(true,r1,r2,r3) >128 let pc,b1 = next pc in129 `DJNZ (`REG(r1,r2,r3), `REL b1), pc, 2130  (true,true,false,true),(false,true,false,true) >131 let pc,b1 = next pc in132 let pc,b2 = next pc in133 `DJNZ (`DIRECT b1, `REL b2), pc, 2134  (false,false,false,false),(false,true,false,false) >135 `INC `A, pc, 1136  (false,false,false,false),(true,r1,r2,r3) >137 `INC (`REG(r1,r2,r3)), pc, 1138  (false,false,false,false),(false,true,false,true) >139 let pc,b1 = next pc in140 `INC (`DIRECT b1), pc, 1141  (false,false,false,false),(false,true,true,i1) >142 `INC (`INDIRECT i1), pc, 1143  (true,false,true,false),(false,false,true,true) >144 `INC `DPTR, pc, 2145  (false,false,true,false),(false,false,false,false) >146 let pc,b1 = next pc in147 let pc,b2 = next pc in148 `JB (`BIT b1, `REL b2), pc, 2149  (false,false,false,true),(false,false,false,false) >150 let pc,b1 = next pc in151 let pc,b2 = next pc in152 `JBC (`BIT b1, `REL b2), pc, 2153  (false,true,false,false),(false,false,false,false) >154 let pc,b1 = next pc in155 `JC (`REL b1), pc, 2156  (false,true,true,true),(false,false,true,true) >157 `JMP `IND_DPTR, pc, 2158  (false,false,true,true),(false,false,false,false) >159 let pc,b1 = next pc in160 let pc,b2 = next pc in161 `JNB (`BIT b1, `REL b2), pc, 2162  (false,true,false,true),(false,false,false,false) >163 let pc,b1 = next pc in164 `JNC (`REL b1), pc, 2165  (false,true,true,true),(false,false,false,false) >166 let pc,b1 = next pc in167 `JNZ (`REL b1), pc, 2168  (false,true,true,false),(false,false,false,false) >169 let pc,b1 = next pc in170 `JZ (`REL b1), pc, 2171  (false,false,false,true),(false,false,true,false) >172 let pc,b1 = next pc in173 let pc,b2 = next pc in174 `LCALL (`ADDR16 (mk_word b1 b2)), pc, 2175  (false,false,false,false),(false,false,true,false) >176 let pc,b1 = next pc in177 let pc,b2 = next pc in178 `LJMP (`ADDR16 (mk_word b1 b2)), pc, 2179  (true,true,true,false),(true,r1,r2,r3) >180 `MOV (`U1 (`A, `REG(r1,r2,r3))), pc, 1181  (true,true,true,false),(false,true,false,true) >182 let pc,b1 = next pc in183 `MOV (`U1 (`A, `DIRECT b1)), pc, 1184  (true,true,true,false),(false,true,true,i1) >185 `MOV (`U1 (`A, `INDIRECT i1)), pc, 1186  (false,true,true,true),(false,true,false,false) >187 let pc,b1 = next pc in188 `MOV (`U1 (`A, `DATA b1)), pc, 1189  (true,true,true,true),(true,r1,r2,r3) >190 `MOV (`U2 (`REG(r1,r2,r3), `A)), pc, 1191  (true,false,true,false),(true,r1,r2,r3) >192 let pc,b1 = next pc in193 `MOV (`U2 (`REG(r1,r2,r3), (`DIRECT b1))), pc, 2194  (false,true,true,true),(true,r1,r2,r3) >195 let pc,b1 = next pc in196 `MOV (`U2 (`REG(r1,r2,r3), (`DATA b1))), pc, 1197  (true,true,true,true),(false,true,false,true) >198 let pc,b1 = next pc in199 `MOV (`U3 (`DIRECT b1, `A)), pc, 1200  (true,false,false,false),(true,r1,r2,r3) >201 let pc,b1 = next pc in202 `MOV (`U3 (`DIRECT b1, `REG(r1,r2,r3))), pc, 2203  (true,false,false,false),(false,true,false,true) >204 let pc,b1 = next pc in205 let pc,b2 = next pc in206 `MOV (`U3 (`DIRECT b1, `DIRECT b2)), pc, 2207  (true,false,false,false),(false,true,true,i1) >208 let pc,b1 = next pc in209 `MOV (`U3 (`DIRECT b1, `INDIRECT i1)), pc, 2210  (false,true,true,true),(false,true,false,true) >211 let pc,b1 = next pc in212 let pc,b2 = next pc in213 `MOV (`U3 (`DIRECT b1, `DATA b2)), pc, 3214  (true,true,true,true),(false,true,true,i1) >215 `MOV (`U2 (`INDIRECT i1, `A)), pc, 1216  (true,false,true,false),(false,true,true,i1) >217 let pc,b1 = next pc in218 `MOV (`U2 (`INDIRECT i1, `DIRECT b1)), pc, 2219  (false,true,true,true),(false,true,true,i1) >220 let pc,b1 = next pc in221 `MOV (`U2 (`INDIRECT i1, `DATA b1)), pc, 1222  (true,false,true,false),(false,false,true,false) >223 let pc,b1 = next pc in224 `MOV (`U5 (`C, `BIT b1)), pc, 1225  (true,false,false,true),(false,false,true,false) >226 let pc,b1 = next pc in227 `MOV (`U6 (`BIT b1, `C)), pc, 2228  (true,false,false,true),(false,false,false,false) >229 let pc,b1 = next pc in230 let pc,b2 = next pc in231 `MOV (`U4 (`DPTR, `DATA16(mk_word b1 b2))), pc, 2232  (true,false,false,true),(false,false,true,true) >233 `MOVC (`A, `A_DPTR), pc, 2234  (true,false,false,false),(false,false,true,true) >235 `MOVC (`A, `A_PC), pc, 2236  (true,true,true,false),(false,false,true,i1) >237 `MOVX (`U1 (`A, `EXT_INDIRECT i1)), pc, 2238  (true,true,true,false),(false,false,false,false) >239 `MOVX (`U1 (`A, `EXT_IND_DPTR)), pc, 2240  (true,true,true,true),(false,false,true,i1) >241 `MOVX (`U2 (`EXT_INDIRECT i1, `A)), pc, 2242  (true,true,true,true),(false,false,false,false) >243 `MOVX (`U2 (`EXT_IND_DPTR, `A)), pc, 2244  (true,false,true,false),(false,true,false,false) >245 `MUL(`A, `B), pc, 4246  (false,false,false,false),(false,false,false,false) >247 `NOP, pc, 1248  (false,true,false,false),(true,r1,r2,r3) >249 `ORL (`U1(`A, `REG(r1,r2,r3))), pc, 1250  (false,true,false,false),(false,true,false,true) >251 let pc,b1 = next pc in252 `ORL (`U1(`A, `DIRECT b1)), pc, 1253  (false,true,false,false),(false,true,true,i1) >254 `ORL (`U1(`A, `INDIRECT i1)), pc, 1255  (false,true,false,false),(false,true,false,false) >256 let pc,b1 = next pc in257 `ORL (`U1(`A, `DATA b1)), pc, 1258  (false,true,false,false),(false,false,true,false) >259 let pc,b1 = next pc in260 `ORL (`U2(`DIRECT b1, `A)), pc, 1261  (false,true,false,false),(false,false,true,true) >262 let pc,b1 = next pc in263 let pc,b2 = next pc in264 `ORL (`U2 (`DIRECT b1, `DATA b2)), pc, 2265  (false,true,true,true),(false,false,true,false) >266 let pc,b1 = next pc in267 `ORL (`U3 (`C, `BIT b1)), pc, 2268  (true,false,true,false),(false,false,false,false) >269 let pc,b1 = next pc in270 `ORL (`U3 (`C, `NBIT b1)), pc, 2271  (true,true,false,true),(false,false,false,false) >272 let pc,b1 = next pc in273 `POP (`DIRECT b1), pc, 2274  (true,true,false,false),(false,false,false,false) >275 let pc,b1 = next pc in276 `PUSH (`DIRECT b1), pc, 2277  (false,false,true,false),(false,false,true,false) >278 `RET, pc, 2279  (false,false,true,true),(false,false,true,false) >280 `RETI, pc, 2281  (false,false,true,false),(false,false,true,true) >282 `RL `A, pc, 1283  (false,false,true,true),(false,false,true,true) >284 `RLC `A, pc, 1285  (false,false,false,false),(false,false,true,true) >286 `RR `A, pc, 1287  (false,false,false,true),(false,false,true,true) >288 `RRC `A, pc, 1289  (true,true,false,true),(false,false,true,true) >290 `SETB `C, pc, 1291  (true,true,false,true),(false,false,true,false) >292 let pc,b1 = next pc in293 `SETB (`BIT b1), pc, 1294  (true,false,false,false),(false,false,false,false) >295 let pc,b1 = next pc in296 `SJMP (`REL b1), pc, 2297  (true,false,false,true),(true,r1,r2,r3) >298 `SUBB (`A, `REG(r1,r2,r3)), pc, 1299  (true,false,false,true),(false,true,false,true) >300 let pc,b1 = next pc in301 `SUBB (`A, `DIRECT b1), pc, 1302  (true,false,false,true),(false,true,true,i1) >303 `SUBB (`A, `INDIRECT i1), pc, 1304  (true,false,false,true),(false,true,false,false) >305 let pc,b1 = next pc in306 `SUBB (`A, `DATA b1), pc, 1307  (true,true,false,false),(false,true,false,false) >308 `SWAP `A, pc, 1309  (true,true,false,false),(true,r1,r2,r3) >310 `XCH (`A, `REG(r1,r2,r3)), pc, 1311  (true,true,false,false),(false,true,false,true) >312 let pc,b1 = next pc in313 `XCH (`A, `DIRECT b1), pc, 1314  (true,true,false,false),(false,true,true,i1) >315 `XCH (`A, `INDIRECT i1), pc, 1316  (true,true,false,true),(false,true,true,i1) >317 `XCHD(`A, `INDIRECT i1), pc, 1318  (false,true,true,false),(true,r1,r2,r3) >319 `XRL(`U1(`A, `REG(r1,r2,r3))), pc, 1320  (false,true,true,false),(false,true,false,true) >321 let pc,b1 = next pc in322 `XRL(`U1(`A, `DIRECT b1)), pc, 1323  (false,true,true,false),(false,true,true,i1) >324 `XRL(`U1(`A, `INDIRECT i1)), pc, 1325  (false,true,true,false),(false,true,false,false) >326 let pc,b1 = next pc in327 `XRL(`U1(`A, `DATA b1)), pc, 1328  (false,true,true,false),(false,false,true,false) >329 let pc,b1 = next pc in330 `XRL(`U2(`DIRECT b1, `A)), pc, 1331  (false,true,true,false),(false,false,true,true) >332 let pc,b1 = next pc in333 let pc,b2 = next pc in334 `XRL(`U2(`DIRECT b1, `DATA b2)), pc, 2335  _,_ > assert false336 ;;337 338 339 *)340 341 342 343 (*344 nrecord Sigma (A: Type[0]) (T: A → Type[0]) : Type[0] ≝ {345 elem:> A;346 witness: T elem347 }.348 349 interpretation "Sigma" 'sigma T = (Sigma ? T).350 351 naxiom daemon: False.352 353 naxiom decode_register: Vector Bool (S (S (S Z))) → [reg].354 naxiom decode_direct: Vector Bool (S (S (S Z))) → [direct].355 356 ndefinition decode_tbl0: List ((Σn.Vector Bool n) × (Vector Bool (S (S (S Z))) → Instruction))357 ≝358 [mk_Cartesian ??359 (mk_Sigma ? (λn.Vector Bool n) ? [ false; false; true; false; true])360 (λl.361 ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)362 (mk_subaddressing_mode ? ? (decode_register l) ?));363 mk_Cartesian ??364 (mk_Sigma ? (λn.Vector Bool n) ? [ false; false; true; false; true])365 (λl.366 ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)367 (mk_subaddressing_mode ? ? (decode_direct l) ?)) ].368 ncases daemon.369 nqed.370 371 372 naxiom decode_register: List Bool → [reg].373 naxiom decode_direct: List Bool → [direct].374 375 ndefinition decode_tbl0: List (List Bool × (List Bool → Instruction))376 ≝377 [mk_Cartesian ??378 [ false; false; true; false; true]379 (λl.380 ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)381 (mk_subaddressing_mode ? ? (decode_register l) ?));382 mk_Cartesian ??383 [ false; false; true; false; true]384 (λl.385 ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)386 (mk_subaddressing_mode ? ? (decode_direct l) ?)) ].387 ncases daemon.388 nqed.389 390 391 ndefinition decode_tbl1:392 List (List Bool × Σaddr:all_types. [addr] → Instruction)393 ≝394 [mk_Cartesian ??395 [ false; false; true; false; true]396 (mk_Sigma ? (λaddr:all_types. [addr] → Instruction)397 reg398 (λa.399 ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)400 (mk_subaddressing_mode ? ? a ?))) ].401 ncases daemon.402 nqed.403 404 ndefinition decode_tbl2:405 List (List Bool × Σaddr:all_types. [addr] → Instruction)406 ≝407 [mk_Cartesian ??408 [ false; false; true; false; false; true; false; true]409 (mk_Sigma ? (λaddr:all_types. [addr] → Instruction)410 direct411 (λa.412 ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)413 (mk_subaddressing_mode ? ? a ?))) ].414 ncases daemon.415 nqed.416 417 ndefinition decode_tbl ≝ decode_tbl1 @ decode_tbl2.418 419 decode_addr_mode; ∀addr:all_types. List Bool → [addr].420 421 decode ≝422 λl:List Bit.423 List.iter424 (fun l0 addr mk_f →425 match split_prefix l l0 with426 [ None ⇒ ...427  Some r ⇒ mk_f (decode_addr_mode r) ]428 429 ) decode_tbl430 431 encode ≝432 433 ndefinition decode_tbl:434 List (List Bool × Σaddr:all_types. [addr] → Instruction)435 ≝436 [mk_Cartesian ??437 [ False; False; True; False; True]438 (mk_Sigma all_types (λaddr:all_types. [addr] → Instruction)439 reg440 (λa:subaddressing_mode ? [reg].441 ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)442 (mk_subaddressing_mode ? ? a ?)));443 mk_Cartesian ??444 [ False; False; True; False; False; True; False; True]445 (mk_Sigma all_types (λaddr:all_types. [addr] → Instruction)446 direct447 (λa:subaddressing_mode ? [direct].448 ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)449 (mk_subaddressing_mode ? ? a ?)))450 ].451 nnormalize;452 453 ].454 *)455
Note: See TracChangeset
for help on using the changeset viewer.