Changeset 821 for src/ASM/Status.ma
 Timestamp:
 May 23, 2011, 3:23:17 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

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.