 Timestamp:
 May 23, 2011, 3:23:17 PM (10 years ago)
 Location:
 src/ASM
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Interpret.ma
r820 r821 158 158 include alias "ASM/BitVectorTrie.ma". 159 159 160 definition execute_1_preinstruction: ∀A : Type[0]. (A → Byte) → preinstruction A → Status → Status≝161 λA : Type[0].160 definition execute_1_preinstruction: ∀A, M: Type[0]. (A → Byte) → preinstruction A → PreStatus M → PreStatus M ≝ 161 λA, M: Type[0]. 162 162 λaddr_of: A → Byte. 163 163 λinstr: preinstruction A. 164 λs: Status.164 λs: PreStatus M. 165 165 match instr with 166 166 [ ADD addr1 addr2 ⇒ 167 let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false addr1)168 (get_arg_8 s false addr2) false in167 let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 ? s false addr1) 168 (get_arg_8 ? s false addr2) false in 169 169 let cy_flag ≝ get_index' ? O ? flags in 170 170 let ac_flag ≝ get_index' ? 1 ? flags in 171 171 let ov_flag ≝ get_index' ? 2 ? flags in 172 let s ≝ set_arg_8 s ACC_A result in173 set_flags s cy_flag (Some Bit ac_flag) ov_flag172 let s ≝ set_arg_8 ? s ACC_A result in 173 set_flags ? s cy_flag (Some Bit ac_flag) ov_flag 174 174  ADDC addr1 addr2 ⇒ 175 let old_cy_flag ≝ get_cy_flag s in176 let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false addr1)177 (get_arg_8 s false addr2) old_cy_flag in175 let old_cy_flag ≝ get_cy_flag ? s in 176 let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 ? s false addr1) 177 (get_arg_8 ? s false addr2) old_cy_flag in 178 178 let cy_flag ≝ get_index' ? O ? flags in 179 179 let ac_flag ≝ get_index' ? 1 ? flags in 180 180 let ov_flag ≝ get_index' ? 2 ? flags in 181 let s ≝ set_arg_8 s ACC_A result in182 set_flags s cy_flag (Some Bit ac_flag) ov_flag181 let s ≝ set_arg_8 ? s ACC_A result in 182 set_flags ? s cy_flag (Some Bit ac_flag) ov_flag 183 183  SUBB addr1 addr2 ⇒ 184 let old_cy_flag ≝ get_cy_flag s in185 let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 s false addr1)186 (get_arg_8 s false addr2) old_cy_flag in184 let old_cy_flag ≝ get_cy_flag ? s in 185 let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 ? s false addr1) 186 (get_arg_8 ? s false addr2) old_cy_flag in 187 187 let cy_flag ≝ get_index' ? O ? flags in 188 188 let ac_flag ≝ get_index' ? 1 ? flags in 189 189 let ov_flag ≝ get_index' ? 2 ? flags in 190 let s ≝ set_arg_8 s ACC_A result in191 set_flags s cy_flag (Some Bit ac_flag) ov_flag190 let s ≝ set_arg_8 ? s ACC_A result in 191 set_flags ? s cy_flag (Some Bit ac_flag) ov_flag 192 192  ANL addr ⇒ 193 193 match addr with … … 196 196 [ inl l' ⇒ 197 197 let 〈addr1, addr2〉 ≝ l' in 198 let and_val ≝ conjunction_bv ? (get_arg_8 s true addr1) (get_arg_8s true addr2) in199 set_arg_8 s addr1 and_val198 let and_val ≝ conjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in 199 set_arg_8 ? s addr1 and_val 200 200  inr r ⇒ 201 201 let 〈addr1, addr2〉 ≝ r in 202 let and_val ≝ conjunction_bv ? (get_arg_8 s true addr1) (get_arg_8s true addr2) in203 set_arg_8 s addr1 and_val202 let and_val ≝ conjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in 203 set_arg_8 ? s addr1 and_val 204 204 ] 205 205  inr r ⇒ 206 206 let 〈addr1, addr2〉 ≝ r in 207 let and_val ≝ (get_cy_flag s) ∧ (get_arg_1s addr2 true) in208 set_flags s and_val (None ?) (get_ov_flags)207 let and_val ≝ (get_cy_flag ? s) ∧ (get_arg_1 ? s addr2 true) in 208 set_flags ? s and_val (None ?) (get_ov_flag ? s) 209 209 ] 210 210  ORL addr ⇒ … … 214 214 [ inl l' ⇒ 215 215 let 〈addr1, addr2〉 ≝ l' in 216 let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8s true addr2) in217 set_arg_8 s addr1 or_val216 let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in 217 set_arg_8 ? s addr1 or_val 218 218  inr r ⇒ 219 219 let 〈addr1, addr2〉 ≝ r in 220 let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8s true addr2) in221 set_arg_8 s addr1 or_val220 let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in 221 set_arg_8 ? s addr1 or_val 222 222 ] 223 223  inr r ⇒ 224 224 let 〈addr1, addr2〉 ≝ r in 225 let or_val ≝ (get_cy_flag s) ∨ (get_arg_1s addr2 true) in226 set_flags s or_val (None ?) (get_ov_flags)225 let or_val ≝ (get_cy_flag ? s) ∨ (get_arg_1 ? s addr2 true) in 226 set_flags ? s or_val (None ?) (get_ov_flag ? s) 227 227 ] 228 228  XRL addr ⇒ … … 230 230 [ inl l' ⇒ 231 231 let 〈addr1, addr2〉 ≝ l' in 232 let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8s true addr2) in233 set_arg_8 s addr1 xor_val232 let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in 233 set_arg_8 ? s addr1 xor_val 234 234  inr r ⇒ 235 235 let 〈addr1, addr2〉 ≝ r in 236 let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8s true addr2) in237 set_arg_8 s addr1 xor_val236 let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in 237 set_arg_8 ? s addr1 xor_val 238 238 ] 239 239  INC addr ⇒ … … 244 244 dptr ]] x) → ? with 245 245 [ ACC_A ⇒ λacc_a: True. 246 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true ACC_A) (bitvector_of_nat 8 1) in247 set_arg_8 s ACC_A result246 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s true ACC_A) (bitvector_of_nat 8 1) in 247 set_arg_8 ? s ACC_A result 248 248  REGISTER r ⇒ λregister: True. 249 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true (REGISTER r)) (bitvector_of_nat 8 1) in250 set_arg_8 s (REGISTER r) result249 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s true (REGISTER r)) (bitvector_of_nat 8 1) in 250 set_arg_8 ? s (REGISTER r) result 251 251  DIRECT d ⇒ λdirect: True. 252 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true (DIRECT d)) (bitvector_of_nat 8 1) in253 set_arg_8 s (DIRECT d) result252 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s true (DIRECT d)) (bitvector_of_nat 8 1) in 253 set_arg_8 ? s (DIRECT d) result 254 254  INDIRECT i ⇒ λindirect: True. 255 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true (INDIRECT i)) (bitvector_of_nat 8 1) in256 set_arg_8 s (INDIRECT i) result255 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s true (INDIRECT i)) (bitvector_of_nat 8 1) in 256 set_arg_8 ? s (INDIRECT i) result 257 257  DPTR ⇒ λdptr: True. 258 let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr s SFR_DPL) (bitvector_of_nat 8 1) in259 let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr s SFR_DPH) (zero 8) carry in260 let s ≝ set_8051_sfr s SFR_DPL bl in261 set_8051_sfr s SFR_DPH bu258 let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr ? s SFR_DPL) (bitvector_of_nat 8 1) in 259 let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr ? s SFR_DPH) (zero 8) carry in 260 let s ≝ set_8051_sfr ? s SFR_DPL bl in 261 set_8051_sfr ? s SFR_DPH bu 262 262  _ ⇒ λother: False. ⊥ 263 263 ] (subaddressing_modein … addr) 264 264  DEC addr ⇒ 265 let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 s true addr) (bitvector_of_nat 8 1) false in266 set_arg_8 s addr result265 let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 ? s true addr) (bitvector_of_nat 8 1) false in 266 set_arg_8 ? s addr result 267 267  MUL addr1 addr2 ⇒ 268 let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr s SFR_ACC_A) in269 let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr s SFR_ACC_B) in268 let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_A) in 269 let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_B) in 270 270 let product ≝ acc_a_nat * acc_b_nat in 271 271 let ov_flag ≝ product ≥ 256 in 272 272 let low ≝ bitvector_of_nat 8 (product mod 256) in 273 273 let high ≝ bitvector_of_nat 8 (product ÷ 256) in 274 let s ≝ set_8051_sfr s SFR_ACC_A low in275 set_8051_sfr s SFR_ACC_B high274 let s ≝ set_8051_sfr ? s SFR_ACC_A low in 275 set_8051_sfr ? s SFR_ACC_B high 276 276  DIV addr1 addr2 ⇒ 277 let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr s SFR_ACC_A) in278 let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr s SFR_ACC_B) in277 let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_A) in 278 let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_B) in 279 279 match acc_b_nat with 280 [ O ⇒ set_flags s false (None Bit) true280 [ O ⇒ set_flags ? s false (None Bit) true 281 281  S o ⇒ 282 282 let q ≝ bitvector_of_nat 8 (acc_a_nat ÷ (S o)) in 283 283 let r ≝ bitvector_of_nat 8 (acc_a_nat mod 256) in 284 let s ≝ set_8051_sfr s SFR_ACC_A q in285 let s ≝ set_8051_sfr s SFR_ACC_B r in286 set_flags s false (None Bit) false284 let s ≝ set_8051_sfr ? s SFR_ACC_A q in 285 let s ≝ set_8051_sfr ? s SFR_ACC_B r in 286 set_flags ? s false (None Bit) false 287 287 ] 288 288  DA addr ⇒ 289 let 〈 acc_nu, acc_nl 〉 ≝ split ? 4 4 (get_8051_sfr s SFR_ACC_A) in290 if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag s) then291 let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr s SFR_ACC_A) (bitvector_of_nat 8 6) false in289 let 〈 acc_nu, acc_nl 〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_ACC_A) in 290 if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag ? s) then 291 let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr ? s SFR_ACC_A) (bitvector_of_nat 8 6) false in 292 292 let cy_flag ≝ get_index' ? O ? flags in 293 293 let 〈acc_nu', acc_nl'〉 ≝ split ? 4 4 result in … … 295 295 let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in 296 296 let new_acc ≝ nu @@ acc_nl' in 297 let s ≝ set_8051_sfr s SFR_ACC_A new_acc in298 set_flags s cy_flag (Some ? (get_ac_flag s)) (get_ov_flags)297 let s ≝ set_8051_sfr ? s SFR_ACC_A new_acc in 298 set_flags ? s cy_flag (Some ? (get_ac_flag ? s)) (get_ov_flag ? s) 299 299 else 300 300 s … … 303 303  CLR addr ⇒ 304 304 match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with 305 [ ACC_A ⇒ λacc_a: True. set_arg_8 s ACC_A (zero 8)306  CARRY ⇒ λcarry: True. set_arg_1 s CARRY false307  BIT_ADDR b ⇒ λbit_addr: True. set_arg_1 s (BIT_ADDR b) false305 [ ACC_A ⇒ λacc_a: True. set_arg_8 ? s ACC_A (zero 8) 306  CARRY ⇒ λcarry: True. set_arg_1 ? s CARRY false 307  BIT_ADDR b ⇒ λbit_addr: True. set_arg_1 ? s (BIT_ADDR b) false 308 308  _ ⇒ λother: False. ⊥ 309 309 ] (subaddressing_modein … addr) … … 311 311 match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with 312 312 [ ACC_A ⇒ λacc_a: True. 313 let old_acc ≝ get_8051_sfr s SFR_ACC_A in313 let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in 314 314 let new_acc ≝ negation_bv ? old_acc in 315 set_8051_sfr s SFR_ACC_A new_acc315 set_8051_sfr ? s SFR_ACC_A new_acc 316 316  CARRY ⇒ λcarry: True. 317 let old_cy_flag ≝ get_arg_1 s CARRY true in317 let old_cy_flag ≝ get_arg_1 ? s CARRY true in 318 318 let new_cy_flag ≝ ¬old_cy_flag in 319 set_arg_1 s CARRY new_cy_flag319 set_arg_1 ? s CARRY new_cy_flag 320 320  BIT_ADDR b ⇒ λbit_addr: True. 321 let old_bit ≝ get_arg_1 s (BIT_ADDR b) true in321 let old_bit ≝ get_arg_1 ? s (BIT_ADDR b) true in 322 322 let new_bit ≝ ¬old_bit in 323 set_arg_1 s (BIT_ADDR b) new_bit323 set_arg_1 ? s (BIT_ADDR b) new_bit 324 324  _ ⇒ λother: False. ? 325 325 ] (subaddressing_modein … addr) 326  SETB b ⇒ set_arg_1 s b false326  SETB b ⇒ set_arg_1 ? s b false 327 327  RL _ ⇒ (* DPM: always ACC_A *) 328 let old_acc ≝ get_8051_sfr s SFR_ACC_A in328 let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in 329 329 let new_acc ≝ rotate_left … 1 old_acc in 330 set_8051_sfr s SFR_ACC_A new_acc330 set_8051_sfr ? s SFR_ACC_A new_acc 331 331  RR _ ⇒ (* DPM: always ACC_A *) 332 let old_acc ≝ get_8051_sfr s SFR_ACC_A in332 let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in 333 333 let new_acc ≝ rotate_right … 1 old_acc in 334 set_8051_sfr s SFR_ACC_A new_acc334 set_8051_sfr ? s SFR_ACC_A new_acc 335 335  RLC _ ⇒ (* DPM: always ACC_A *) 336 let old_cy_flag ≝ get_cy_flag s in337 let old_acc ≝ get_8051_sfr s SFR_ACC_A in336 let old_cy_flag ≝ get_cy_flag ? s in 337 let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in 338 338 let new_cy_flag ≝ get_index' ? O ? old_acc in 339 339 let new_acc ≝ shift_left … 1 old_acc old_cy_flag in 340 let s ≝ set_arg_1 s CARRY new_cy_flag in341 set_8051_sfr s SFR_ACC_A new_acc340 let s ≝ set_arg_1 ? s CARRY new_cy_flag in 341 set_8051_sfr ? s SFR_ACC_A new_acc 342 342  RRC _ ⇒ (* DPM: always ACC_A *) 343 let old_cy_flag ≝ get_cy_flag s in344 let old_acc ≝ get_8051_sfr s SFR_ACC_A in343 let old_cy_flag ≝ get_cy_flag ? s in 344 let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in 345 345 let new_cy_flag ≝ get_index' ? 7 ? old_acc in 346 346 let new_acc ≝ shift_right … 1 old_acc old_cy_flag in 347 let s ≝ set_arg_1 s CARRY new_cy_flag in348 set_8051_sfr s SFR_ACC_A new_acc347 let s ≝ set_arg_1 ? s CARRY new_cy_flag in 348 set_8051_sfr ? s SFR_ACC_A new_acc 349 349  SWAP _ ⇒ (* DPM: always ACC_A *) 350 let old_acc ≝ get_8051_sfr s SFR_ACC_A in350 let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in 351 351 let 〈nu,nl〉 ≝ split ? 4 4 old_acc in 352 352 let new_acc ≝ nl @@ nu in 353 set_8051_sfr s SFR_ACC_A new_acc353 set_8051_sfr ? s SFR_ACC_A new_acc 354 354  PUSH addr ⇒ 355 355 match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → ? with 356 356 [ DIRECT d ⇒ λdirect: True. 357 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in358 let s ≝ set_8051_sfr s SFR_SP new_sp in359 write_at_stack_pointer s d357 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in 358 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 359 write_at_stack_pointer ? s d 360 360  _ ⇒ λother: False. ⊥ 361 361 ] (subaddressing_modein … addr) 362 362  POP addr ⇒ 363 let contents ≝ read_at_stack_pointer s in364 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) false in365 let s ≝ set_8051_sfr s SFR_SP new_sp in366 set_arg_8 s addr contents363 let contents ≝ read_at_stack_pointer ? s in 364 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in 365 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 366 set_arg_8 ? s addr contents 367 367  XCH addr1 addr2 ⇒ 368 let old_addr ≝ get_arg_8 s false addr2 in369 let old_acc ≝ get_8051_sfr s SFR_ACC_A in370 let s ≝ set_8051_sfr s SFR_ACC_A old_addr in371 set_arg_8 s addr2 old_acc368 let old_addr ≝ get_arg_8 ? s false addr2 in 369 let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in 370 let s ≝ set_8051_sfr ? s SFR_ACC_A old_addr in 371 set_arg_8 ? s addr2 old_acc 372 372  XCHD addr1 addr2 ⇒ 373 let 〈acc_nu, acc_nl〉 ≝ split … 4 4 (get_8051_sfr s SFR_ACC_A) in374 let 〈arg_nu, arg_nl〉 ≝ split … 4 4 (get_arg_8 s false addr2) in373 let 〈acc_nu, acc_nl〉 ≝ split … 4 4 (get_8051_sfr ? s SFR_ACC_A) in 374 let 〈arg_nu, arg_nl〉 ≝ split … 4 4 (get_arg_8 ? s false addr2) in 375 375 let new_acc ≝ acc_nu @@ arg_nl in 376 376 let new_arg ≝ arg_nu @@ acc_nl in 377 let s ≝ set_8051_sfr s SFR_ACC_A new_acc in378 set_arg_8 s addr2 new_arg377 let s ≝ set_8051_sfr ? s SFR_ACC_A new_acc in 378 set_arg_8 ? s addr2 new_arg 379 379  RET ⇒ 380 let high_bits ≝ read_at_stack_pointer s in381 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) false in382 let s ≝ set_8051_sfr s SFR_SP new_sp in383 let low_bits ≝ read_at_stack_pointer s in384 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) false in385 let s ≝ set_8051_sfr s SFR_SP new_sp in380 let high_bits ≝ read_at_stack_pointer ? s in 381 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in 382 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 383 let low_bits ≝ read_at_stack_pointer ? s in 384 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in 385 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 386 386 let new_pc ≝ high_bits @@ low_bits in 387 set_program_counter s new_pc387 set_program_counter ? s new_pc 388 388  RETI ⇒ 389 let high_bits ≝ read_at_stack_pointer s in390 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) false in391 let s ≝ set_8051_sfr s SFR_SP new_sp in392 let low_bits ≝ read_at_stack_pointer s in393 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) false in394 let s ≝ set_8051_sfr s SFR_SP new_sp in389 let high_bits ≝ read_at_stack_pointer ? s in 390 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in 391 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 392 let low_bits ≝ read_at_stack_pointer ? s in 393 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in 394 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 395 395 let new_pc ≝ high_bits @@ low_bits in 396 set_program_counter s new_pc396 set_program_counter ? s new_pc 397 397  MOVX addr ⇒ 398 398 (* DPM: only copies  doesn't affect I/O *) … … 400 400 [ inl l ⇒ 401 401 let 〈addr1, addr2〉 ≝ l in 402 set_arg_8 s addr1 (get_arg_8s false addr2)402 set_arg_8 ? s addr1 (get_arg_8 ? s false addr2) 403 403  inr r ⇒ 404 404 let 〈addr1, addr2〉 ≝ r in 405 set_arg_8 s addr1 (get_arg_8s false addr2)405 set_arg_8 ? s addr1 (get_arg_8 ? s false addr2) 406 406 ] 407 407  MOV addr ⇒ … … 417 417 [ inl l'''' ⇒ 418 418 let 〈addr1, addr2〉 ≝ l'''' in 419 set_arg_8 s addr1 (get_arg_8s false addr2)419 set_arg_8 ? s addr1 (get_arg_8 ? s false addr2) 420 420  inr r'''' ⇒ 421 421 let 〈addr1, addr2〉 ≝ r'''' in 422 set_arg_8 s addr1 (get_arg_8s false addr2)422 set_arg_8 ? s addr1 (get_arg_8 ? s false addr2) 423 423 ] 424 424  inr r''' ⇒ 425 425 let 〈addr1, addr2〉 ≝ r''' in 426 set_arg_8 s addr1 (get_arg_8s false addr2)426 set_arg_8 ? s addr1 (get_arg_8 ? s false addr2) 427 427 ] 428 428  inr r'' ⇒ 429 429 let 〈addr1, addr2〉 ≝ r'' in 430 set_arg_16 s (get_arg_16s addr2) addr1430 set_arg_16 ? s (get_arg_16 ? s addr2) addr1 431 431 ] 432 432  inr r ⇒ 433 433 let 〈addr1, addr2〉 ≝ r in 434 set_arg_1 s addr1 (get_arg_1s addr2 false)434 set_arg_1 ? s addr1 (get_arg_1 ? s addr2 false) 435 435 ] 436 436  inr r ⇒ 437 437 let 〈addr1, addr2〉 ≝ r in 438 set_arg_1 s addr1 (get_arg_1s addr2 false)438 set_arg_1 ? s addr1 (get_arg_1 ? s addr2 false) 439 439 ] 440 440  JC addr ⇒ 441 441 let r ≝ addr_of addr in 442 if get_cy_flag s then443 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in444 set_program_counter s new_pc442 if get_cy_flag ? s then 443 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in 444 set_program_counter ? s new_pc 445 445 else 446 446 s 447 447  JNC addr ⇒ 448 448 let r ≝ addr_of addr in 449 if ¬(get_cy_flag s) then450 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in451 set_program_counter s new_pc449 if ¬(get_cy_flag ? s) then 450 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in 451 set_program_counter ? s new_pc 452 452 else 453 453 s 454 454  JB addr1 addr2 ⇒ 455 455 let r ≝ addr_of addr2 in 456 if get_arg_1 s addr1 false then457 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in458 set_program_counter s new_pc456 if get_arg_1 ? s addr1 false then 457 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in 458 set_program_counter ? s new_pc 459 459 else 460 460 s 461 461  JNB addr1 addr2 ⇒ 462 462 let r ≝ addr_of addr2 in 463 if ¬(get_arg_1 s addr1 false) then464 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in465 set_program_counter s new_pc463 if ¬(get_arg_1 ? s addr1 false) then 464 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in 465 set_program_counter ? s new_pc 466 466 else 467 467 s 468 468  JBC addr1 addr2 ⇒ 469 469 let r ≝ addr_of addr2 in 470 let s ≝ set_arg_1 s addr1 false in471 if get_arg_1 s addr1 false then472 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in473 set_program_counter s new_pc470 let s ≝ set_arg_1 ? s addr1 false in 471 if get_arg_1 ? s addr1 false then 472 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in 473 set_program_counter ? s new_pc 474 474 else 475 475 s 476 476  JZ addr ⇒ 477 477 let r ≝ addr_of addr in 478 if eq_bv ? (get_8051_sfr s SFR_ACC_A) (zero 8) then479 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in480 set_program_counter s new_pc478 if eq_bv ? (get_8051_sfr ? s SFR_ACC_A) (zero 8) then 479 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in 480 set_program_counter ? s new_pc 481 481 else 482 482 s 483 483  JNZ addr ⇒ 484 484 let r ≝ addr_of addr in 485 if ¬(eq_bv ? (get_8051_sfr s SFR_ACC_A) (zero 8)) then486 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in487 set_program_counter s new_pc485 if ¬(eq_bv ? (get_8051_sfr ? s SFR_ACC_A) (zero 8)) then 486 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in 487 set_program_counter ? s new_pc 488 488 else 489 489 s … … 493 493 [ inl l ⇒ 494 494 let 〈addr1, addr2〉 ≝ l in 495 let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 s false addr1))496 (nat_of_bitvector ? (get_arg_8 s false addr2)) in497 if ¬(eq_bv ? (get_arg_8 s false addr1) (get_arg_8s false addr2)) then498 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in499 let s ≝ set_program_counter s new_pc in500 set_flags s new_cy (None ?) (get_ov_flags)495 let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 ? s false addr1)) 496 (nat_of_bitvector ? (get_arg_8 ? s false addr2)) in 497 if ¬(eq_bv ? (get_arg_8 ? s false addr1) (get_arg_8 ? s false addr2)) then 498 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in 499 let s ≝ set_program_counter ? s new_pc in 500 set_flags ? s new_cy (None ?) (get_ov_flag ? s) 501 501 else 502 (set_flags s new_cy (None ?) (get_ov_flags))502 (set_flags ? s new_cy (None ?) (get_ov_flag ? s)) 503 503  inr r' ⇒ 504 504 let 〈addr1, addr2〉 ≝ r' in 505 let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 s false addr1))506 (nat_of_bitvector ? (get_arg_8 s false addr2)) in507 if ¬(eq_bv ? (get_arg_8 s false addr1) (get_arg_8s false addr2)) then508 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in509 let s ≝ set_program_counter s new_pc in510 set_flags s new_cy (None ?) (get_ov_flags)505 let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 ? s false addr1)) 506 (nat_of_bitvector ? (get_arg_8 ? s false addr2)) in 507 if ¬(eq_bv ? (get_arg_8 ? s false addr1) (get_arg_8 ? s false addr2)) then 508 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in 509 let s ≝ set_program_counter ? s new_pc in 510 set_flags ? s new_cy (None ?) (get_ov_flag ? s) 511 511 else 512 (set_flags s new_cy (None ?) (get_ov_flags))512 (set_flags ? s new_cy (None ?) (get_ov_flag ? s)) 513 513 ] 514 514  DJNZ addr1 addr2 ⇒ 515 515 let r ≝ addr_of addr2 in 516 let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 s true addr1) (bitvector_of_nat 8 1) false in517 let s ≝ set_arg_8 s addr1 result in516 let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 ? s true addr1) (bitvector_of_nat 8 1) false in 517 let s ≝ set_arg_8 ? s addr1 result in 518 518 if ¬(eq_bv ? result (zero 8)) then 519 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in520 set_program_counter s new_pc519 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in 520 set_program_counter ? s new_pc 521 521 else 522 522 s … … 541 541 definition execute_1: Status → Status ≝ 542 542 λs: Status. 543 let 〈instr_pc, ticks〉 ≝ fetch (code_memory s) (program_counters) in543 let 〈instr_pc, ticks〉 ≝ fetch (code_memory ? s) (program_counter ? s) in 544 544 let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in 545 let s ≝ set_clock s (clocks + ticks) in546 let s ≝ set_program_counter s pc in545 let s ≝ set_clock ? s (clock ? s + ticks) in 546 let s ≝ set_program_counter ? s pc in 547 547 let s ≝ 548 548 match instr with 549 [ RealInstruction instr ⇒ execute_1_preinstruction [[ relative ]] 549 [ RealInstruction instr ⇒ execute_1_preinstruction [[ relative ]] ? 550 550 (λx. 551 551 match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → ? with … … 556 556 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with 557 557 [ ADDR11 a ⇒ λaddr11: True. 558 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in559 let s ≝ set_8051_sfr s SFR_SP new_sp in560 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in561 let s ≝ write_at_stack_pointer s pc_bl in562 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in563 let s ≝ set_8051_sfr s SFR_SP new_sp in564 let s ≝ write_at_stack_pointer s pc_bu in558 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in 559 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 560 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in 561 let s ≝ write_at_stack_pointer ? s pc_bl in 562 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in 563 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 564 let s ≝ write_at_stack_pointer ? s pc_bu in 565 565 let 〈thr, eig〉 ≝ split ? 3 8 a in 566 566 let 〈fiv, thr'〉 ≝ split ? 5 3 pc_bu in 567 567 let new_addr ≝ (fiv @@ thr) @@ pc_bl in 568 set_program_counter s new_addr568 set_program_counter ? s new_addr 569 569  _ ⇒ λother: False. ⊥ 570 570 ] (subaddressing_modein … addr) … … 572 572 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with 573 573 [ ADDR16 a ⇒ λaddr16: True. 574 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in575 let s ≝ set_8051_sfr s SFR_SP new_sp in576 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in577 let s ≝ write_at_stack_pointer s pc_bl in578 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in579 let s ≝ set_8051_sfr s SFR_SP new_sp in580 let s ≝ write_at_stack_pointer s pc_bu in581 set_program_counter s a574 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in 575 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 576 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in 577 let s ≝ write_at_stack_pointer ? s pc_bl in 578 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in 579 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 580 let s ≝ write_at_stack_pointer ? s pc_bu in 581 set_program_counter ? s a 582 582  _ ⇒ λother: False. ⊥ 583 583 ] (subaddressing_modein … addr) … … 585 585 match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → ? with 586 586 [ ACC_DPTR ⇒ λacc_dptr: True. 587 let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in588 let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfrs SFR_DPL) in587 let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in 588 let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in 589 589 let 〈carry, new_addr〉 ≝ half_add ? dptr big_acc in 590 let result ≝ lookup ? ? new_addr (code_memory s) (zero ?) in591 set_8051_sfr s SFR_ACC_A result590 let result ≝ lookup ? ? new_addr (code_memory ? s) (zero ?) in 591 set_8051_sfr ? s SFR_ACC_A result 592 592  ACC_PC ⇒ λacc_pc: True. 593 let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in594 let 〈carry,inc_pc〉 ≝ half_add ? (program_counter s) (bitvector_of_nat 16 1) in593 let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in 594 let 〈carry,inc_pc〉 ≝ half_add ? (program_counter ? s) (bitvector_of_nat 16 1) in 595 595 (* DPM: Under specified: does the carry from PC incrementation affect the *) 596 596 (* addition of the PC with the DPTR? At the moment, no. *) 597 let s ≝ set_program_counter s inc_pc in597 let s ≝ set_program_counter ? s inc_pc in 598 598 let 〈carry, new_addr〉 ≝ half_add ? inc_pc big_acc in 599 let result ≝ lookup ? ? new_addr (code_memory s) (zero ?) in600 set_8051_sfr s SFR_ACC_A result599 let result ≝ lookup ? ? new_addr (code_memory ? s) (zero ?) in 600 set_8051_sfr ? s SFR_ACC_A result 601 601  _ ⇒ λother: False. ⊥ 602 602 ] (subaddressing_modein … addr2) 603 603  JMP _ ⇒ (* DPM: always indirect_dptr *) 604 let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfrs SFR_DPL) in605 let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in604 let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in 605 let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in 606 606 let 〈carry, jmp_addr〉 ≝ half_add ? big_acc dptr in 607 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) jmp_addr in608 set_program_counter s new_pc607 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) jmp_addr in 608 set_program_counter ? s new_pc 609 609  LJMP addr ⇒ 610 610 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with 611 611 [ ADDR16 a ⇒ λaddr16: True. 612 set_program_counter s a612 set_program_counter ? s a 613 613  _ ⇒ λother: False. ⊥ 614 614 ] (subaddressing_modein … addr) … … 616 616 match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with 617 617 [ RELATIVE r ⇒ λrelative: True. 618 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in619 set_program_counter s new_pc618 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in 619 set_program_counter ? s new_pc 620 620  _ ⇒ λother: False. ⊥ 621 621 ] (subaddressing_modein … addr) … … 623 623 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with 624 624 [ ADDR11 a ⇒ λaddr11: True. 625 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in625 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in 626 626 let 〈nu, nl〉 ≝ split ? 4 4 pc_bu in 627 627 let bit ≝ get_index' ? O ? nl in 628 628 let 〈relevant1, relevant2〉 ≝ split ? 3 8 a in 629 629 let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in 630 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) new_addr in631 set_program_counter s new_pc630 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) new_addr in 631 set_program_counter ? s new_pc 632 632  _ ⇒ λother: False. ⊥ 633 633 ] (subaddressing_modein … addr) … … 652 652 653 653 axiom fetch_pseudo_instruction: 654 ∀p : list labelled_instruction.654 ∀ps: PseudoStatus. 655 655 ∀pc: Word. 656 656 (pseudo_instruction × Word) × nat. … … 659 659 axiom address_of_word_labels: Identifier → Word. 660 660 661 definition execute_1_pseudo_instruction: pseudo_assembly_program → Status → Status ≝ 662 λp. 661 definition execute_1_pseudo_instruction: PseudoStatus → PseudoStatus ≝ 663 662 λs. 664 let 〈instr_pc, ticks〉 ≝ fetch_pseudo_instruction (\snd p) (program_counters) in663 let 〈instr_pc, ticks〉 ≝ fetch_pseudo_instruction s (program_counter ? s) in 665 664 let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in 666 let s ≝ set_clock s (clocks + ticks) in667 let s ≝ set_program_counter s pc in665 let s ≝ set_clock ? s (clock ? s + ticks) in 666 let s ≝ set_program_counter ? s pc in 668 667 let s ≝ 669 668 match instr with 670 [ Instruction instr ⇒ execute_1_preinstruction ?address_of_labels instr s669 [ Instruction instr ⇒ execute_1_preinstruction … address_of_labels instr s 671 670  Comment cmt ⇒ s 672 671  Cost cst ⇒ s 673  Jmp jmp ⇒ set_program_counter s (address_of_word_labels jmp)672  Jmp jmp ⇒ set_program_counter ? s (address_of_word_labels jmp) 674 673  Call call ⇒ 675 674 let a ≝ address_of_word_labels call in 676 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in677 let s ≝ set_8051_sfr s SFR_SP new_sp in678 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in679 let s ≝ write_at_stack_pointer s pc_bl in680 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in681 let s ≝ set_8051_sfr s SFR_SP new_sp in682 let s ≝ write_at_stack_pointer s pc_bu in683 set_program_counter s a684  Mov dptr ident ⇒ set_arg_16 s (get_arg_16s (DATA16 (address_of_word_labels ident))) dptr675 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in 676 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 677 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in 678 let s ≝ write_at_stack_pointer ? s pc_bl in 679 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in 680 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 681 let s ≝ write_at_stack_pointer ? s pc_bu in 682 set_program_counter ? s a 683  Mov dptr ident ⇒ set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels ident))) dptr 685 684 ] 686 685 in … … 696 695 ]. 697 696 698 let rec execute_pseudo_instruction (n: nat) ( p: pseudo_assembly_program) (s: Status) on n:Status ≝697 let rec execute_pseudo_instruction (n: nat) (s: PseudoStatus) on n: PseudoStatus ≝ 699 698 match n with 700 699 [ O ⇒ s 701  S o ⇒ execute_pseudo_instruction o p (execute_1_pseudo_instruction ps)700  S o ⇒ execute_pseudo_instruction o (execute_1_pseudo_instruction s) 702 701 ]. 
src/ASM/Status.ma
r757 r821 85 85 (* Processor status. *) 86 86 (* ===================================== *) 87 record Status: Type[0] ≝87 record PreStatus (M: Type[0]): Type[0] ≝ 88 88 { 89 code_memory: BitVectorTrie Byte 16;89 code_memory: M; 90 90 low_internal_ram: BitVectorTrie Byte 7; 91 91 high_internal_ram: BitVectorTrie Byte 7; … … 103 103 }. 104 104 105 definition Status ≝ PreStatus (BitVectorTrie Byte 16). 106 definition PseudoStatus ≝ PreStatus (list labelled_instruction). 107 105 108 lemma sfr8051_index_19: 106 109 ∀i: SFR8051. … … 124 127 125 128 definition set_clock ≝ 126 λs: Status. 129 λM: Type[0]. 130 λs: PreStatus M. 127 131 λt: Time. 128 let old_code_memory ≝ code_memory s in129 let old_low_internal_ram ≝ low_internal_ram s in130 let old_high_internal_ram ≝ high_internal_ram s in131 let old_external_ram ≝ external_ram s in132 let old_program_counter ≝ program_counter s in133 let old_special_function_registers_8051 ≝ special_function_registers_8051 s in134 let old_special_function_registers_8052 ≝ special_function_registers_8052 s in135 let old_p1_latch ≝ p1_latch s in136 let old_p3_latch ≝ p3_latch s in137 mk_ Statusold_code_memory132 let old_code_memory ≝ code_memory ? s in 133 let old_low_internal_ram ≝ low_internal_ram ? s in 134 let old_high_internal_ram ≝ high_internal_ram ? s in 135 let old_external_ram ≝ external_ram ? s in 136 let old_program_counter ≝ program_counter ? s in 137 let old_special_function_registers_8051 ≝ special_function_registers_8051 ? s in 138 let old_special_function_registers_8052 ≝ special_function_registers_8052 ? s in 139 let old_p1_latch ≝ p1_latch ? s in 140 let old_p3_latch ≝ p3_latch ? s in 141 mk_PreStatus M old_code_memory 138 142 old_low_internal_ram 139 143 old_high_internal_ram … … 147 151 148 152 definition set_p1_latch ≝ 149 λs: Status. 153 λM: Type[0]. 154 λs: PreStatus M. 150 155 λb: Byte. 151 let old_code_memory ≝ code_memory s in152 let old_low_internal_ram ≝ low_internal_ram s in153 let old_high_internal_ram ≝ high_internal_ram s in154 let old_external_ram ≝ external_ram s in155 let old_program_counter ≝ program_counter s in156 let old_special_function_registers_8051 ≝ special_function_registers_8051 s in157 let old_special_function_registers_8052 ≝ special_function_registers_8052 s in158 let old_p3_latch ≝ p3_latch s in159 let old_clock ≝ clock s in160 mk_ Statusold_code_memory156 let old_code_memory ≝ code_memory ? s in 157 let old_low_internal_ram ≝ low_internal_ram ? s in 158 let old_high_internal_ram ≝ high_internal_ram ? s in 159 let old_external_ram ≝ external_ram ? s in 160 let old_program_counter ≝ program_counter ? s in 161 let old_special_function_registers_8051 ≝ special_function_registers_8051 ? s in 162 let old_special_function_registers_8052 ≝ special_function_registers_8052 ? s in 163 let old_p3_latch ≝ p3_latch ? s in 164 let old_clock ≝ clock ? s in 165 mk_PreStatus M old_code_memory 161 166 old_low_internal_ram 162 167 old_high_internal_ram … … 170 175 171 176 definition set_p3_latch ≝ 172 λs: Status. 177 λM: Type[0]. 178 λs: PreStatus M. 173 179 λb: Byte. 174 let old_code_memory ≝ code_memory s in175 let old_low_internal_ram ≝ low_internal_ram s in176 let old_high_internal_ram ≝ high_internal_ram s in177 let old_external_ram ≝ external_ram s in178 let old_program_counter ≝ program_counter s in179 let old_special_function_registers_8051 ≝ special_function_registers_8051 s in180 let old_special_function_registers_8052 ≝ special_function_registers_8052 s in181 let old_p1_latch ≝ p1_latch s in182 let old_clock ≝ clock s in183 mk_ Statusold_code_memory180 let old_code_memory ≝ code_memory ? s in 181 let old_low_internal_ram ≝ low_internal_ram ? s in 182 let old_high_internal_ram ≝ high_internal_ram ? s in 183 let old_external_ram ≝ external_ram ? s in 184 let old_program_counter ≝ program_counter ? s in 185 let old_special_function_registers_8051 ≝ special_function_registers_8051 ? s in 186 let old_special_function_registers_8052 ≝ special_function_registers_8052 ? s in 187 let old_p1_latch ≝ p1_latch ? s in 188 let old_clock ≝ clock ? s in 189 mk_PreStatus M old_code_memory 184 190 old_low_internal_ram 185 191 old_high_internal_ram … … 193 199 194 200 definition get_8051_sfr ≝ 195 λs: Status. 201 λM: Type[0]. 202 λs: PreStatus M. 196 203 λi: SFR8051. 197 let sfr ≝ special_function_registers_8051 s in204 let sfr ≝ special_function_registers_8051 ? s in 198 205 let index ≝ sfr_8051_index i in 199 206 get_index_v … sfr index ?. … … 202 209 203 210 definition get_8052_sfr ≝ 204 λs: Status. 211 λM: Type[0]. 212 λs: PreStatus M. 205 213 λi: SFR8052. 206 let sfr ≝ special_function_registers_8052 s in214 let sfr ≝ special_function_registers_8052 ? s in 207 215 let index ≝ sfr_8052_index i in 208 216 get_index_v … sfr index ?. … … 211 219 212 220 definition set_8051_sfr ≝ 213 λs: Status. 221 λM: Type[0]. 222 λs: PreStatus M. 214 223 λi: SFR8051. 215 224 λb: Byte. 216 225 let index ≝ sfr_8051_index i in 217 let old_code_memory ≝ code_memory s in218 let old_low_internal_ram ≝ low_internal_ram s in219 let old_high_internal_ram ≝ high_internal_ram s in220 let old_external_ram ≝ external_ram s in221 let old_program_counter ≝ program_counter s in222 let old_special_function_registers_8051 ≝ special_function_registers_8051 s in223 let old_special_function_registers_8052 ≝ special_function_registers_8052 s in226 let old_code_memory ≝ code_memory ? s in 227 let old_low_internal_ram ≝ low_internal_ram ? s in 228 let old_high_internal_ram ≝ high_internal_ram ? s in 229 let old_external_ram ≝ external_ram ? s in 230 let old_program_counter ≝ program_counter ? s in 231 let old_special_function_registers_8051 ≝ special_function_registers_8051 ? s in 232 let old_special_function_registers_8052 ≝ special_function_registers_8052 ? s in 224 233 let new_special_function_registers_8051 ≝ 225 234 set_index Byte 19 old_special_function_registers_8051 index b ? in 226 let old_p1_latch ≝ p1_latch s in227 let old_p3_latch ≝ p3_latch s in228 let old_clock ≝ clock s in229 mk_ Statusold_code_memory235 let old_p1_latch ≝ p1_latch ? s in 236 let old_p3_latch ≝ p3_latch ? s in 237 let old_clock ≝ clock ? s in 238 mk_PreStatus M old_code_memory 230 239 old_low_internal_ram 231 240 old_high_internal_ram … … 241 250 242 251 definition set_8052_sfr ≝ 243 λs: Status. 252 λM: Type[0]. 253 λs: PreStatus M. 244 254 λi: SFR8052. 245 255 λb: Byte. 246 256 let index ≝ sfr_8052_index i in 247 let old_code_memory ≝ code_memory s in248 let old_low_internal_ram ≝ low_internal_ram s in249 let old_high_internal_ram ≝ high_internal_ram s in250 let old_external_ram ≝ external_ram s in251 let old_program_counter ≝ program_counter s in252 let old_special_function_registers_8051 ≝ special_function_registers_8051 s in253 let old_special_function_registers_8052 ≝ special_function_registers_8052 s in257 let old_code_memory ≝ code_memory ? s in 258 let old_low_internal_ram ≝ low_internal_ram ? s in 259 let old_high_internal_ram ≝ high_internal_ram ? s in 260 let old_external_ram ≝ external_ram ? s in 261 let old_program_counter ≝ program_counter ? s in 262 let old_special_function_registers_8051 ≝ special_function_registers_8051 ? s in 263 let old_special_function_registers_8052 ≝ special_function_registers_8052 ? s in 254 264 let new_special_function_registers_8052 ≝ 255 265 set_index Byte 5 old_special_function_registers_8052 index b ? in 256 let old_p1_latch ≝ p1_latch s in257 let old_p3_latch ≝ p3_latch s in258 let old_clock ≝ clock s in259 mk_ Statusold_code_memory266 let old_p1_latch ≝ p1_latch ? s in 267 let old_p3_latch ≝ p3_latch ? s in 268 let old_clock ≝ clock ? s in 269 mk_PreStatus M old_code_memory 260 270 old_low_internal_ram 261 271 old_high_internal_ram … … 271 281 272 282 definition set_program_counter ≝ 273 λs: Status. 283 λM: Type[0]. 284 λs: PreStatus M. 274 285 λw: Word. 275 let old_code_memory ≝ code_memory s in276 let old_low_internal_ram ≝ low_internal_ram s in277 let old_high_internal_ram ≝ high_internal_ram s in278 let old_external_ram ≝ external_ram s in279 let old_special_function_registers_8051 ≝ special_function_registers_8051 s in280 let old_special_function_registers_8052 ≝ special_function_registers_8052 s in281 let old_p1_latch ≝ p1_latch s in282 let old_p3_latch ≝ p3_latch s in283 let old_clock ≝ clock s in284 mk_ Statusold_code_memory286 let old_code_memory ≝ code_memory ? s in 287 let old_low_internal_ram ≝ low_internal_ram ? s in 288 let old_high_internal_ram ≝ high_internal_ram ? s in 289 let old_external_ram ≝ external_ram ? s in 290 let old_special_function_registers_8051 ≝ special_function_registers_8051 ? s in 291 let old_special_function_registers_8052 ≝ special_function_registers_8052 ? s in 292 let old_p1_latch ≝ p1_latch ? s in 293 let old_p3_latch ≝ p3_latch ? s in 294 let old_clock ≝ clock ? s in 295 mk_PreStatus M old_code_memory 285 296 old_low_internal_ram 286 297 old_high_internal_ram … … 294 305 295 306 definition set_code_memory ≝ 296 λs: Status. 297 λr: BitVectorTrie Byte 16. 298 let old_low_internal_ram ≝ low_internal_ram s in 299 let old_high_internal_ram ≝ high_internal_ram s in 300 let old_external_ram ≝ external_ram s in 301 let old_program_counter ≝ program_counter s in 302 let old_special_function_registers_8051 ≝ special_function_registers_8051 s in 303 let old_special_function_registers_8052 ≝ special_function_registers_8052 s in 304 let old_p1_latch ≝ p1_latch s in 305 let old_p3_latch ≝ p3_latch s in 306 let old_clock ≝ clock s in 307 mk_Status r 307 λM: Type[0]. 308 λs: PreStatus M. 309 λr: M. 310 let old_low_internal_ram ≝ low_internal_ram ? s in 311 let old_high_internal_ram ≝ high_internal_ram ? s in 312 let old_external_ram ≝ external_ram ? s in 313 let old_program_counter ≝ program_counter ? s in 314 let old_special_function_registers_8051 ≝ special_function_registers_8051 ? s in 315 let old_special_function_registers_8052 ≝ special_function_registers_8052 ? s in 316 let old_p1_latch ≝ p1_latch ? s in 317 let old_p3_latch ≝ p3_latch ? s in 318 let old_clock ≝ clock ? s in 319 mk_PreStatus M r 308 320 old_low_internal_ram 309 321 old_high_internal_ram … … 317 329 318 330 definition set_low_internal_ram ≝ 319 λs: Status. 331 λM: Type[0]. 332 λs: PreStatus M. 320 333 λr: BitVectorTrie Byte 7. 321 let old_code_memory ≝ code_memory s in322 let old_high_internal_ram ≝ high_internal_ram s in323 let old_external_ram ≝ external_ram s in324 let old_program_counter ≝ program_counter s in325 let old_special_function_registers_8051 ≝ special_function_registers_8051 s in326 let old_special_function_registers_8052 ≝ special_function_registers_8052 s in327 let old_p1_latch ≝ p1_latch s in328 let old_p3_latch ≝ p3_latch s in329 let old_clock ≝ clock s in330 mk_ Statusold_code_memory334 let old_code_memory ≝ code_memory ? s in 335 let old_high_internal_ram ≝ high_internal_ram ? s in 336 let old_external_ram ≝ external_ram ? s in 337 let old_program_counter ≝ program_counter ? s in 338 let old_special_function_registers_8051 ≝ special_function_registers_8051 ? s in 339 let old_special_function_registers_8052 ≝ special_function_registers_8052 ? s in 340 let old_p1_latch ≝ p1_latch ? s in 341 let old_p3_latch ≝ p3_latch ? s in 342 let old_clock ≝ clock ? s in 343 mk_PreStatus M old_code_memory 331 344 r 332 345 old_high_internal_ram … … 340 353 341 354 definition set_high_internal_ram ≝ 342 λs: Status. 355 λM: Type[0]. 356 λs: PreStatus M. 343 357 λr: BitVectorTrie Byte 7. 344 let old_code_memory ≝ code_memory s in345 let old_low_internal_ram ≝ low_internal_ram s in346 let old_high_internal_ram ≝ high_internal_ram s in347 let old_external_ram ≝ external_ram s in348 let old_program_counter ≝ program_counter s in349 let old_special_function_registers_8051 ≝ special_function_registers_8051 s in350 let old_special_function_registers_8052 ≝ special_function_registers_8052 s in351 let old_p1_latch ≝ p1_latch s in352 let old_p3_latch ≝ p3_latch s in353 let old_clock ≝ clock s in354 mk_ Statusold_code_memory358 let old_code_memory ≝ code_memory ? s in 359 let old_low_internal_ram ≝ low_internal_ram ? s in 360 let old_high_internal_ram ≝ high_internal_ram ? s in 361 let old_external_ram ≝ external_ram ? s in 362 let old_program_counter ≝ program_counter ? s in 363 let old_special_function_registers_8051 ≝ special_function_registers_8051 ? s in 364 let old_special_function_registers_8052 ≝ special_function_registers_8052 ? s in 365 let old_p1_latch ≝ p1_latch ? s in 366 let old_p3_latch ≝ p3_latch ? s in 367 let old_clock ≝ clock ? s in 368 mk_PreStatus M old_code_memory 355 369 old_low_internal_ram 356 370 r … … 364 378 365 379 definition set_external_ram ≝ 366 λs: Status. 380 λM: Type[0]. 381 λs: PreStatus M. 367 382 λr: BitVectorTrie Byte 16. 368 let old_code_memory ≝ code_memory s in369 let old_low_internal_ram ≝ low_internal_ram s in370 let old_high_internal_ram ≝ high_internal_ram s in371 let old_program_counter ≝ program_counter s in372 let old_special_function_registers_8051 ≝ special_function_registers_8051 s in373 let old_special_function_registers_8052 ≝ special_function_registers_8052 s in374 let old_p1_latch ≝ p1_latch s in375 let old_p3_latch ≝ p3_latch s in376 let old_clock ≝ clock s in377 mk_ Statusold_code_memory383 let old_code_memory ≝ code_memory ? s in 384 let old_low_internal_ram ≝ low_internal_ram ? s in 385 let old_high_internal_ram ≝ high_internal_ram ? s in 386 let old_program_counter ≝ program_counter ? s in 387 let old_special_function_registers_8051 ≝ special_function_registers_8051 ? s in 388 let old_special_function_registers_8052 ≝ special_function_registers_8052 ? s in 389 let old_p1_latch ≝ p1_latch ? s in 390 let old_p3_latch ≝ p3_latch ? s in 391 let old_clock ≝ clock ? s in 392 mk_PreStatus M old_code_memory 378 393 old_low_internal_ram 379 394 old_high_internal_ram … … 387 402 388 403 definition get_cy_flag ≝ 389 λs: Status. 390 let sfr ≝ special_function_registers_8051 s in 404 λM: Type[0]. 405 λs: PreStatus M. 406 let sfr ≝ special_function_registers_8051 ? s in 391 407 let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in 392 408 get_index_v bool 8 psw O ?. … … 400 416 401 417 definition get_ac_flag ≝ 402 λs: Status. 403 let sfr ≝ special_function_registers_8051 s in 418 λM: Type[0]. 419 λs: PreStatus M. 420 let sfr ≝ special_function_registers_8051 ? s in 404 421 let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in 405 422 get_index_v bool 8 psw (S O) ?. … … 410 427 411 428 definition get_fo_flag ≝ 412 λs: Status. 413 let sfr ≝ special_function_registers_8051 s in 429 λM: Type[0]. 430 λs: PreStatus M. 431 let sfr ≝ special_function_registers_8051 ? s in 414 432 let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in 415 433 get_index_v bool 8 psw 2 ?. … … 420 438 421 439 definition get_rs1_flag ≝ 422 λs: Status. 423 let sfr ≝ special_function_registers_8051 s in 440 λM: Type[0]. 441 λs: PreStatus M. 442 let sfr ≝ special_function_registers_8051 ? s in 424 443 let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in 425 444 get_index_v bool 8 psw 3 ?. … … 430 449 431 450 definition get_rs0_flag ≝ 432 λs: Status. 433 let sfr ≝ special_function_registers_8051 s in 451 λM: Type[0]. 452 λs: PreStatus M. 453 let sfr ≝ special_function_registers_8051 ? s in 434 454 let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in 435 455 get_index_v bool 8 psw 4 ?. … … 440 460 441 461 definition get_ov_flag ≝ 442 λs: Status. 443 let sfr ≝ special_function_registers_8051 s in 462 λM: Type[0]. 463 λs: PreStatus M. 464 let sfr ≝ special_function_registers_8051 ? s in 444 465 let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in 445 466 get_index_v bool 8 psw 5 ?. … … 450 471 451 472 definition get_ud_flag ≝ 452 λs: Status. 453 let sfr ≝ special_function_registers_8051 s in 473 λM: Type[0]. 474 λs: PreStatus M. 475 let sfr ≝ special_function_registers_8051 ? s in 454 476 let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in 455 477 get_index_v bool 8 psw 6 ?. … … 460 482 461 483 definition get_p_flag ≝ 462 λs: Status. 463 let sfr ≝ special_function_registers_8051 s in 484 λM: Type[0]. 485 λs: PreStatus M. 486 let sfr ≝ special_function_registers_8051 ? s in 464 487 let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in 465 488 get_index_v bool 8 psw 7 ?. … … 470 493 471 494 definition set_flags ≝ 472 λs: Status. 495 λM: Type[0]. 496 λs: PreStatus M. 473 497 λcy: Bit. 474 498 λac: option Bit. 475 499 λov: Bit. 476 let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr s SFR_PSW) in500 let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr ? s SFR_PSW) in 477 501 let old_cy ≝ get_index_v… nu O ? in 478 502 let old_ac ≝ get_index_v… nu 1 ? in … … 486 510 let new_psw ≝ [[ old_cy ; new_ac ; old_fo ; old_rs1 ; 487 511 old_rs0 ; old_ov ; old_ud ; old_p ]] in 488 set_8051_sfr s SFR_PSW new_psw.512 set_8051_sfr ? s SFR_PSW new_psw. 489 513 [1,2,3,4,5,6,7,8: 490 514 normalize … … 495 519 496 520 definition initialise_status ≝ 497 let status ≝ mk_Status (Stub Byte 16) (* Code mem. *) 521 λM: Type[0]. 522 λcode_mem: M. 523 let status ≝ mk_PreStatus M code_mem (* Code mem. *) 498 524 (Stub Byte 7) (* Low mem. *) 499 525 (Stub Byte 7) (* High mem. *) … … 506 532 O (* Clock. *) 507 533 in 508 set_8051_sfr status SFR_SP (bitvector_of_nat 8 7).534 set_8051_sfr ? status SFR_SP (bitvector_of_nat 8 7). 509 535 510 536 axiom not_implemented: False. 511 537 512 538 definition get_bit_addressable_sfr ≝ 513 λs: Status. 539 λM: Type[0]. 540 λs: PreStatus M. 514 541 λn: nat. 515 542 λb: BitVector n. … … 520 547 else if (eqb address 144) then 521 548 if l then 522 (p1_latch s)549 (p1_latch ? s) 523 550 else 524 (get_8051_sfr s SFR_P1)551 (get_8051_sfr ? s SFR_P1) 525 552 else if (eqb address 160) then 526 553 ? 527 554 else if (eqb address 176) then 528 555 if l then 529 (p3_latch s)556 (p3_latch ? s) 530 557 else 531 (get_8051_sfr s SFR_P3)558 (get_8051_sfr ? s SFR_P3) 532 559 else if (eqb address 153) then 533 get_8051_sfr s SFR_SBUF560 get_8051_sfr ? s SFR_SBUF 534 561 else if (eqb address 138) then 535 get_8051_sfr s SFR_TL0562 get_8051_sfr ? s SFR_TL0 536 563 else if (eqb address 139) then 537 get_8051_sfr s SFR_TL1564 get_8051_sfr ? s SFR_TL1 538 565 else if (eqb address 140) then 539 get_8051_sfr s SFR_TH0566 get_8051_sfr ? s SFR_TH0 540 567 else if (eqb address 141) then 541 get_8051_sfr s SFR_TH1568 get_8051_sfr ? s SFR_TH1 542 569 else if (eqb address 200) then 543 get_8052_sfr s SFR_T2CON570 get_8052_sfr ? s SFR_T2CON 544 571 else if (eqb address 202) then 545 get_8052_sfr s SFR_RCAP2L572 get_8052_sfr ? s SFR_RCAP2L 546 573 else if (eqb address 203) then 547 get_8052_sfr s SFR_RCAP2H574 get_8052_sfr ? s SFR_RCAP2H 548 575 else if (eqb address 204) then 549 get_8052_sfr s SFR_TL2576 get_8052_sfr ? s SFR_TL2 550 577 else if (eqb address 205) then 551 get_8052_sfr s SFR_TH2578 get_8052_sfr ? s SFR_TH2 552 579 else if (eqb address 135) then 553 get_8051_sfr s SFR_PCON580 get_8051_sfr ? s SFR_PCON 554 581 else if (eqb address 136) then 555 get_8051_sfr s SFR_TCON582 get_8051_sfr ? s SFR_TCON 556 583 else if (eqb address 137) then 557 get_8051_sfr s SFR_TMOD584 get_8051_sfr ? s SFR_TMOD 558 585 else if (eqb address 152) then 559 get_8051_sfr s SFR_SCON586 get_8051_sfr ? s SFR_SCON 560 587 else if (eqb address 168) then 561 get_8051_sfr s SFR_IE588 get_8051_sfr ? s SFR_IE 562 589 else if (eqb address 184) then 563 get_8051_sfr s SFR_IP590 get_8051_sfr ? s SFR_IP 564 591 else if (eqb address 129) then 565 get_8051_sfr s SFR_SP592 get_8051_sfr ? s SFR_SP 566 593 else if (eqb address 130) then 567 get_8051_sfr s SFR_DPL594 get_8051_sfr ? s SFR_DPL 568 595 else if (eqb address 131) then 569 get_8051_sfr s SFR_DPH596 get_8051_sfr ? s SFR_DPH 570 597 else if (eqb address 208) then 571 get_8051_sfr s SFR_PSW598 get_8051_sfr ? s SFR_PSW 572 599 else if (eqb address 224) then 573 get_8051_sfr s SFR_ACC_A600 get_8051_sfr ? s SFR_ACC_A 574 601 else if (eqb address 240) then 575 get_8051_sfr s SFR_ACC_B602 get_8051_sfr ? s SFR_ACC_B 576 603 else 577 604 ?. … … 580 607 581 608 definition set_bit_addressable_sfr ≝ 582 λs: Status. 609 λM: Type[0]. 610 λs: PreStatus M. 583 611 λb: Byte. 584 612 λv: Byte. … … 587 615 ? 588 616 else if (eqb address 144) then 589 let status_1 ≝ set_8051_sfr s SFR_P1 v in590 let status_2 ≝ set_p1_latch s v in617 let status_1 ≝ set_8051_sfr ? s SFR_P1 v in 618 let status_2 ≝ set_p1_latch ? s v in 591 619 status_2 592 620 else if (eqb address 160) then 593 621 ? 594 622 else if (eqb address 176) then 595 let status_1 ≝ set_8051_sfr s SFR_P3 v in596 let status_2 ≝ set_p3_latch s v in623 let status_1 ≝ set_8051_sfr ? s SFR_P3 v in 624 let status_2 ≝ set_p3_latch ? s v in 597 625 status_2 598 626 else if (eqb address 153) then 599 set_8051_sfr s SFR_SBUF v627 set_8051_sfr ? s SFR_SBUF v 600 628 else if (eqb address 138) then 601 set_8051_sfr s SFR_TL0 v629 set_8051_sfr ? s SFR_TL0 v 602 630 else if (eqb address 139) then 603 set_8051_sfr s SFR_TL1 v631 set_8051_sfr ? s SFR_TL1 v 604 632 else if (eqb address 140) then 605 set_8051_sfr s SFR_TH0 v633 set_8051_sfr ? s SFR_TH0 v 606 634 else if (eqb address 141) then 607 set_8051_sfr s SFR_TH1 v635 set_8051_sfr ? s SFR_TH1 v 608 636 else if (eqb address 200) then 609 set_8052_sfr s SFR_T2CON v637 set_8052_sfr ? s SFR_T2CON v 610 638 else if (eqb address 202) then 611 set_8052_sfr s SFR_RCAP2L v639 set_8052_sfr ? s SFR_RCAP2L v 612 640 else if (eqb address 203) then 613 set_8052_sfr s SFR_RCAP2H v641 set_8052_sfr ? s SFR_RCAP2H v 614 642 else if (eqb address 204) then 615 set_8052_sfr s SFR_TL2 v643 set_8052_sfr ? s SFR_TL2 v 616 644 else if (eqb address 205) then 617 set_8052_sfr s SFR_TH2 v645 set_8052_sfr ? s SFR_TH2 v 618 646 else if (eqb address 135) then 619 set_8051_sfr s SFR_PCON v647 set_8051_sfr ? s SFR_PCON v 620 648 else if (eqb address 136) then 621 set_8051_sfr s SFR_TCON v649 set_8051_sfr ? s SFR_TCON v 622 650 else if (eqb address 137) then 623 set_8051_sfr s SFR_TMOD v651 set_8051_sfr ? s SFR_TMOD v 624 652 else if (eqb address 152) then 625 set_8051_sfr s SFR_SCON v653 set_8051_sfr ? s SFR_SCON v 626 654 else if (eqb address 168) then 627 set_8051_sfr s SFR_IE v655 set_8051_sfr ? s SFR_IE v 628 656 else if (eqb address 184) then 629 set_8051_sfr s SFR_IP v657 set_8051_sfr ? s SFR_IP v 630 658 else if (eqb address 129) then 631 set_8051_sfr s SFR_SP v659 set_8051_sfr ? s SFR_SP v 632 660 else if (eqb address 130) then 633 set_8051_sfr s SFR_DPL v661 set_8051_sfr ? s SFR_DPL v 634 662 else if (eqb address 131) then 635 set_8051_sfr s SFR_DPH v663 set_8051_sfr ? s SFR_DPH v 636 664 else if (eqb address 208) then 637 set_8051_sfr s SFR_PSW v665 set_8051_sfr ? s SFR_PSW v 638 666 else if (eqb address 224) then 639 set_8051_sfr s SFR_ACC_A v667 set_8051_sfr ? s SFR_ACC_A v 640 668 else if (eqb address 240) then 641 set_8051_sfr s SFR_ACC_B v669 set_8051_sfr ? s SFR_ACC_B v 642 670 else 643 671 ?. … … 646 674 647 675 definition bit_address_of_register ≝ 648 λs: Status. 676 λM: Type[0]. 677 λs: PreStatus M. 649 678 λr: BitVector 3. 650 679 let b ≝ get_index_v … r O ? in 651 680 let c ≝ get_index_v … r 1 ? in 652 681 let d ≝ get_index_v … r 2 ? in 653 let 〈 un, ln 〉 ≝ split ? 4 4 (get_8051_sfr s SFR_PSW) in682 let 〈 un, ln 〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_PSW) in 654 683 let 〈 r1, r0 〉 ≝ 〈 get_index_v … 4 un 2 ?, get_index_v … 4 un 3 ? 〉 in 655 684 let offset ≝ … … 672 701 673 702 definition get_register ≝ 674 λs: Status. 703 λM: Type[0]. 704 λs: PreStatus M. 675 705 λr: BitVector 3. 676 let address ≝ bit_address_of_register s r in677 lookup … address (low_internal_ram s) (zero 8).706 let address ≝ bit_address_of_register ? s r in 707 lookup … address (low_internal_ram ? s) (zero 8). 678 708 679 709 definition set_register ≝ 680 λs: Status. 710 λM: Type[0]. 711 λs: PreStatus M. 681 712 λr: BitVector 3. 682 713 λv: Byte. 683 let address ≝ bit_address_of_register s r in684 let old_low_internal_ram ≝ low_internal_ram s in714 let address ≝ bit_address_of_register ? s r in 715 let old_low_internal_ram ≝ low_internal_ram ? s in 685 716 let new_low_internal_ram ≝ insert … address v old_low_internal_ram in 686 set_low_internal_ram s new_low_internal_ram.717 set_low_internal_ram ? s new_low_internal_ram. 687 718 688 719 definition read_at_stack_pointer ≝ 689 λs: Status. 690 let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr s SFR_SP) in 720 λM: Type[0]. 721 λs: PreStatus M. 722 let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr ? s SFR_SP) in 691 723 let m ≝ get_index_v … nu O ? in 692 724 let r1 ≝ get_index_v … nu 1 ? in … … 696 728 let memory ≝ 697 729 if m then 698 (low_internal_ram s)730 (low_internal_ram ? s) 699 731 else 700 (high_internal_ram s)732 (high_internal_ram ? s) 701 733 in 702 734 lookup … address memory (zero 8). … … 709 741 710 742 definition write_at_stack_pointer ≝ 711 λs: Status. 743 λM: Type[0]. 744 λs: PreStatus M. 712 745 λv: Byte. 713 let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr s SFR_SP) in746 let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr ? s SFR_SP) in 714 747 let bit_zero ≝ get_index_v… nu O ? in 715 748 let bit_1 ≝ get_index_v… nu 1 ? in … … 718 751 if bit_zero then 719 752 let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl) 720 v (low_internal_ram s) in721 set_low_internal_ram s memory753 v (low_internal_ram ? s) in 754 set_low_internal_ram ? s memory 722 755 else 723 756 let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl) 724 v (high_internal_ram s) in725 set_high_internal_ram s memory.757 v (high_internal_ram ? s) in 758 set_high_internal_ram ? s memory. 726 759 [1,2,3,4: 727 760 normalize … … 731 764 qed. 732 765 733 definition set_arg_16: Status → Word → [[ dptr ]] → Status ≝ 734 λs,v,a. 766 definition set_arg_16: ∀M: Type[0]. PreStatus M → Word → [[ dptr ]] → PreStatus M ≝ 767 λM. 768 λs. 769 λv. 770 λa. 735 771 match a return λx. bool_to_Prop (is_in ? [[ dptr ]] x) → ? with 736 772 [ DPTR ⇒ λ_:True. 737 773 let 〈 bu, bl 〉 ≝ split … 8 8 v in 738 let status ≝ set_8051_sfr s SFR_DPH bu in739 let status ≝ set_8051_sfr status SFR_DPL bl in774 let status ≝ set_8051_sfr ? s SFR_DPH bu in 775 let status ≝ set_8051_sfr ? status SFR_DPL bl in 740 776 status 741 777  _ ⇒ λK. … … 745 781 ] (subaddressing_modein … a). 746 782 747 definition get_arg_16: Status→ [[ data16 ]] → Word ≝748 λ s, a.783 definition get_arg_16: ∀M: Type[0]. PreStatus M → [[ data16 ]] → Word ≝ 784 λm, s, a. 749 785 match a return λx. bool_to_Prop (is_in ? [[ data16 ]] x) → ? with 750 786 [ DATA16 d ⇒ λ_:True. d … … 755 791 ] (subaddressing_modein … a). 756 792 757 definition get_arg_8: Status→ bool → [[ direct ; indirect ; registr ;793 definition get_arg_8: ∀M: Type[0]. PreStatus M → bool → [[ direct ; indirect ; registr ; 758 794 acc_a ; acc_b ; data ; acc_dptr ; 759 795 acc_pc ; ext_indirect ; 760 796 ext_indirect_dptr ]] → Byte ≝ 761 λ s, l, a.797 λm, s, l, a. 762 798 match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ; 763 799 acc_a ; acc_b ; data ; acc_dptr ; 764 800 acc_pc ; ext_indirect ; 765 801 ext_indirect_dptr ]] x) → ? with 766 [ ACC_A ⇒ λacc_a: True. get_8051_sfr s SFR_ACC_A767  ACC_B ⇒ λacc_b: True. get_8051_sfr s SFR_ACC_B802 [ ACC_A ⇒ λacc_a: True. get_8051_sfr ? s SFR_ACC_A 803  ACC_B ⇒ λacc_b: True. get_8051_sfr ? s SFR_ACC_B 768 804  DATA d ⇒ λdata: True. d 769  REGISTER r ⇒ λregister: True. get_register s r805  REGISTER r ⇒ λregister: True. get_register ? s r 770 806  EXT_INDIRECT_DPTR ⇒ 771 807 λext_indirect_dptr: True. 772 let address ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfrs SFR_DPL) in773 lookup … 16 address (external_ram s) (zero 8)808 let address ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in 809 lookup … 16 address (external_ram ? s) (zero 8) 774 810  EXT_INDIRECT e ⇒ 775 811 λext_indirect: True. 776 let address ≝ get_register s [[ false; false; e ]] in812 let address ≝ get_register ? s [[ false; false; e ]] in 777 813 let padded_address ≝ pad 8 8 address in 778 lookup … 16 padded_address (external_ram s) (zero 8)814 lookup … 16 padded_address (external_ram ? s) (zero 8) 779 815  ACC_DPTR ⇒ 780 816 λacc_dptr: True. 781 let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfrs SFR_DPL) in782 let padded_acc ≝ pad 8 8 (get_8051_sfr s SFR_ACC_A) in817 let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in 818 let padded_acc ≝ pad 8 8 (get_8051_sfr ? s SFR_ACC_A) in 783 819 let 〈 carry, address 〉 ≝ half_add 16 dptr padded_acc in 784 lookup … 16 address (external_ram s) (zero 8)820 lookup … 16 address (external_ram ? s) (zero 8) 785 821  ACC_PC ⇒ 786 822 λacc_pc: True. 787 let padded_acc ≝ pad 8 8 (get_8051_sfr s SFR_ACC_A) in788 let 〈 carry, address 〉 ≝ half_add 16 (program_counter s) padded_acc in789 lookup … 16 address (external_ram s) (zero 8)823 let padded_acc ≝ pad 8 8 (get_8051_sfr ? s SFR_ACC_A) in 824 let 〈 carry, address 〉 ≝ half_add 16 (program_counter ? s) padded_acc in 825 lookup … 16 address (external_ram ? s) (zero 8) 790 826  DIRECT d ⇒ 791 827 λdirect: True. … … 796 832 let 〈 bit_one, three_bits 〉 ≝ split ? 1 3 nu in 797 833 let address ≝ three_bits @@ nl in 798 lookup ? 7 address (low_internal_ram s) (zero 8)799  false ⇒ get_bit_addressable_sfr s 8 d l834 lookup ? 7 address (low_internal_ram ? s) (zero 8) 835  false ⇒ get_bit_addressable_sfr ? s 8 d l 800 836 ] 801 837  INDIRECT i ⇒ 802 838 λindirect: True. 803 let 〈 nu, nl 〉 ≝ split ? 4 4 (get_register s [[ false; false; i]]) in839 let 〈 nu, nl 〉 ≝ split ? 4 4 (get_register ? s [[ false; false; i]]) in 804 840 let 〈 bit_one_v, three_bits 〉 ≝ split ? 1 3 nu in 805 841 let bit_1 ≝ get_index_v … bit_one_v O ? in 806 842 match bit_1 with 807 843 [ true ⇒ 808 lookup ? 7 (three_bits @@ nl) (low_internal_ram s) (zero 8)844 lookup ? 7 (three_bits @@ nl) (low_internal_ram ? s) (zero 8) 809 845  false ⇒ 810 lookup ? 7 (three_bits @@ nl) (high_internal_ram s) (zero 8)846 lookup ? 7 (three_bits @@ nl) (high_internal_ram ? s) (zero 8) 811 847 ] 812 848  _ ⇒ λother. … … 820 856 qed. 821 857 822 definition set_arg_8: Status→ [[ direct ; indirect ; registr ;858 definition set_arg_8: ∀M: Type[0]. PreStatus M → [[ direct ; indirect ; registr ; 823 859 acc_a ; acc_b ; ext_indirect ; 824 ext_indirect_dptr ]] → Byte → Status≝825 λ s, a, v.860 ext_indirect_dptr ]] → Byte → PreStatus M ≝ 861 λm, s, a, v. 826 862 match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ; 827 863 acc_a ; acc_b ; ext_indirect ; … … 833 869 let 〈 ignore, three_bits 〉 ≝ split ? 1 3 nu in 834 870 match bit_1 with 835 [ true ⇒ set_bit_addressable_sfr s d v871 [ true ⇒ set_bit_addressable_sfr ? s d v 836 872  false ⇒ 837 let memory ≝ insert ? 7 (three_bits @@ nl) v (low_internal_ram s) in838 set_low_internal_ram s memory873 let memory ≝ insert ? 7 (three_bits @@ nl) v (low_internal_ram ? s) in 874 set_low_internal_ram ? s memory 839 875 ] 840 876  INDIRECT i ⇒ 841 877 λindirect: True. 842 let register ≝ get_register s [[ false; false; i ]] in878 let register ≝ get_register ? s [[ false; false; i ]] in 843 879 let 〈nu, nl〉 ≝ split ? 4 4 register in 844 880 let bit_1 ≝ get_index_v … nu 1 ? in … … 846 882 match bit_1 with 847 883 [ true ⇒ 848 let memory ≝ insert … (three_bits @@ nl) v (low_internal_ram s) in849 set_low_internal_ram s memory884 let memory ≝ insert … (three_bits @@ nl) v (low_internal_ram ? s) in 885 set_low_internal_ram ? s memory 850 886  false ⇒ 851 let memory ≝ insert … (three_bits @@ nl) v (high_internal_ram s) in852 set_high_internal_ram s memory887 let memory ≝ insert … (three_bits @@ nl) v (high_internal_ram ? s) in 888 set_high_internal_ram ? s memory 853 889 ] 854  REGISTER r ⇒ λregister: True. set_register s r v855  ACC_A ⇒ λacc_a: True. set_8051_sfr s SFR_ACC_A v856  ACC_B ⇒ λacc_b: True. set_8051_sfr s SFR_ACC_B v890  REGISTER r ⇒ λregister: True. set_register ? s r v 891  ACC_A ⇒ λacc_a: True. set_8051_sfr ? s SFR_ACC_A v 892  ACC_B ⇒ λacc_b: True. set_8051_sfr ? s SFR_ACC_B v 857 893  EXT_INDIRECT e ⇒ 858 894 λext_indirect: True. 859 let address ≝ get_register s [[ false; false; e ]] in895 let address ≝ get_register ? s [[ false; false; e ]] in 860 896 let padded_address ≝ pad 8 8 address in 861 let memory ≝ insert ? 16 padded_address v (external_ram s) in862 set_external_ram s memory897 let memory ≝ insert ? 16 padded_address v (external_ram ? s) in 898 set_external_ram ? s memory 863 899  EXT_INDIRECT_DPTR ⇒ 864 900 λext_indirect_dptr: True. 865 let address ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfrs SFR_DPL) in866 let memory ≝ insert ? 16 address v (external_ram s) in867 set_external_ram s memory901 let address ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in 902 let memory ≝ insert ? 16 address v (external_ram ? s) in 903 set_external_ram ? s memory 868 904  _ ⇒ 869 905 λother: False. … … 928 964 qed. 929 965 930 definition get_arg_1: Status→ [[ bit_addr ; n_bit_addr ; carry ]] →966 definition get_arg_1: ∀M: Type[0]. PreStatus M → [[ bit_addr ; n_bit_addr ; carry ]] → 931 967 bool → bool ≝ 932 λ s, a, l.968 λm, s, a, l. 933 969 match a return λx. bool_to_Prop (is_in ? [[ bit_addr ; 934 970 n_bit_addr ; … … 945 981 let m ≝ address mod 8 in 946 982 let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in 947 let sfr ≝ get_bit_addressable_sfr s ? trans l in983 let sfr ≝ get_bit_addressable_sfr ? s ? trans l in 948 984 get_index_v … sfr m ? 949 985  false ⇒ 950 986 let address ≝ nat_of_bitvector … (three_bits @@ nl) in 951 987 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in 952 let t ≝ lookup … 7 address' (low_internal_ram s) (zero 8) in988 let t ≝ lookup … 7 address' (low_internal_ram ? s) (zero 8) in 953 989 get_index_v … t (modulus address 8) ? 954 990 ] … … 964 1000 let m ≝ address mod 8 in 965 1001 let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in 966 let sfr ≝ get_bit_addressable_sfr s ? trans l in1002 let sfr ≝ get_bit_addressable_sfr ? s ? trans l in 967 1003 ¬(get_index_v … sfr m ?) 968 1004  false ⇒ 969 1005 let address ≝ nat_of_bitvector … (three_bits @@ nl) in 970 1006 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in 971 let trans ≝ lookup … 7 address' (low_internal_ram s) (zero 8) in1007 let trans ≝ lookup … 7 address' (low_internal_ram ? s) (zero 8) in 972 1008 ¬(get_index_v … trans (modulus address 8) ?) 973 1009 ] 974  CARRY ⇒ λcarry: True. get_cy_flag s1010  CARRY ⇒ λcarry: True. get_cy_flag ? s 975 1011  _ ⇒ λother. 976 1012 match other in False with [ ] … … 985 1021 qed. 986 1022 987 definition set_arg_1: Status→ [[ bit_addr ; carry ]] →988 Bit → Status≝989 λ s, a, v.1023 definition set_arg_1: ∀M: Type[0]. PreStatus M → [[ bit_addr ; carry ]] → 1024 Bit → PreStatus M ≝ 1025 λm, s, a, v. 990 1026 match a return λx. bool_to_Prop (is_in ? [[ bit_addr ; carry ]] x) → ? with 991 1027 [ BIT_ADDR b ⇒ λbit_addr: True. 992 let 〈 nu, nl 〉 ≝ split ? 4 4 (get_8051_sfr s SFR_PSW) in1028 let 〈 nu, nl 〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_PSW) in 993 1029 let bit_1 ≝ get_index_v … nu 1 ? in 994 1030 let 〈 ignore, three_bits 〉 ≝ split ? 1 3 nu in … … 999 1035 let m ≝ address mod 8 in 1000 1036 let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in 1001 let sfr ≝ get_bit_addressable_sfr s ? t true in1037 let sfr ≝ get_bit_addressable_sfr ? s ? t true in 1002 1038 let new_sfr ≝ set_index … sfr m v ? in 1003 set_bit_addressable_sfr s new_sfr t1039 set_bit_addressable_sfr ? s new_sfr t 1004 1040  false ⇒ 1005 1041 let address ≝ nat_of_bitvector … (three_bits @@ nl) in 1006 1042 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in 1007 let t ≝ lookup … 7 address' (low_internal_ram s) (zero 8) in1043 let t ≝ lookup … 7 address' (low_internal_ram ? s) (zero 8) in 1008 1044 let n_bit ≝ set_index … t (modulus address 8) v ? in 1009 let memory ≝ insert ? 7 address' n_bit (low_internal_ram s) in1010 set_low_internal_ram s memory1045 let memory ≝ insert ? 7 address' n_bit (low_internal_ram ? s) in 1046 set_low_internal_ram ? s memory 1011 1047 ] 1012 1048  CARRY ⇒ 1013 1049 λcarry: True. 1014 let 〈 nu, nl 〉 ≝ split ? 4 4 (get_8051_sfr s SFR_PSW) in1050 let 〈 nu, nl 〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_PSW) in 1015 1051 let bit_1 ≝ get_index_v… nu 1 ? in 1016 1052 let bit_2 ≝ get_index_v… nu 2 ? in 1017 1053 let bit_3 ≝ get_index_v… nu 3 ? in 1018 1054 let new_psw ≝ [[ v; bit_1 ; bit_2; bit_3 ]] @@ nl in 1019 set_8051_sfr s SFR_PSW new_psw1055 set_8051_sfr ? s SFR_PSW new_psw 1020 1056  _ ⇒ 1021 1057 λother: False. … … 1038 1074 1039 1075 definition load ≝ 1040 λl, status. 1041 set_code_memory status (load_code_memory l). 1076 λl. 1077 λstatus. 1078 set_code_memory ? status (load_code_memory l).
Note: See TracChangeset
for help on using the changeset viewer.