Changeset 313
 Timestamp:
 Nov 26, 2010, 3:33:32 PM (11 years ago)
 Location:
 Deliverables/D4.1/Matita
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Arithmetic.ma
r286 r313 28 28 ndefinition nineteen ≝ ten + nine. 29 29 ndefinition twenty_four ≝ sixteen + eight. 30 ndefinition thirty_two ≝ sixteen + sixteen. 30 31 ndefinition one_hundred ≝ ten * ten. 31 32 ndefinition one_hundred_and_twenty_eight ≝ sixteen * eight. 
Deliverables/D4.1/Matita/BitVector.ma
r275 r313 217 217 ((exponential (S (S Z)) o) * hdval) + nat_of_bitvector o tl 218 218 ]. 219 220 naxiom half_add: 221 ∀n: Nat. 222 ∀b, c: BitVector n. 223 Bool × (BitVector n). 224 225 naxiom full_add: 226 ∀n: Nat. 227 ∀b, c: BitVector n. 228 ∀d: Bit. 229 Bool × (BitVector n). 
Deliverables/D4.1/Matita/Status.ma
r311 r313 304 304 r 305 305 old_external_ram 306 old_program_counter 307 old_special_function_registers_8051 308 old_special_function_registers_8052 309 old_p1_latch 310 old_p3_latch. 311 312 ndefinition set_external_ram ≝ 313 λs: Status. 314 λr: BitVectorTrie Byte sixteen. 315 let old_code_memory ≝ code_memory s in 316 let old_low_internal_ram ≝ low_internal_ram s in 317 let old_high_internal_ram ≝ high_internal_ram s in 318 let old_program_counter ≝ program_counter s in 319 let old_special_function_registers_8051 ≝ special_function_registers_8051 s in 320 let old_special_function_registers_8052 ≝ special_function_registers_8052 s in 321 let old_p1_latch ≝ p1_latch s in 322 let old_p3_latch ≝ p3_latch s in 323 mk_Status old_code_memory 324 old_low_internal_ram 325 old_high_internal_ram 326 r 306 327 old_program_counter 307 328 old_special_function_registers_8051 … … 525 546 λs: Status. 526 547 λb: Byte. 548 λv: Byte. 527 549 let address ≝ nat_of_bitvector … b in 528 550 if (decidable_equality address one_hundred_and_twenty_eight) then 529 551 ? 530 552 else if (decidable_equality address one_hundred_and_forty_four) then 531 let status_1 ≝ set_8051_sfr s SFR_P1 bin532 let status_2 ≝ set_p1_latch s bin553 let status_1 ≝ set_8051_sfr s SFR_P1 v in 554 let status_2 ≝ set_p1_latch s v in 533 555 status_2 534 556 else if (decidable_equality address one_hundred_and_sixty) then 535 557 ? 536 558 else if (decidable_equality address one_hundred_and_seventy_six) then 537 let status_1 ≝ set_8051_sfr s SFR_P3 bin538 let status_2 ≝ set_p3_latch s bin559 let status_1 ≝ set_8051_sfr s SFR_P3 v in 560 let status_2 ≝ set_p3_latch s v in 539 561 status_2 540 562 else if (decidable_equality address one_hundred_and_fifty_three) then 541 set_8051_sfr s SFR_SBUF b563 set_8051_sfr s SFR_SBUF v 542 564 else if (decidable_equality address one_hundred_and_thirty_eight) then 543 set_8051_sfr s SFR_TL0 b565 set_8051_sfr s SFR_TL0 v 544 566 else if (decidable_equality address one_hundred_and_thirty_nine) then 545 set_8051_sfr s SFR_TL1 b567 set_8051_sfr s SFR_TL1 v 546 568 else if (decidable_equality address one_hundred_and_forty) then 547 set_8051_sfr s SFR_TH0 b569 set_8051_sfr s SFR_TH0 v 548 570 else if (decidable_equality address one_hundred_and_forty_one) then 549 set_8051_sfr s SFR_TH1 b571 set_8051_sfr s SFR_TH1 v 550 572 else if (decidable_equality address two_hundred) then 551 set_8052_sfr s SFR_T2CON b573 set_8052_sfr s SFR_T2CON v 552 574 else if (decidable_equality address two_hundred_and_two) then 553 set_8052_sfr s SFR_RCAP2L b575 set_8052_sfr s SFR_RCAP2L v 554 576 else if (decidable_equality address two_hundred_and_three) then 555 set_8052_sfr s SFR_RCAP2H b577 set_8052_sfr s SFR_RCAP2H v 556 578 else if (decidable_equality address two_hundred_and_four) then 557 set_8052_sfr s SFR_TL2 b579 set_8052_sfr s SFR_TL2 v 558 580 else if (decidable_equality address two_hundred_and_five) then 559 set_8052_sfr s SFR_TH2 b581 set_8052_sfr s SFR_TH2 v 560 582 else if (decidable_equality address one_hundred_and_thirty_five) then 561 set_8051_sfr s SFR_PCON b583 set_8051_sfr s SFR_PCON v 562 584 else if (decidable_equality address one_hundred_and_thirty_six) then 563 set_8051_sfr s SFR_TCON b585 set_8051_sfr s SFR_TCON v 564 586 else if (decidable_equality address one_hundred_and_thirty_seven) then 565 set_8051_sfr s SFR_TMOD b587 set_8051_sfr s SFR_TMOD v 566 588 else if (decidable_equality address one_hundred_and_fifty_two) then 567 set_8051_sfr s SFR_SCON b589 set_8051_sfr s SFR_SCON v 568 590 else if (decidable_equality address one_hundred_and_sixty_eight) then 569 set_8051_sfr s SFR_IE b591 set_8051_sfr s SFR_IE v 570 592 else if (decidable_equality address one_hundred_and_eighty_four) then 571 set_8051_sfr s SFR_IP b593 set_8051_sfr s SFR_IP v 572 594 else if (decidable_equality address one_hundred_and_twenty_nine) then 573 set_8051_sfr s SFR_SP b595 set_8051_sfr s SFR_SP v 574 596 else if (decidable_equality address one_hundred_and_thirty) then 575 set_8051_sfr s SFR_DPL b597 set_8051_sfr s SFR_DPL v 576 598 else if (decidable_equality address one_hundred_and_thirty_one) then 577 set_8051_sfr s SFR_DPH b599 set_8051_sfr s SFR_DPH v 578 600 else if (decidable_equality address two_hundred_and_eight) then 579 set_8051_sfr s SFR_PSW b601 set_8051_sfr s SFR_PSW v 580 602 else if (decidable_equality address two_hundred_and_twenty_four) then 581 set_8051_sfr s SFR_ACC_A b603 set_8051_sfr s SFR_ACC_A v 582 604 else if (decidable_equality address two_hundred_and_forty) then 583 set_8051_sfr s SFR_ACC_B b605 set_8051_sfr s SFR_ACC_B v 584 606 else 585 607 ?. … … 695 717 ] 696 718 ] (subaddressing_modein … a). 697 698 naxiom half_add:699 ∀n: Nat.700 ∀b, c: BitVector n.701 BitVector n × Bool.702 719 703 720 ndefinition get_arg_8: Status → Bool → [[ direct ; indirect ; register ; … … 727 744 let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in 728 745 let padded_acc ≝ pad eight eight (get_8051_sfr s SFR_ACC_A) in 729 let 〈 address, carry〉 ≝ half_add sixteen dptr padded_acc in746 let 〈 carry, address 〉 ≝ half_add sixteen dptr padded_acc in 730 747 lookup … sixteen address (external_ram s) (zero eight) 731 748  ACC_PC ⇒ 732 749 λacc_pc: True. 733 750 let padded_acc ≝ pad eight eight (get_8051_sfr s SFR_ACC_A) in 734 let 〈 address, carry〉 ≝ half_add sixteen (program_counter s) padded_acc in751 let 〈 carry, address 〉 ≝ half_add sixteen (program_counter s) padded_acc in 735 752 lookup … sixteen address (external_ram s) (zero eight) 736 753  DIRECT d ⇒ … … 765 782 ##] 766 783 nqed. 767 nqed. 784 785 (* 786 ndefinition get_arg_1: Status → [[ bit_addr ; n_bit_addr ; carry ]] → 787 Bool → Bool ≝ 788 λs, a, l. 789 match a return λx. bool_to_Prop (is_in ? [[ bit_addr ; 790 n_bit_addr ; 791 carry ]] x) → ? with 792 [ BIT_ADDR b ⇒ 793 λbit_addr: True. 794 let 〈 nu, nl 〉 ≝ split … four four b in 795 let bit_one ≝ get_index … nu one ? in 796 let 〈 bit_one_v, three_bits 〉 ≝ split ? one three nu in 797 match bit_one with 798 [ true ⇒ 799 let address ≝ nat_of_bitvector … (three_bits @@ nl) in 800 let d ≝ address ÷ eight in 801 let m ≝ address mod eight in 802 let trans ≝ bitvector_of_nat ((d * eight) + one_hundred_and_twenty_eight) eight in 803 let sfr ≝ get_bit_addressable_sfr s ? trans l in 804 get_index ? sfr m ? 805  false ⇒ 806 let address ≝ nat_of_bitvector … (three_bits @@ nl) in 807 let address' ≝ bitvector_of_nat ((address ÷ eight) + thirty_two) seven in 808 let t ≝ lookup … seven address' (low_internal_ram s) (zero eight) in 809 get_index ? t (modulus address eight) ? 810 ] 811  N_BIT_ADDR n ⇒ 812 λn_bit_addr: True. 813 let 〈 nu, nl 〉 ≝ split … four four n in 814 let bit_one ≝ get_index … nu one ? in 815 let 〈 bit_one_v, three_bits 〉 ≝ split ? one three nu in 816 match bit_one with 817 [ true ⇒ 818 let address ≝ nat_of_bitvector … (three_bits @@ nl) in 819 let d ≝ address ÷ eight in 820 let m ≝ address mod eight in 821 let trans ≝ bitvector_of_nat ((d * eight) + one_hundred_and_twenty_eight) eight in 822 let sfr ≝ get_bit_addressable_sfr s ? trans l in 823 negation (get_index ? sfr m ?) 824  false ⇒ 825 let address ≝ nat_of_bitvector … (three_bits @@ nl) in 826 let address' ≝ bitvector_of_nat ((address ÷ eight) + thirty_two) seven in 827 let trans ≝ lookup … seven address' (low_internal_ram s) (zero eight) in 828 negation (get_index ? trans (modulus address eight) ?) 829 ] 830  CARRY ⇒ λcarry: True. get_cy_flag s 831  _ ⇒ λother. 832 match other in False with [ ] 833 ] (subaddressing_modein … a). *) 834 835 ndefinition set_arg_8: Status → [[ direct ; indirect ; register ; 836 acc_a ; acc_b ; ext_indirect ; 837 ext_indirect_dptr ]] → Byte → Status ≝ 838 λs, a, v. 839 match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; register ; 840 acc_a ; acc_b ; ext_indirect ; 841 ext_indirect_dptr ]] x) → ? with 842 [ DIRECT d ⇒ 843 λdirect: True. 844 let 〈 nu, nl 〉 ≝ split … four four d in 845 let bit_one ≝ get_index … nu one ? in 846 let 〈 ignore, three_bits 〉 ≝ split ? one three nu in 847 match bit_one with 848 [ true ⇒ set_bit_addressable_sfr s d v 849  false ⇒ 850 let memory ≝ insert ? seven (three_bits @@ nl) v (low_internal_ram s) in 851 set_low_internal_ram s memory 852 ] 853  INDIRECT i ⇒ 854 λindirect: True. ? 855  REGISTER r1 r2 r3 ⇒ λregister: True. set_register s r1 r2 r3 v 856  ACC_A ⇒ λacc_a: True. set_8051_sfr s SFR_ACC_A v 857  ACC_B ⇒ λacc_b: True. set_8051_sfr s SFR_ACC_B v 858  EXT_INDIRECT e ⇒ 859 λext_indirect: True. 860 let address ≝ get_register s false false e in 861 let padded_address ≝ pad eight eight address in 862 let memory ≝ insert ? sixteen padded_address v (external_ram s) in 863 set_external_ram s memory 864  EXT_INDIRECT_DPTR ⇒ 865 λext_indirect_dptr: True. 866 let address ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in 867 let memory ≝ insert ? sixteen address v (external_ram s) in 868 set_external_ram s memory 869  _ ⇒ 870 λother: False. 871 match other in False with [ ] 872 ] (subaddressing_modein … a).
Note: See TracChangeset
for help on using the changeset viewer.