Changeset 1666 for src/ASM/Status.ma
 Timestamp:
 Jan 28, 2012, 1:42:15 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Status.ma
r1600 r1666 86 86 (* Processor status. *) 87 87 (* ===================================== *) 88 record PreStatus (M: Type[0]) : Type[0] ≝88 record PreStatus (M: Type[0]) (code_memory: M) : Type[0] ≝ 89 89 { 90 code_memory: M;91 90 low_internal_ram: BitVectorTrie Byte 7; 92 91 high_internal_ram: BitVectorTrie Byte 7; … … 129 128 definition set_clock ≝ 130 129 λM: Type[0]. 131 λs: PreStatus M. 130 λcode_memory:M. 131 λs: PreStatus M code_memory. 132 132 λt: Time. 133 let old_code_memory ≝ code_memory ? s in 134 let old_low_internal_ram ≝ low_internal_ram ? s in 135 let old_high_internal_ram ≝ high_internal_ram ? s in 136 let old_external_ram ≝ external_ram ? s in 137 let old_program_counter ≝ program_counter ? s in 138 let old_special_function_registers_8051 ≝ special_function_registers_8051 ? s in 139 let old_special_function_registers_8052 ≝ special_function_registers_8052 ? s in 140 let old_p1_latch ≝ p1_latch ? s in 141 let old_p3_latch ≝ p3_latch ? s in 142 mk_PreStatus M old_code_memory 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 code_memory 143 142 old_low_internal_ram 144 143 old_high_internal_ram … … 153 152 definition set_p1_latch ≝ 154 153 λM: Type[0]. 155 λs: PreStatus M. 154 λcode_memory:M. 155 λs: PreStatus M code_memory. 156 156 λb: Byte. 157 let old_code_memory ≝ code_memory ? s in 158 let old_low_internal_ram ≝ low_internal_ram ? s in 159 let old_high_internal_ram ≝ high_internal_ram ? s in 160 let old_external_ram ≝ external_ram ? s in 161 let old_program_counter ≝ program_counter ? s in 162 let old_special_function_registers_8051 ≝ special_function_registers_8051 ? s in 163 let old_special_function_registers_8052 ≝ special_function_registers_8052 ? s in 164 let old_p3_latch ≝ p3_latch ? s in 165 let old_clock ≝ clock ? s in 166 mk_PreStatus M old_code_memory 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 code_memory 167 166 old_low_internal_ram 168 167 old_high_internal_ram … … 177 176 definition set_p3_latch ≝ 178 177 λM: Type[0]. 179 λs: PreStatus M. 178 λcode_memory:M. 179 λs: PreStatus M code_memory. 180 180 λb: Byte. 181 let old_code_memory ≝ code_memory ? s in 182 let old_low_internal_ram ≝ low_internal_ram ? s in 183 let old_high_internal_ram ≝ high_internal_ram ? s in 184 let old_external_ram ≝ external_ram ? s in 185 let old_program_counter ≝ program_counter ? s in 186 let old_special_function_registers_8051 ≝ special_function_registers_8051 ? s in 187 let old_special_function_registers_8052 ≝ special_function_registers_8052 ? s in 188 let old_p1_latch ≝ p1_latch ? s in 189 let old_clock ≝ clock ? s in 190 mk_PreStatus M old_code_memory 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 code_memory 191 190 old_low_internal_ram 192 191 old_high_internal_ram … … 201 200 definition get_8051_sfr ≝ 202 201 λM: Type[0]. 203 λs: PreStatus M. 202 λcode_memory:M. 203 λs: PreStatus M code_memory. 204 204 λi: SFR8051. 205 let sfr ≝ special_function_registers_8051 ? s in205 let sfr ≝ special_function_registers_8051 ?? s in 206 206 let index ≝ sfr_8051_index i in 207 207 get_index_v … sfr index ?. … … 211 211 definition get_8052_sfr ≝ 212 212 λM: Type[0]. 213 λs: PreStatus M. 213 λcode_memory:M. 214 λs: PreStatus M code_memory. 214 215 λi: SFR8052. 215 let sfr ≝ special_function_registers_8052 ? s in216 let sfr ≝ special_function_registers_8052 ?? s in 216 217 let index ≝ sfr_8052_index i in 217 218 get_index_v … sfr index ?. … … 221 222 definition set_8051_sfr ≝ 222 223 λM: Type[0]. 223 λs: PreStatus M. 224 λcode_memory:M. 225 λs: PreStatus M code_memory. 224 226 λi: SFR8051. 225 227 λb: Byte. 226 228 let index ≝ sfr_8051_index i in 227 let old_code_memory ≝ code_memory ? s in 228 let old_low_internal_ram ≝ low_internal_ram ? s in 229 let old_high_internal_ram ≝ high_internal_ram ? s in 230 let old_external_ram ≝ external_ram ? s in 231 let old_program_counter ≝ program_counter ? s in 232 let old_special_function_registers_8051 ≝ special_function_registers_8051 ? s in 233 let old_special_function_registers_8052 ≝ special_function_registers_8052 ? s in 229 let old_low_internal_ram ≝ low_internal_ram ?? s in 230 let old_high_internal_ram ≝ high_internal_ram ?? s in 231 let old_external_ram ≝ external_ram ?? s in 232 let old_program_counter ≝ program_counter ?? s in 233 let old_special_function_registers_8051 ≝ special_function_registers_8051 ?? s in 234 let old_special_function_registers_8052 ≝ special_function_registers_8052 ?? s in 234 235 let new_special_function_registers_8051 ≝ 235 236 set_index Byte 19 old_special_function_registers_8051 index b ? in 236 let old_p1_latch ≝ p1_latch ? s in237 let old_p3_latch ≝ p3_latch ? s in238 let old_clock ≝ clock ? s in239 mk_PreStatus M old_code_memory237 let old_p1_latch ≝ p1_latch ?? s in 238 let old_p3_latch ≝ p3_latch ?? s in 239 let old_clock ≝ clock ?? s in 240 mk_PreStatus M code_memory 240 241 old_low_internal_ram 241 242 old_high_internal_ram … … 252 253 definition set_8052_sfr ≝ 253 254 λM: Type[0]. 254 λs: PreStatus M. 255 λcode_memory:M. 256 λs: PreStatus M code_memory. 255 257 λi: SFR8052. 256 258 λb: Byte. 257 259 let index ≝ sfr_8052_index i in 258 let old_code_memory ≝ code_memory ? s in 259 let old_low_internal_ram ≝ low_internal_ram ? s in 260 let old_high_internal_ram ≝ high_internal_ram ? s in 261 let old_external_ram ≝ external_ram ? s in 262 let old_program_counter ≝ program_counter ? s in 263 let old_special_function_registers_8051 ≝ special_function_registers_8051 ? s in 264 let old_special_function_registers_8052 ≝ special_function_registers_8052 ? s in 260 let old_low_internal_ram ≝ low_internal_ram ?? s in 261 let old_high_internal_ram ≝ high_internal_ram ?? s in 262 let old_external_ram ≝ external_ram ?? s in 263 let old_program_counter ≝ program_counter ?? s in 264 let old_special_function_registers_8051 ≝ special_function_registers_8051 ?? s in 265 let old_special_function_registers_8052 ≝ special_function_registers_8052 ?? s in 265 266 let new_special_function_registers_8052 ≝ 266 267 set_index Byte 5 old_special_function_registers_8052 index b ? in 267 let old_p1_latch ≝ p1_latch ? s in268 let old_p3_latch ≝ p3_latch ? s in269 let old_clock ≝ clock ? s in270 mk_PreStatus M old_code_memory268 let old_p1_latch ≝ p1_latch ?? s in 269 let old_p3_latch ≝ p3_latch ?? s in 270 let old_clock ≝ clock ?? s in 271 mk_PreStatus M code_memory 271 272 old_low_internal_ram 272 273 old_high_internal_ram … … 283 284 definition set_program_counter ≝ 284 285 λM: Type[0]. 285 λs: PreStatus M. 286 λcode_memory:M. 287 λs: PreStatus M code_memory. 286 288 λw: Word. 287 let old_code_memory ≝ code_memory ? s in 288 let old_low_internal_ram ≝ low_internal_ram ? s in 289 let old_high_internal_ram ≝ high_internal_ram ? s in 290 let old_external_ram ≝ external_ram ? s in 291 let old_special_function_registers_8051 ≝ special_function_registers_8051 ? s in 292 let old_special_function_registers_8052 ≝ special_function_registers_8052 ? s in 293 let old_p1_latch ≝ p1_latch ? s in 294 let old_p3_latch ≝ p3_latch ? s in 295 let old_clock ≝ clock ? s in 296 mk_PreStatus M old_code_memory 289 let old_low_internal_ram ≝ low_internal_ram ?? s in 290 let old_high_internal_ram ≝ high_internal_ram ?? s in 291 let old_external_ram ≝ external_ram ?? s in 292 let old_special_function_registers_8051 ≝ special_function_registers_8051 ?? s in 293 let old_special_function_registers_8052 ≝ special_function_registers_8052 ?? s in 294 let old_p1_latch ≝ p1_latch ?? s in 295 let old_p3_latch ≝ p3_latch ?? s in 296 let old_clock ≝ clock ?? s in 297 mk_PreStatus M code_memory 297 298 old_low_internal_ram 298 299 old_high_internal_ram … … 307 308 definition set_code_memory ≝ 308 309 λM,M': Type[0]. 309 λs: PreStatus M. 310 λcode_memory:M. 311 λs: PreStatus M code_memory. 310 312 λr: M'. 311 let old_low_internal_ram ≝ low_internal_ram ? s in312 let old_high_internal_ram ≝ high_internal_ram ? s in313 let old_external_ram ≝ external_ram ? s in314 let old_program_counter ≝ program_counter ? s in315 let old_special_function_registers_8051 ≝ special_function_registers_8051 ? s in316 let old_special_function_registers_8052 ≝ special_function_registers_8052 ? s in317 let old_p1_latch ≝ p1_latch ? s in318 let old_p3_latch ≝ p3_latch ? s in319 let old_clock ≝ clock ? s in313 let old_low_internal_ram ≝ low_internal_ram ?? s in 314 let old_high_internal_ram ≝ high_internal_ram ?? s in 315 let old_external_ram ≝ external_ram ?? s in 316 let old_program_counter ≝ program_counter ?? s in 317 let old_special_function_registers_8051 ≝ special_function_registers_8051 ?? s in 318 let old_special_function_registers_8052 ≝ special_function_registers_8052 ?? s in 319 let old_p1_latch ≝ p1_latch ?? s in 320 let old_p3_latch ≝ p3_latch ?? s in 321 let old_clock ≝ clock ?? s in 320 322 mk_PreStatus M' r 321 323 old_low_internal_ram … … 331 333 definition set_low_internal_ram ≝ 332 334 λM: Type[0]. 333 λs: PreStatus M. 335 λcode_memory:M. 336 λs: PreStatus M code_memory. 334 337 λr: BitVectorTrie Byte 7. 335 let old_code_memory ≝ code_memory ? s in 336 let old_high_internal_ram ≝ high_internal_ram ? s in 337 let old_external_ram ≝ external_ram ? s in 338 let old_program_counter ≝ program_counter ? s in 339 let old_special_function_registers_8051 ≝ special_function_registers_8051 ? s in 340 let old_special_function_registers_8052 ≝ special_function_registers_8052 ? s in 341 let old_p1_latch ≝ p1_latch ? s in 342 let old_p3_latch ≝ p3_latch ? s in 343 let old_clock ≝ clock ? s in 344 mk_PreStatus M old_code_memory 338 let old_high_internal_ram ≝ high_internal_ram ?? s in 339 let old_external_ram ≝ external_ram ?? s in 340 let old_program_counter ≝ program_counter ?? s in 341 let old_special_function_registers_8051 ≝ special_function_registers_8051 ?? s in 342 let old_special_function_registers_8052 ≝ special_function_registers_8052 ?? s in 343 let old_p1_latch ≝ p1_latch ?? s in 344 let old_p3_latch ≝ p3_latch ?? s in 345 let old_clock ≝ clock ?? s in 346 mk_PreStatus M code_memory 345 347 r 346 348 old_high_internal_ram … … 355 357 definition set_high_internal_ram ≝ 356 358 λM: Type[0]. 357 λs: PreStatus M. 359 λcode_memory:M. 360 λs: PreStatus M code_memory. 358 361 λr: BitVectorTrie Byte 7. 359 let old_code_memory ≝ code_memory ? s in 360 let old_low_internal_ram ≝ low_internal_ram ? s in 361 let old_high_internal_ram ≝ high_internal_ram ? s in 362 let old_external_ram ≝ external_ram ? s in 363 let old_program_counter ≝ program_counter ? s in 364 let old_special_function_registers_8051 ≝ special_function_registers_8051 ? s in 365 let old_special_function_registers_8052 ≝ special_function_registers_8052 ? s in 366 let old_p1_latch ≝ p1_latch ? s in 367 let old_p3_latch ≝ p3_latch ? s in 368 let old_clock ≝ clock ? s in 369 mk_PreStatus M old_code_memory 362 let old_low_internal_ram ≝ low_internal_ram ?? s in 363 let old_high_internal_ram ≝ high_internal_ram ?? s in 364 let old_external_ram ≝ external_ram ?? s in 365 let old_program_counter ≝ program_counter ?? s in 366 let old_special_function_registers_8051 ≝ special_function_registers_8051 ?? s in 367 let old_special_function_registers_8052 ≝ special_function_registers_8052 ?? s in 368 let old_p1_latch ≝ p1_latch ?? s in 369 let old_p3_latch ≝ p3_latch ?? s in 370 let old_clock ≝ clock ?? s in 371 mk_PreStatus M code_memory 370 372 old_low_internal_ram 371 373 r … … 380 382 definition set_external_ram ≝ 381 383 λM: Type[0]. 382 λs: PreStatus M. 384 λcode_memory:M. 385 λs: PreStatus M code_memory. 383 386 λr: BitVectorTrie Byte 16. 384 let old_code_memory ≝ code_memory ? s in 385 let old_low_internal_ram ≝ low_internal_ram ? s in 386 let old_high_internal_ram ≝ high_internal_ram ? s in 387 let old_program_counter ≝ program_counter ? s in 388 let old_special_function_registers_8051 ≝ special_function_registers_8051 ? s in 389 let old_special_function_registers_8052 ≝ special_function_registers_8052 ? s in 390 let old_p1_latch ≝ p1_latch ? s in 391 let old_p3_latch ≝ p3_latch ? s in 392 let old_clock ≝ clock ? s in 393 mk_PreStatus M old_code_memory 387 let old_low_internal_ram ≝ low_internal_ram ?? s in 388 let old_high_internal_ram ≝ high_internal_ram ?? s in 389 let old_program_counter ≝ program_counter ?? s in 390 let old_special_function_registers_8051 ≝ special_function_registers_8051 ?? s in 391 let old_special_function_registers_8052 ≝ special_function_registers_8052 ?? s in 392 let old_p1_latch ≝ p1_latch ?? s in 393 let old_p3_latch ≝ p3_latch ?? s in 394 let old_clock ≝ clock ?? s in 395 mk_PreStatus M code_memory 394 396 old_low_internal_ram 395 397 old_high_internal_ram … … 404 406 definition get_cy_flag ≝ 405 407 λM: Type[0]. 406 λs: PreStatus M. 407 let sfr ≝ special_function_registers_8051 ? s in 408 λcode_memory:M. 409 λs: PreStatus M code_memory. 410 let sfr ≝ special_function_registers_8051 ?? s in 408 411 let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in 409 412 get_index_v bool 8 psw O ?. … … 418 421 definition get_ac_flag ≝ 419 422 λM: Type[0]. 420 λs: PreStatus M. 421 let sfr ≝ special_function_registers_8051 ? s in 423 λcode_memory:M. 424 λs: PreStatus M code_memory. 425 let sfr ≝ special_function_registers_8051 ?? s in 422 426 let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in 423 427 get_index_v bool 8 psw 1 ?. … … 429 433 definition get_fo_flag ≝ 430 434 λM: Type[0]. 431 λs: PreStatus M. 432 let sfr ≝ special_function_registers_8051 ? s in 435 λcode_memory:M. 436 λs: PreStatus M code_memory. 437 let sfr ≝ special_function_registers_8051 ?? s in 433 438 let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in 434 439 get_index_v bool 8 psw 2 ?. … … 440 445 definition get_rs1_flag ≝ 441 446 λM: Type[0]. 442 λs: PreStatus M. 443 let sfr ≝ special_function_registers_8051 ? s in 447 λcode_memory:M. 448 λs: PreStatus M code_memory. 449 let sfr ≝ special_function_registers_8051 ?? s in 444 450 let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in 445 451 get_index_v bool 8 psw 3 ?. … … 451 457 definition get_rs0_flag ≝ 452 458 λM: Type[0]. 453 λs: PreStatus M. 454 let sfr ≝ special_function_registers_8051 ? s in 459 λcode_memory:M. 460 λs: PreStatus M code_memory. 461 let sfr ≝ special_function_registers_8051 ?? s in 455 462 let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in 456 463 get_index_v bool 8 psw 4 ?. … … 462 469 definition get_ov_flag ≝ 463 470 λM: Type[0]. 464 λs: PreStatus M. 465 let sfr ≝ special_function_registers_8051 ? s in 471 λcode_memory:M. 472 λs: PreStatus M code_memory. 473 let sfr ≝ special_function_registers_8051 ?? s in 466 474 let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in 467 475 get_index_v bool 8 psw 5 ?. … … 473 481 definition get_ud_flag ≝ 474 482 λM: Type[0]. 475 λs: PreStatus M. 476 let sfr ≝ special_function_registers_8051 ? s in 483 λcode_memory:M. 484 λs: PreStatus M code_memory. 485 let sfr ≝ special_function_registers_8051 ?? s in 477 486 let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in 478 487 get_index_v bool 8 psw 6 ?. … … 484 493 definition get_p_flag ≝ 485 494 λM: Type[0]. 486 λs: PreStatus M. 487 let sfr ≝ special_function_registers_8051 ? s in 495 λcode_memory:M. 496 λs: PreStatus M code_memory. 497 let sfr ≝ special_function_registers_8051 ?? s in 488 498 let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in 489 499 get_index_v bool 8 psw 7 ?. … … 495 505 definition set_flags ≝ 496 506 λM: Type[0]. 497 λs: PreStatus M. 507 λcode_memory:M. 508 λs: PreStatus M code_memory. 498 509 λcy: Bit. 499 510 λac: option Bit. 500 511 λov: Bit. 501 let old_cy ≝ get_index_v … (get_8051_sfr? s SFR_PSW) O ? in502 let old_ac ≝ get_index_v … (get_8051_sfr? s SFR_PSW) 1 ? in503 let old_fo ≝ get_index_v … (get_8051_sfr? s SFR_PSW) 2 ? in504 let old_rs1 ≝ get_index_v … (get_8051_sfr? s SFR_PSW) 3 ? in505 let old_rs0 ≝ get_index_v … (get_8051_sfr? s SFR_PSW) 4 ? in506 let old_ov ≝ get_index_v … (get_8051_sfr? s SFR_PSW) 5 ? in507 let old_ud ≝ get_index_v … (get_8051_sfr? s SFR_PSW) 6 ? in508 let old_p ≝ get_index_v … (get_8051_sfr? s SFR_PSW) 7 ? in512 let old_cy ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) O ? in 513 let old_ac ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) 1 ? in 514 let old_fo ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) 2 ? in 515 let old_rs1 ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) 3 ? in 516 let old_rs0 ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) 4 ? in 517 let old_ov ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) 5 ? in 518 let old_ud ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) 6 ? in 519 let old_p ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) 7 ? in 509 520 let new_ac ≝ match ac with [ None ⇒ old_ac  Some j ⇒ j ] in 510 let new_psw ≝ [[ old_cy ; new_ac ; old_fo ; old_rs1 ;511 old_rs0 ; old_ov ; old_ud ; old_p ]] in512 set_8051_sfr ? s SFR_PSW new_psw.521 set_8051_sfr ?? s SFR_PSW 522 [[ old_cy ; new_ac ; old_fo ; old_rs1 ; 523 old_rs0 ; old_ov ; old_ud ; old_p ]]. 513 524 [1,2,3,4,5,6,7,8: 514 525 normalize … … 532 543 O (* Clock. *) 533 544 in 534 set_8051_sfr ? status SFR_SP (bitvector_of_nat 8 7).545 set_8051_sfr ?? status SFR_SP (bitvector_of_nat 8 7). 535 546 536 547 definition get_bit_addressable_sfr ≝ 537 548 λM: Type[0]. 538 λs: PreStatus M. 549 λcode_memory:M. 550 λs: PreStatus M code_memory. 539 551 λn: nat. 540 552 λb: BitVector n. … … 545 557 else if (eqb address 144) then 546 558 if l then 547 (p1_latch ? s)559 (p1_latch ?? s) 548 560 else 549 (get_8051_sfr ? s SFR_P1)561 (get_8051_sfr ?? s SFR_P1) 550 562 else if (eqb address 160) then 551 563 ? 552 564 else if (eqb address 176) then 553 565 if l then 554 (p3_latch ? s)566 (p3_latch ?? s) 555 567 else 556 (get_8051_sfr ? s SFR_P3)568 (get_8051_sfr ?? s SFR_P3) 557 569 else if (eqb address 153) then 558 get_8051_sfr ? s SFR_SBUF570 get_8051_sfr ?? s SFR_SBUF 559 571 else if (eqb address 138) then 560 get_8051_sfr ? s SFR_TL0572 get_8051_sfr ?? s SFR_TL0 561 573 else if (eqb address 139) then 562 get_8051_sfr ? s SFR_TL1574 get_8051_sfr ?? s SFR_TL1 563 575 else if (eqb address 140) then 564 get_8051_sfr ? s SFR_TH0576 get_8051_sfr ?? s SFR_TH0 565 577 else if (eqb address 141) then 566 get_8051_sfr ? s SFR_TH1578 get_8051_sfr ?? s SFR_TH1 567 579 else if (eqb address 200) then 568 get_8052_sfr ? s SFR_T2CON580 get_8052_sfr ?? s SFR_T2CON 569 581 else if (eqb address 202) then 570 get_8052_sfr ? s SFR_RCAP2L582 get_8052_sfr ?? s SFR_RCAP2L 571 583 else if (eqb address 203) then 572 get_8052_sfr ? s SFR_RCAP2H584 get_8052_sfr ?? s SFR_RCAP2H 573 585 else if (eqb address 204) then 574 get_8052_sfr ? s SFR_TL2586 get_8052_sfr ?? s SFR_TL2 575 587 else if (eqb address 205) then 576 get_8052_sfr ? s SFR_TH2588 get_8052_sfr ?? s SFR_TH2 577 589 else if (eqb address 135) then 578 get_8051_sfr ? s SFR_PCON590 get_8051_sfr ?? s SFR_PCON 579 591 else if (eqb address 136) then 580 get_8051_sfr ? s SFR_TCON592 get_8051_sfr ?? s SFR_TCON 581 593 else if (eqb address 137) then 582 get_8051_sfr ? s SFR_TMOD594 get_8051_sfr ?? s SFR_TMOD 583 595 else if (eqb address 152) then 584 get_8051_sfr ? s SFR_SCON596 get_8051_sfr ?? s SFR_SCON 585 597 else if (eqb address 168) then 586 get_8051_sfr ? s SFR_IE598 get_8051_sfr ?? s SFR_IE 587 599 else if (eqb address 184) then 588 get_8051_sfr ? s SFR_IP600 get_8051_sfr ?? s SFR_IP 589 601 else if (eqb address 129) then 590 get_8051_sfr ? s SFR_SP602 get_8051_sfr ?? s SFR_SP 591 603 else if (eqb address 130) then 592 get_8051_sfr ? s SFR_DPL604 get_8051_sfr ?? s SFR_DPL 593 605 else if (eqb address 131) then 594 get_8051_sfr ? s SFR_DPH606 get_8051_sfr ?? s SFR_DPH 595 607 else if (eqb address 208) then 596 get_8051_sfr ? s SFR_PSW608 get_8051_sfr ?? s SFR_PSW 597 609 else if (eqb address 224) then 598 get_8051_sfr ? s SFR_ACC_A610 get_8051_sfr ?? s SFR_ACC_A 599 611 else if (eqb address 240) then 600 get_8051_sfr ? s SFR_ACC_B612 get_8051_sfr ?? s SFR_ACC_B 601 613 else 602 614 ?. … … 606 618 definition set_bit_addressable_sfr ≝ 607 619 λM: Type[0]. 608 λs: PreStatus M. 620 λcode_memory:M. 621 λs: PreStatus M code_memory. 609 622 λb: Byte. 610 623 λv: Byte. … … 613 626 ? 614 627 else if (eqb address 144) then 615 let status_1 ≝ set_8051_sfr ? s SFR_P1 v in616 let status_2 ≝ set_p1_latch ? s v in628 let status_1 ≝ set_8051_sfr ?? s SFR_P1 v in 629 let status_2 ≝ set_p1_latch ?? s v in 617 630 status_2 618 631 else if (eqb address 160) then 619 632 ? 620 633 else if (eqb address 176) then 621 let status_1 ≝ set_8051_sfr ? s SFR_P3 v in622 let status_2 ≝ set_p3_latch ? s v in634 let status_1 ≝ set_8051_sfr ?? s SFR_P3 v in 635 let status_2 ≝ set_p3_latch ?? s v in 623 636 status_2 624 637 else if (eqb address 153) then 625 set_8051_sfr ? s SFR_SBUF v638 set_8051_sfr ?? s SFR_SBUF v 626 639 else if (eqb address 138) then 627 set_8051_sfr ? s SFR_TL0 v640 set_8051_sfr ?? s SFR_TL0 v 628 641 else if (eqb address 139) then 629 set_8051_sfr ? s SFR_TL1 v642 set_8051_sfr ?? s SFR_TL1 v 630 643 else if (eqb address 140) then 631 set_8051_sfr ? s SFR_TH0 v644 set_8051_sfr ?? s SFR_TH0 v 632 645 else if (eqb address 141) then 633 set_8051_sfr ? s SFR_TH1 v646 set_8051_sfr ?? s SFR_TH1 v 634 647 else if (eqb address 200) then 635 set_8052_sfr ? s SFR_T2CON v648 set_8052_sfr ?? s SFR_T2CON v 636 649 else if (eqb address 202) then 637 set_8052_sfr ? s SFR_RCAP2L v650 set_8052_sfr ?? s SFR_RCAP2L v 638 651 else if (eqb address 203) then 639 set_8052_sfr ? s SFR_RCAP2H v652 set_8052_sfr ?? s SFR_RCAP2H v 640 653 else if (eqb address 204) then 641 set_8052_sfr ? s SFR_TL2 v654 set_8052_sfr ?? s SFR_TL2 v 642 655 else if (eqb address 205) then 643 set_8052_sfr ? s SFR_TH2 v656 set_8052_sfr ?? s SFR_TH2 v 644 657 else if (eqb address 135) then 645 set_8051_sfr ? s SFR_PCON v658 set_8051_sfr ?? s SFR_PCON v 646 659 else if (eqb address 136) then 647 set_8051_sfr ? s SFR_TCON v660 set_8051_sfr ?? s SFR_TCON v 648 661 else if (eqb address 137) then 649 set_8051_sfr ? s SFR_TMOD v662 set_8051_sfr ?? s SFR_TMOD v 650 663 else if (eqb address 152) then 651 set_8051_sfr ? s SFR_SCON v664 set_8051_sfr ?? s SFR_SCON v 652 665 else if (eqb address 168) then 653 set_8051_sfr ? s SFR_IE v666 set_8051_sfr ?? s SFR_IE v 654 667 else if (eqb address 184) then 655 set_8051_sfr ? s SFR_IP v668 set_8051_sfr ?? s SFR_IP v 656 669 else if (eqb address 129) then 657 set_8051_sfr ? s SFR_SP v670 set_8051_sfr ?? s SFR_SP v 658 671 else if (eqb address 130) then 659 set_8051_sfr ? s SFR_DPL v672 set_8051_sfr ?? s SFR_DPL v 660 673 else if (eqb address 131) then 661 set_8051_sfr ? s SFR_DPH v674 set_8051_sfr ?? s SFR_DPH v 662 675 else if (eqb address 208) then 663 set_8051_sfr ? s SFR_PSW v676 set_8051_sfr ?? s SFR_PSW v 664 677 else if (eqb address 224) then 665 set_8051_sfr ? s SFR_ACC_A v678 set_8051_sfr ?? s SFR_ACC_A v 666 679 else if (eqb address 240) then 667 set_8051_sfr ? s SFR_ACC_B v680 set_8051_sfr ?? s SFR_ACC_B v 668 681 else 669 682 ?. … … 673 686 definition bit_address_of_register ≝ 674 687 λM: Type[0]. 675 λs: PreStatus M. 688 λcode_memory:M. 689 λs: PreStatus M code_memory. 676 690 λr: BitVector 3. 677 691 let b ≝ get_index_v … r O ? in 678 692 let c ≝ get_index_v … r 1 ? in 679 693 let d ≝ get_index_v … r 2 ? in 680 let 〈 un, ln 〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_PSW) in694 let 〈 un, ln 〉 ≝ split ? 4 4 (get_8051_sfr ?? s SFR_PSW) in 681 695 let 〈 r1, r0 〉 ≝ 〈 get_index_v … 4 un 2 ?, get_index_v … 4 un 3 ? 〉 in 682 696 let offset ≝ … … 700 714 definition get_register ≝ 701 715 λM: Type[0]. 702 λs: PreStatus M. 716 λcode_memory:M. 717 λs: PreStatus M code_memory. 703 718 λr: BitVector 3. 704 let address ≝ bit_address_of_register ?s r in705 lookup ?? address (low_internal_ram ?s) (zero 8).719 let address ≝ bit_address_of_register … s r in 720 lookup ?? address (low_internal_ram … s) (zero 8). 706 721 707 722 definition set_register ≝ 708 723 λM: Type[0]. 709 λs: PreStatus M. 724 λcode_memory:M. 725 λs: PreStatus M code_memory. 710 726 λr: BitVector 3. 711 727 λv: Byte. 712 let address ≝ bit_address_of_register ?s r in713 let old_low_internal_ram ≝ low_internal_ram ? s in728 let address ≝ bit_address_of_register … s r in 729 let old_low_internal_ram ≝ low_internal_ram ?? s in 714 730 let new_low_internal_ram ≝ insert … address v old_low_internal_ram in 715 set_low_internal_ram ?s new_low_internal_ram.731 set_low_internal_ram … s new_low_internal_ram. 716 732 717 733 definition read_at_stack_pointer ≝ 718 734 λM: Type[0]. 719 λs: PreStatus M. 720 let 〈 nu, nl 〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_SP) in 721 let m ≝ get_index_v … nu O ? in 722 let r1 ≝ get_index_v … nu 1 ? in 723 let r2 ≝ get_index_v … nu 2 ? in 724 let r3 ≝ get_index_v … nu 3 ? in 735 λcode_memory:M. 736 λs: PreStatus M code_memory. 737 let 〈 nu, nl 〉 ≝ split ? 4 4 (get_8051_sfr ?? s SFR_SP) in 738 let m ≝ get_index_v ?? nu O ? in 739 let r1 ≝ get_index_v ?? nu 1 ? in 740 let r2 ≝ get_index_v ?? nu 2 ? in 741 let r3 ≝ get_index_v ?? nu 3 ? in 725 742 let address ≝ [[ r1 ; r2 ; r3 ]] @@ nl in 726 743 let memory ≝ 727 744 if m then 728 (low_internal_ram ? s)745 (low_internal_ram ?? s) 729 746 else 730 (high_internal_ram ? s)747 (high_internal_ram ?? s) 731 748 in 732 749 lookup … address memory (zero 8). … … 740 757 definition write_at_stack_pointer ≝ 741 758 λM: Type[0]. 742 λs: PreStatus M. 759 λcode_memory:M. 760 λs: PreStatus M code_memory. 743 761 λv: Byte. 744 let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr ? s SFR_SP) in745 let bit_zero ≝ get_index_v …nu O ? in746 let bit_1 ≝ get_index_v …nu 1 ? in747 let bit_2 ≝ get_index_v …nu 2 ? in748 let bit_3 ≝ get_index_v …nu 3 ? in762 let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr ?? s SFR_SP) in 763 let bit_zero ≝ get_index_v ?? nu O ? in 764 let bit_1 ≝ get_index_v ?? nu 1 ? in 765 let bit_2 ≝ get_index_v ?? nu 2 ? in 766 let bit_3 ≝ get_index_v ?? nu 3 ? in 749 767 if bit_zero then 750 768 let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl) 751 v (low_internal_ram ? s) in752 set_low_internal_ram ? s memory769 v (low_internal_ram ?? s) in 770 set_low_internal_ram ?? s memory 753 771 else 754 772 let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl) 755 v (high_internal_ram ? s) in756 set_high_internal_ram ? s memory.773 v (high_internal_ram ?? s) in 774 set_high_internal_ram ?? s memory. 757 775 [1,2,3,4: 758 776 normalize … … 762 780 qed. 763 781 764 definition set_arg_16': ∀M: Type[0]. ∀s:PreStatus M. Word → [[ dptr ]] → Σs':PreStatus M. clock … s = clock … s' ≝ 765 λM. 766 λs. 767 λv. 768 λa. 769 match a return λx. bool_to_Prop (is_in ? [[ dptr ]] x) → Σs'. clock M s = clock M s' with 782 definition set_arg_16': ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. Word → [[ dptr ]] → Σs':PreStatus M code_memory. clock ?? s = clock ?? s' ≝ 783 λM,code_memory,s,v,a. 784 match a return λx. bool_to_Prop (is_in ? [[ dptr ]] x) → Σs'. clock M ? s = clock M ? s' with 770 785 [ DPTR ⇒ λ_:True. 771 786 let 〈 bu, bl 〉 ≝ split … 8 8 v in 772 let status ≝ set_8051_sfr ?s SFR_DPH bu in773 let status ≝ set_8051_sfr ?status SFR_DPL bl in787 let status ≝ set_8051_sfr … s SFR_DPH bu in 788 let status ≝ set_8051_sfr … status SFR_DPL bl in 774 789 status 775 790  _ ⇒ λK. … … 781 796 qed. 782 797 783 definition set_arg_16: ∀M: Type[0]. ∀ s:PreStatus M. Word → [[ dptr ]] → PreStatus M≝798 definition set_arg_16: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. Word → [[ dptr ]] → PreStatus M code_memory ≝ 784 799 set_arg_16'. 785 800 786 lemma set_arg_16_ok: ∀M, s,v,x. clock M s = clock … (set_arg_16 Ms v x).787 #M # s #x #v whd in match set_arg_16; normalize nodelta @pi2801 lemma set_arg_16_ok: ∀M,cm,s,v,x. clock M cm s = clock M cm (set_arg_16 M cm s v x). 802 #M #cm #s #x #v whd in match set_arg_16; normalize nodelta @pi2 788 803 qed. 789 804 790 805 791 definition get_arg_16: ∀M: Type[0]. PreStatus M→ [[ data16 ]] → Word ≝792 λm, s, a.806 definition get_arg_16: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → [[ data16 ]] → Word ≝ 807 λm, cm, s, a. 793 808 match a return λx. bool_to_Prop (is_in ? [[ data16 ]] x) → ? with 794 809 [ DATA16 d ⇒ λ_:True. d … … 799 814 ] (subaddressing_modein … a). 800 815 801 definition get_arg_8: ∀M: Type[0]. PreStatus M→ bool → [[ direct ; indirect ; registr ;816 definition get_arg_8: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → bool → [[ direct ; indirect ; registr ; 802 817 acc_a ; acc_b ; data ; acc_dptr ; 803 818 acc_pc ; ext_indirect ; 804 819 ext_indirect_dptr ]] → Byte ≝ 805 λm, s, l, a.820 λm, cm, s, l, a. 806 821 match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ; 807 822 acc_a ; acc_b ; data ; acc_dptr ; 808 823 acc_pc ; ext_indirect ; 809 824 ext_indirect_dptr ]] x) → ? with 810 [ ACC_A ⇒ λacc_a: True. get_8051_sfr ? s SFR_ACC_A811  ACC_B ⇒ λacc_b: True. get_8051_sfr ? s SFR_ACC_B825 [ ACC_A ⇒ λacc_a: True. get_8051_sfr ?? s SFR_ACC_A 826  ACC_B ⇒ λacc_b: True. get_8051_sfr ?? s SFR_ACC_B 812 827  DATA d ⇒ λdata: True. d 813  REGISTER r ⇒ λregister: True. get_register ? s r828  REGISTER r ⇒ λregister: True. get_register ?? s r 814 829  EXT_INDIRECT_DPTR ⇒ 815 830 λext_indirect_dptr: True. 816 let address ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr? s SFR_DPL) in817 lookup ? 16 address (external_ram ? s) (zero 8)831 let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in 832 lookup ? 16 address (external_ram ?? s) (zero 8) 818 833  EXT_INDIRECT e ⇒ 819 834 λext_indirect: True. 820 let address ≝ get_register ? s [[ false; false; e ]] in835 let address ≝ get_register ?? s [[ false; false; e ]] in 821 836 let padded_address ≝ pad 8 8 address in 822 lookup ? 16 padded_address (external_ram ? s) (zero 8)837 lookup ? 16 padded_address (external_ram ?? s) (zero 8) 823 838  ACC_DPTR ⇒ 824 839 λacc_dptr: True. 825 let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr? s SFR_DPL) in826 let padded_acc ≝ pad 8 8 (get_8051_sfr ? s SFR_ACC_A) in840 let dptr ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in 841 let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in 827 842 let 〈 carry, address 〉 ≝ half_add 16 dptr padded_acc in 828 lookup ? 16 address (external_ram ? s) (zero 8)843 lookup ? 16 address (external_ram ?? s) (zero 8) 829 844  ACC_PC ⇒ 830 845 λacc_pc: True. 831 let padded_acc ≝ pad 8 8 (get_8051_sfr ? s SFR_ACC_A) in832 let 〈 carry, address 〉 ≝ half_add 16 (program_counter ? s) padded_acc in833 lookup ? 16 address (external_ram ? s) (zero 8)846 let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in 847 let 〈 carry, address 〉 ≝ half_add 16 (program_counter ?? s) padded_acc in 848 lookup ? 16 address (external_ram ?? s) (zero 8) 834 849  DIRECT d ⇒ 835 850 λdirect: True. … … 840 855 [ false ⇒ 841 856 let address ≝ three_bits @@ nl in 842 lookup ? 7 address (low_internal_ram ? s) (zero 8)843  true ⇒ get_bit_addressable_sfr ? s 8 d l857 lookup ? 7 address (low_internal_ram ?? s) (zero 8) 858  true ⇒ get_bit_addressable_sfr ?? s 8 d l 844 859 ] 845 860  INDIRECT i ⇒ 846 861 λindirect: True. 847 let 〈 nu, nl 〉 ≝ split ? 4 4 (get_register ? s [[ false; false; i]]) in862 let 〈 nu, nl 〉 ≝ split ? 4 4 (get_register ?? s [[ false; false; i]]) in 848 863 let 〈 bit_one_v, three_bits 〉 ≝ split ? 1 3 nu in 849 864 let bit_1 ≝ get_index_v ?? bit_one_v O ? in 850 865 match bit_1 with 851 866 [ false ⇒ 852 lookup ? 7 (three_bits @@ nl) (low_internal_ram ? s) (zero 8)867 lookup ? 7 (three_bits @@ nl) (low_internal_ram ?? s) (zero 8) 853 868  true ⇒ 854 lookup ? 7 (three_bits @@ nl) (high_internal_ram ? s) (zero 8)869 lookup ? 7 (three_bits @@ nl) (high_internal_ram ?? s) (zero 8) 855 870 ] 856 871  _ ⇒ λother. … … 864 879 qed. 865 880 866 axiom set_bit_addressable_sfr_ignores_clock: ∀m,s,d,v. clockm s = clock … (set_bit_addressable_sfr … s d v).867 868 definition set_arg_8': ∀M: Type[0]. ∀ s:PreStatus M. [[ direct ; indirect ; registr ;881 axiom clock_set_bit_addressable_sfr: ∀m,cm,s,d,v. clock m cm s = clock … (set_bit_addressable_sfr … s d v). 882 883 definition set_arg_8': ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. [[ direct ; indirect ; registr ; 869 884 acc_a ; acc_b ; ext_indirect ; 870 ext_indirect_dptr ]] → Byte → Σs':PreStatus M .871 clock … s = clock …s' ≝872 λm, s, a, v.885 ext_indirect_dptr ]] → Byte → Σs':PreStatus M code_memory. 886 clock … code_memory s = clock … code_memory s' ≝ 887 λm, cm, s, a, v. 873 888 match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ; 874 889 acc_a ; acc_b ; ext_indirect ; 875 890 ext_indirect_dptr ]] x) → 876 Σs':PreStatus m . ?(*clock … s*) = ?(*clock … s'*)891 Σs':PreStatus m cm. clock m cm s = clock m cm s' 877 892 (*CSC: bug here if one specified the two clock above*) 878 893 with … … 883 898 let 〈 ignore, three_bits 〉 ≝ split ? 1 3 nu in 884 899 match bit_one with 885 [ true ⇒ set_bit_addressable_sfr ? s d v900 [ true ⇒ set_bit_addressable_sfr ?? s d v 886 901  false ⇒ 887 let memory ≝ insert ? 7 (three_bits @@ nl) v (low_internal_ram ? s) in888 set_low_internal_ram ? s memory902 let memory ≝ insert ? 7 (three_bits @@ nl) v (low_internal_ram ?? s) in 903 set_low_internal_ram ?? s memory 889 904 ] 890 905  INDIRECT i ⇒ 891 906 λindirect: True. 892 let register ≝ get_register ? s [[ false; false; i ]] in907 let register ≝ get_register ?? s [[ false; false; i ]] in 893 908 let 〈nu, nl〉 ≝ split ? 4 4 register in 894 909 let bit_1 ≝ get_index_v … nu 0 ? in … … 896 911 match bit_1 with 897 912 [ false ⇒ 898 let memory ≝ insert … (three_bits @@ nl) v (low_internal_ram ? s) in899 set_low_internal_ram ? s memory913 let memory ≝ insert … (three_bits @@ nl) v (low_internal_ram ?? s) in 914 set_low_internal_ram ?? s memory 900 915  true ⇒ 901 let memory ≝ insert … (three_bits @@ nl) v (high_internal_ram ? s) in902 set_high_internal_ram ? s memory916 let memory ≝ insert … (three_bits @@ nl) v (high_internal_ram ?? s) in 917 set_high_internal_ram ?? s memory 903 918 ] 904  REGISTER r ⇒ λregister: True. set_register ? s r v905  ACC_A ⇒ λacc_a: True. set_8051_sfr ? s SFR_ACC_A v906  ACC_B ⇒ λacc_b: True. set_8051_sfr ? s SFR_ACC_B v919  REGISTER r ⇒ λregister: True. set_register ?? s r v 920  ACC_A ⇒ λacc_a: True. set_8051_sfr ?? s SFR_ACC_A v 921  ACC_B ⇒ λacc_b: True. set_8051_sfr ?? s SFR_ACC_B v 907 922  EXT_INDIRECT e ⇒ 908 923 λext_indirect: True. 909 let address ≝ get_register ? s [[ false; false; e ]] in924 let address ≝ get_register ?? s [[ false; false; e ]] in 910 925 let padded_address ≝ pad 8 8 address in 911 let memory ≝ insert ? 16 padded_address v (external_ram ? s) in912 set_external_ram ? s memory926 let memory ≝ insert ? 16 padded_address v (external_ram ?? s) in 927 set_external_ram ?? s memory 913 928  EXT_INDIRECT_DPTR ⇒ 914 929 λext_indirect_dptr: True. 915 let address ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr? s SFR_DPL) in916 let memory ≝ insert ? 16 address v (external_ram ? s) in917 set_external_ram ? s memory930 let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in 931 let memory ≝ insert ? 16 address v (external_ram ?? s) in 932 set_external_ram ?? s memory 918 933  _ ⇒ 919 934 λother: False. … … 922 937 // qed. 923 938 924 definition set_arg_8: ∀M: Type[0]. ∀ s:PreStatus M. [[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]] → Byte → PreStatus M≝939 definition set_arg_8: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. [[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]] → Byte → PreStatus M code_memory ≝ 925 940 set_arg_8'. 926 941 927 lemma set_arg_8_ok: ∀M, s,x,v. clock M s = clock … (set_arg_8 Ms x v).928 #M # s #x #v whd in match set_arg_8; normalize nodelta @pi2942 lemma set_arg_8_ok: ∀M,cm,s,x,v. clock M cm s = clock … (set_arg_8 M cm s x v). 943 #M #cm #s #x #v whd in match set_arg_8; normalize nodelta @pi2 929 944 qed. 930 945 … … 980 995 qed. 981 996 982 definition get_arg_1: ∀M: Type[0]. PreStatus M→ [[ bit_addr ; n_bit_addr ; carry ]] →997 definition get_arg_1: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → [[ bit_addr ; n_bit_addr ; carry ]] → 983 998 bool → bool ≝ 984 λm, s, a, l.999 λm, cm, s, a, l. 985 1000 match a return λx. bool_to_Prop (is_in ? [[ bit_addr ; 986 1001 n_bit_addr ; … … 997 1012 let m ≝ address mod 8 in 998 1013 let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in 999 let sfr ≝ get_bit_addressable_sfr ? s ? trans l in1014 let sfr ≝ get_bit_addressable_sfr ?? s ? trans l in 1000 1015 get_index_v … sfr m ? 1001 1016  false ⇒ 1002 1017 let address ≝ nat_of_bitvector … (three_bits @@ nl) in 1003 1018 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in 1004 let t ≝ lookup … 7 address' (low_internal_ram ? s) (zero 8) in1019 let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in 1005 1020 get_index_v … t (modulus address 8) ? 1006 1021 ] … … 1016 1031 let m ≝ address mod 8 in 1017 1032 let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in 1018 let sfr ≝ get_bit_addressable_sfr ? s ? trans l in1033 let sfr ≝ get_bit_addressable_sfr ?? s ? trans l in 1019 1034 ¬(get_index_v … sfr m ?) 1020 1035  false ⇒ 1021 1036 let address ≝ nat_of_bitvector … (three_bits @@ nl) in 1022 1037 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in 1023 let trans ≝ lookup ? 7 address' (low_internal_ram ? s) (zero 8) in1038 let trans ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in 1024 1039 ¬(get_index_v … trans (modulus address 8) ?) 1025 1040 ] 1026  CARRY ⇒ λcarry: True. get_cy_flag ? s1041  CARRY ⇒ λcarry: True. get_cy_flag ?? s 1027 1042  _ ⇒ λother. 1028 1043 match other in False with [ ] … … 1037 1052 qed. 1038 1053 1039 definition set_arg_1': ∀M: Type[0]. ∀ s:PreStatus M. [[bit_addr; carry]] → Bit → Σs':PreStatus M. clock … s = clock …s' ≝1054 definition set_arg_1': ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. [[bit_addr; carry]] → Bit → Σs':PreStatus M code_memory. clock ? code_memory s = clock ? code_memory s' ≝ 1040 1055 λm: Type[0]. 1041 λs: PreStatus m. 1056 λcm. 1057 λs: PreStatus m cm. 1042 1058 λa: [[bit_addr; carry]]. 1043 1059 λv: Bit. 1044 match a return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → Σs'. clock m s = clockm s' with1060 match a return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → Σs'. clock m cm s = clock m cm s' with 1045 1061 [ BIT_ADDR b ⇒ λbit_addr: True. 1046 let 〈nu, nl〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_PSW) in1062 let 〈nu, nl〉 ≝ split ? 4 4 (get_8051_sfr ?? s SFR_PSW) in 1047 1063 let bit_1 ≝ get_index_v ?? nu 0 ? in 1048 1064 let 〈ignore, three_bits〉 ≝ split ? 1 3 nu in … … 1053 1069 let m ≝ address mod 8 in 1054 1070 let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in 1055 let sfr ≝ get_bit_addressable_sfr ? s ? t true in1071 let sfr ≝ get_bit_addressable_sfr ?? s ? t true in 1056 1072 let new_sfr ≝ set_index … sfr m v ? in 1057 set_bit_addressable_sfr ? s new_sfr t1073 set_bit_addressable_sfr ?? s new_sfr t 1058 1074  false ⇒ 1059 1075 let address ≝ nat_of_bitvector … (three_bits @@ nl) in 1060 1076 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in 1061 let t ≝ lookup ? 7 address' (low_internal_ram ? s) (zero 8) in1077 let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in 1062 1078 let n_bit ≝ set_index … t (modulus address 8) v ? in 1063 let memory ≝ insert ? 7 address' n_bit (low_internal_ram ? s) in1064 set_low_internal_ram ? s memory1079 let memory ≝ insert ? 7 address' n_bit (low_internal_ram ?? s) in 1080 set_low_internal_ram ?? s memory 1065 1081 ] 1066 1082  CARRY ⇒ 1067 1083 λcarry: True. 1068 let 〈nu, nl〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_PSW) in1084 let 〈nu, nl〉 ≝ split ? 4 4 (get_8051_sfr ?? s SFR_PSW) in 1069 1085 let bit_1 ≝ get_index_v… nu 1 ? in 1070 1086 let bit_2 ≝ get_index_v… nu 2 ? in 1071 1087 let bit_3 ≝ get_index_v… nu 3 ? in 1072 1088 let new_psw ≝ [[ v; bit_1 ; bit_2; bit_3 ]] @@ nl in 1073 set_8051_sfr ? s SFR_PSW new_psw1089 set_8051_sfr ?? s SFR_PSW new_psw 1074 1090  _ ⇒ 1075 1091 λother: False. … … 1081 1097 qed. 1082 1098 1083 definition set_arg_1: ∀M: Type[0]. PreStatus M → [[bit_addr; carry]] → Bit → PreStatus M≝ set_arg_1'.1084 1085 lemma set_arg_1_ok: ∀M, s,x,v. clock M s = clock … (set_arg_1 Ms x v).1086 #M # s #x #v whd in match set_arg_1; normalize nodelta @pi21099 definition set_arg_1: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → [[bit_addr; carry]] → Bit → PreStatus M code_memory ≝ set_arg_1'. 1100 1101 lemma set_arg_1_ok: ∀M,cm,s,x,v. clock M cm s = clock … (set_arg_1 M cm s x v). 1102 #M #cm #s #x #v whd in match set_arg_1; normalize nodelta @pi2 1087 1103 qed. 1088 1104 … … 1093 1109 1094 1110 definition load ≝ 1095 λl .1111 λl,cm. 1096 1112 λstatus. 1097 set_code_memory (BitVectorTrie Word 16) ? status (load_code_memory l).1113 set_code_memory (BitVectorTrie Word 16) ? cm status (load_code_memory l). 1098 1114 1099 1115 definition fetch_pseudo_instruction: list labelled_instruction → Word → (pseudo_instruction × Word) ≝ … … 1318 1334 1319 1335 definition address_of_word_labels ≝ 1320 λp s: PseudoStatus.1336 λpr: pseudo_assembly_program. 1321 1337 λid: Identifier. 1322 address_of_word_labels_code_mem (\snd (code_memory ? ps)) id.1338 address_of_word_labels_code_mem (\snd pr) id. 1323 1339 1324 1340 definition construct_datalabels: preamble → ? ≝
Note: See TracChangeset
for help on using the changeset viewer.