Changeset 2272 for src/ASM/Status.ma
 Timestamp:
 Jul 27, 2012, 5:53:25 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Status.ma
r2270 r2272 700 700 set_low_internal_ram … s new_low_internal_ram. 701 701 702 definition read_at_stack_pointer ≝ 703 λM: Type[0]. 704 λcode_memory:M. 705 λs: PreStatus M code_memory. 706 let 〈 nu, nl 〉 ≝ vsplit ? 4 4 (get_8051_sfr ?? s SFR_SP) in 707 let m ≝ get_index_v ?? nu O ? in 708 let r1 ≝ get_index_v ?? nu 1 ? in 709 let r2 ≝ get_index_v ?? nu 2 ? in 710 let r3 ≝ get_index_v ?? nu 3 ? in 711 let address ≝ [[ r1 ; r2 ; r3 ]] @@ nl in 702 definition read_from_internal_ram ≝ 703 λM: Type[0]. 704 λcode_memory:M. 705 λs: PreStatus M code_memory. 706 λaddr: Byte. 707 let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 addr in 712 708 let memory ≝ 713 if mthen709 if head' … bit_one then 714 710 (low_internal_ram ?? s) 715 711 else 716 712 (high_internal_ram ?? s) 717 713 in 718 lookup … address memory (zero 8).719 [1,2,3,4: 720 normalize 721 repeat (@ le_S_S)722 @ le_O_n723 ]724 qed.714 lookup … seven_bits memory (zero 8). 715 716 definition read_at_stack_pointer ≝ 717 λM: Type[0]. 718 λcode_memory:M. 719 λs: PreStatus M code_memory. 720 read_from_internal_ram M code_memory s (get_8051_sfr ?? s SFR_SP). 725 721 726 722 definition write_at_stack_pointer ≝ … … 729 725 λs: PreStatus M code_memory. 730 726 λv: Byte. 731 let 〈 nu, nl 〉 ≝ vsplit … 4 4 (get_8051_sfr ?? s SFR_SP) in 732 let bit_zero ≝ get_index_v ?? nu O ? in 733 let bit_1 ≝ get_index_v ?? nu 1 ? in 734 let bit_2 ≝ get_index_v ?? nu 2 ? in 735 let bit_3 ≝ get_index_v ?? nu 3 ? in 736 if bit_zero then 737 let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl) 738 v (high_internal_ram ?? s) in 727 let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr ?? s SFR_SP) in 728 if head' … 0 bit_one then 729 let memory ≝ insert … seven_bits v (high_internal_ram ?? s) in 739 730 set_high_internal_ram ?? s memory 740 731 else 741 let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl) 742 v (low_internal_ram ?? s) in 732 let memory ≝ insert … seven_bits v (low_internal_ram ?? s) in 743 733 set_low_internal_ram ?? s memory. 744 [1,2,3,4:745 normalize746 repeat (@ le_S_S)747 @ le_O_n748 ]749 qed.750 734 751 735 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' ≝ … … 971 955 match head' … bit_1 with 972 956 [ true ⇒ 973 let address ≝ nat_of_bitvector … seven_bits in 974 let d ≝ address ÷ 8 in 975 let m ≝ address mod 8 in 976 let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in 957 let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in 958 let trans ≝ true:::four_bits @@ [[false; false; false]] in 977 959 let sfr ≝ get_bit_addressable_sfr ?? s trans l in 978 get_index_v … sfr m?960 get_index_v … sfr (nat_of_bitvector … three_bits) ? 979 961  false ⇒ 980 let address ≝ nat_of_bitvector …seven_bits in981 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32)in962 let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in 963 let address' ≝ [[true; false; false]]@@four_bits in 982 964 let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in 983 get_index_v … t ( modulus address 8) ?965 get_index_v … t (nat_of_bitvector … three_bits) ? 984 966 ] 985 967  N_BIT_ADDR n ⇒ … … 988 970 match head' … bit_1 with 989 971 [ true ⇒ 990 let address ≝ nat_of_bitvector … seven_bits in 991 let d ≝ address ÷ 8 in 992 let m ≝ address mod 8 in 993 let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in 972 let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in 973 let trans ≝ true:::four_bits @@ [[false; false; false]] in 994 974 let sfr ≝ get_bit_addressable_sfr ?? s trans l in 995 ¬(get_index_v … sfr m?)975 ¬(get_index_v ?? sfr (nat_of_bitvector … three_bits) ?) 996 976  false ⇒ 997 let address ≝ nat_of_bitvector …seven_bits in998 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32)in977 let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in 978 let address' ≝ [[true; false; false]]@@four_bits in 999 979 let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in 1000 ¬(get_index_v … t ( modulus address 8) ?)980 ¬(get_index_v … t (nat_of_bitvector … three_bits) ?) 1001 981 ] 1002 982  CARRY ⇒ λcarry: True. get_cy_flag ?? s … … 1004 984 match other in False with [ ] 1005 985 ] (subaddressing_modein … a). 1006 @modulus_less_than986 // 1007 987 qed. 1008 988 … … 1018 998 match head' … bit_1 with 1019 999 [ true ⇒ 1020 let address ≝ nat_of_bitvector … seven_bits in 1021 let d ≝ address ÷ 8 in 1022 let m ≝ address mod 8 in 1023 let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in 1024 let sfr ≝ get_bit_addressable_sfr … s t true in 1025 let new_sfr ≝ set_index … sfr m v ? in 1026 set_bit_addressable_sfr … s new_sfr t 1000 let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in 1001 let trans ≝ true:::four_bits @@ [[false; false; false]] in 1002 let sfr ≝ get_bit_addressable_sfr … s trans true in 1003 let new_sfr ≝ set_index … sfr (nat_of_bitvector … three_bits) v ? in 1004 set_bit_addressable_sfr … s new_sfr trans 1027 1005  false ⇒ 1028 let address ≝ nat_of_bitvector …seven_bits in1029 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32)in1006 let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in 1007 let address' ≝ [[true; false; false]]@@four_bits in 1030 1008 let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in 1031 let n_bit ≝ set_index … t ( modulus address 8) v ? in1009 let n_bit ≝ set_index … t (nat_of_bitvector … three_bits) v ? in 1032 1010 let memory ≝ insert ? 7 address' n_bit (low_internal_ram ?? s) in 1033 1011 set_low_internal_ram … s memory … … 1043 1021 [ ] 1044 1022 ] (subaddressing_modein … a). 1045 @modulus_less_than1023 // 1046 1024 qed. 1047 1025
Note: See TracChangeset
for help on using the changeset viewer.