Changeset 319
 Timestamp:
 Nov 26, 2010, 6:12:45 PM (11 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Fetch.ma
r318 r319 26 26 let 〈b,v〉≝ head8 v in if b then 27 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〉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 pmem pc in 〈〈MOV (U3 (DIRECT b1) ACC_A), pc〉, one〉 36 36 else 37 37 〈〈CPL ACC_A, pc〉, one〉 38 38 else 39 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〉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 pmem pc in 〈〈MOV (U1 A (DIRECT b1)), pc〉, one〉 56 56 else 57 57 〈〈CLR ACC_A, pc〉, one〉 58 58 else 59 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〉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 66 else 67 67 let 〈b,v〉≝ head8 v in if b then 68 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〉69 let 〈pc,b1〉≝ next pmem 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 pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈DJNZ (DIRECT b1) (REL b2), pc〉, two〉 77 77 else 78 78 〈〈DA ACC_A, pc〉, one〉 … … 82 82 〈〈SETB C, pc〉, one〉 83 83 else 84 let pc,b1 = nextpc 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 = nextpc 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〉84 let 〈pc,b1〉≝ next pmem 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 pmem 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 pmem pc in 〈〈XCH A (DIRECT b1), pc〉, one〉 100 100 else 101 101 〈〈SWAP ACC_A, pc〉, one〉 … … 105 105 〈〈CLR C, pc〉, one〉 106 106 else 107 let pc,b1 = nextpc 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 = nextpc in 〈〈PUSH (DIRECT b1), pc〉, two〉107 let 〈pc,b1〉≝ next pmem 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 pmem pc in 〈〈PUSH (DIRECT b1), pc〉, two〉 113 113 else 114 114 let 〈b,v〉≝ head8 v in if b then 115 115 let 〈b,v〉≝ head8 v in if b then 116 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〉117 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem 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 pmem pc in let 〈pc,b2〉≝ next pmem 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 pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈CJNE (U1 A (DIRECT b1)) (REL b2), pc〉, two〉 125 else 126 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈CJNE (U1 A (DATA b1)) (REL b2), pc〉, two〉 127 127 else 128 128 let 〈b,v〉≝ head8 v in if b then … … 130 130 〈〈CPL C, pc〉, one〉 131 131 else 132 let pc,b1 = nextpc 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〉132 let 〈pc,b1〉≝ next pmem 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 pmem 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 pmem 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 pmem pc in 〈〈MOV (U2 (INDIRECT v) (DIRECT b1)), pc〉, two〉 145 else 146 〈〈MUL A B, pc〉, four〉 147 147 else 148 148 let 〈b,v〉≝ head8 v in if b then … … 150 150 〈〈INC DPTR, pc〉, two〉 151 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〉152 let 〈pc,b1〉≝ next pmem 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 pmem pc in 〈〈ORL (U3 C (NBIT b1)), pc〉, two〉 158 158 else 159 159 let 〈b,v〉≝ head8 v in if b then 160 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 = nextpc in 〈〈SJMP (REL b1), pc〉, two〉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 pmem pc in 〈〈SUBB A (DIRECT b1), pc〉, one〉 169 else 170 let 〈pc,b1〉≝ next pmem 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 pmem 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 pmem pc in let 〈pc,b2〉≝ next pmem 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 pmem 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 pmem 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 pmem pc in let 〈pc,b2〉≝ next pmem 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 pmem 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 pmem pc in 〈〈SJMP (REL b1), pc〉, two〉 205 205 else 206 206 let 〈b,v〉≝ head8 v in if b then … … 208 208 let 〈b,v〉≝ head8 v in if b then 209 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〉210 let 〈pc,b1〉≝ next pmem 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 pmem 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 pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈MOV (U3 (DIRECT b1) (DATA b2)), pc〉, three〉 218 else 219 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV (U1 A (DATA b1)), pc〉, one〉 220 220 else 221 221 let 〈b,v〉≝ head8 v in if b then … … 223 223 〈〈JMP IND_DPTR, pc〉, two〉 224 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 = nextpc 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 = nextpc in 〈〈JZ (REL b1), pc〉, two〉225 let 〈pc,b1〉≝ next pmem 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 pmem 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 pmem pc in 〈〈XRL(U1 A (DIRECT b1)), pc〉, one〉 241 else 242 let 〈pc,b1〉≝ next pmem 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 pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈XRL(U2 (DIRECT b1) (DATA b2)), pc〉, two〉 247 else 248 let 〈pc,b1〉≝ next pmem 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 pmem pc in 〈〈JZ (REL b1), pc〉, two〉 254 254 else 255 255 let 〈b,v〉≝ head8 v in if b then 256 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 = nextpc 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 = nextpc in 〈〈JC (REL b1), pc〉, two〉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 pmem pc in 〈〈ANL (U1 A (DIRECT b1)), pc〉, one〉 265 else 266 let 〈pc,b1〉≝ next pmem 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 pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈ANL (U2 (DIRECT b1) (DATA b2)), pc〉, two〉 271 else 272 let 〈pc,b1〉≝ next pmem 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 pmem 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 pmem pc in 〈〈ORL (U1 A (DIRECT b1)), pc〉, one〉 288 else 289 let 〈pc,b1〉≝ next pmem 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 pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈ORL (U2 (DIRECT b1) (DATA b2)), pc〉, two〉 294 else 295 let 〈pc,b1〉≝ next pmem 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 pmem pc in 〈〈JC (REL b1), pc〉, two〉 301 301 else 302 302 let 〈b,v〉≝ head8 v in if b then 303 303 let 〈b,v〉≝ head8 v in if b then 304 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〉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 pmem pc in 〈〈ADDC A (DIRECT b1), pc〉, one〉 313 else 314 let 〈pc,b1〉≝ next pmem pc in 〈〈ADDC A (DATA b1), pc〉, one〉 315 315 else 316 316 let 〈b,v〉≝ head8 v in if b then … … 323 323 assert false 324 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〉325 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem 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 pmem pc in 〈〈ADD A (DIRECT b1), pc〉, one〉 336 else 337 let 〈pc,b1〉≝ next pmem pc in 〈〈ADD A (DATA b1), pc〉, one〉 338 338 else 339 339 let 〈b,v〉≝ head8 v in if b then … … 347 347 assert false 348 348 else 349 let pc,b1 = next pc in let pc,b2 = next pc in 〈〈JB (BIT b1,REL b2), pc〉, two〉349 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈JB (BIT b1) (REL b2), pc〉, two〉 350 350 else 351 351 let 〈b,v〉≝ head8 v in if b then … … 358 358 else 359 359 let 〈b,v〉≝ head8 v in if b then 360 let pc,b1 = nextpc in 〈〈DEC (DIRECT b1), pc〉, one〉360 let 〈pc,b1〉≝ next pmem pc in 〈〈DEC (DIRECT b1), pc〉, one〉 361 361 else 362 362 〈〈DEC ACC_A, pc〉, one〉 … … 366 366 〈〈RRC ACC_A, pc〉, one〉 367 367 else 368 let pc,b1 = next pc in let pc,b2 = nextpc 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〉368 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem 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 pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈JBC (BIT b1) (REL b2), pc〉, two〉 374 374 else 375 375 let 〈b,v〉≝ head8 v in if b then … … 381 381 else 382 382 let 〈b,v〉≝ head8 v in if b then 383 let pc,b1 = nextpc in 〈〈INC (DIRECT b1), pc〉, one〉383 let 〈pc,b1〉≝ next pmem pc in 〈〈INC (DIRECT b1), pc〉, one〉 384 384 else 385 385 〈〈INC ACC_A, pc〉, one〉 … … 389 389 〈〈RR ACC_A, pc〉, one〉 390 390 else 391 let pc,b1 = next pc in let pc,b2 = nextpc in 〈〈LJMP (ADDR16 (mk_word b1 b2)), pc〉, two〉391 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈LJMP (ADDR16 (mk_word b1 b2)), pc〉, two〉 392 392 else 393 393 let 〈b,v〉≝ head8 v in if b then
Note: See TracChangeset
for help on using the changeset viewer.