Changeset 820 for src/ASM/Fetch.ma
 Timestamp:
 May 20, 2011, 6:09:00 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

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