Changeset 281 for Deliverables/D4.1/Matita/Status.ma
 Timestamp:
 Nov 24, 2010, 6:29:12 PM (11 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Status.ma
r276 r281 95 95 96 96 special_function_registers_8051: Vector Byte nineteen; 97 special_function_registers_8052: Vector Byte five 97 special_function_registers_8052: Vector Byte five; 98 99 p1_latch: Byte; 100 p3_latch: Byte 98 101 }. 99 102 … … 174 177 ndefinition set_program_counter ≝ 175 178 λs: Status. 176 λi: SFR8052.177 179 λw: Word. 178 let index ≝ sfr_8052_index i in179 180 let old_code_memory ≝ code_memory s in 180 181 let old_low_internal_ram ≝ low_internal_ram s in … … 358 359 (zero sixteen) 359 360 (replicate Byte nineteen (zero eight)) 360 (replicate Byte five (zero eight)) in 361 status. 361 (replicate Byte five (zero eight)) 362 (zero eight) 363 (zero eight) in 364 set_program_counter status (bitvector_of_nat sixteen seven). 365 366 naxiom not_implemented: False. 367 368 include "Arithmetic.ma". 369 370 ndefinition get_bit_addressable_sfr ≝ 371 λs: Status. 372 λn: Nat. 373 λb: BitVector n. 374 λl: Bool. 375 let address ≝ nat_of_bitvector … b in 376 if (decidable_equality address one_hundred_and_twenty_eight) then 377 ? 378 else if (decidable_equality address one_hundred_and_forty_four) then 379 if l then 380 (p1_latch s) 381 else 382 (get_8051_sfr s SFR_P1) 383 else if (decidable_equality address one_hundred_and_sixty) then 384 ? 385 else if (decidable_equality address one_hundred_and_seventy_six) then 386 if l then 387 (p3_latch s) 388 else 389 (get_8051_sfr s SFR_P3) 390 else if (decidable_equality address one_hundred_and_fifty_three) then 391 get_8051_sfr s SFR_SBUF 392 else if (decidable_equality address one_hundred_and_thirty_eight) then 393 get_8051_sfr s SFR_TL0 394 else if (decidable_equality address one_hundred_and_thirty_nine) then 395 get_8051_sfr s SFR_TL1 396 else if (decidable_equality address one_hundred_and_forty) then 397 get_8051_sfr s SFR_TH0 398 else if (decidable_equality address one_hundred_and_forty_one) then 399 get_8051_sfr s SFR_TH1 400 else if (decidable_equality address two_hundred) then 401 get_8052_sfr s SFR_T2CON 402 else if (decidable_equality address two_hundred_and_two) then 403 get_8052_sfr s SFR_RCAP2L 404 else if (decidable_equality address two_hundred_and_three) then 405 get_8052_sfr s SFR_RCAP2H 406 else if (decidable_equality address two_hundred_and_four) then 407 get_8052_sfr s SFR_TL2 408 else if (decidable_equality address two_hundred_and_five) then 409 get_8052_sfr s SFR_TH2 410 else if (decidable_equality address one_hundred_and_thirty_five) then 411 get_8051_sfr s SFR_PCON 412 else if (decidable_equality address one_hundred_and_thirty_six) then 413 get_8051_sfr s SFR_TCON 414 else if (decidable_equality address one_hundred_and_thirty_seven) then 415 get_8051_sfr s SFR_TMOD 416 else if (decidable_equality address one_hundred_and_fifty_two) then 417 get_8051_sfr s SFR_SCON 418 else if (decidable_equality address one_hundred_and_sixty_eight) then 419 get_8051_sfr s SFR_IE 420 else if (decidable_equality address one_hundred_and_eighty_four) then 421 get_8051_sfr s SFR_IP 422 else if (decidable_equality address one_hundred_and_twenty_nine) then 423 get_8051_sfr s SFR_SP 424 else if (decidable_equality address one_hundred_and_thirty) then 425 get_8051_sfr s SFR_DPL 426 else if (decidable_equality address one_hundred_and_thirty_one) then 427 get_8051_sfr s SFR_DPH 428 else if (decidable_equality address two_hundred_and_eight) then 429 get_8051_sfr s SFR_PSW 430 else if (decidable_equality address two_hundred_and_twenty_four) then 431 get_8051_sfr s SFR_ACC_A 432 else if (decidable_equality address two_hundred_and_forty) then 433 get_8051_sfr s SFR_ACC_B 434 else 435 ?. 436 ncases not_implemented. 437 nqed.
Note: See TracChangeset
for help on using the changeset viewer.