Changeset 2032 for src/ASM/Status.ma
 Timestamp:
 Jun 8, 2012, 4:32:03 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Status.ma
r1946 r2032 693 693 let c ≝ get_index_v … r 1 ? in 694 694 let d ≝ get_index_v … r 2 ? in 695 let 〈 un, ln 〉 ≝ split ? 4 4 (get_8051_sfr ?? s SFR_PSW) in695 let 〈 un, ln 〉 ≝ vsplit ? 4 4 (get_8051_sfr ?? s SFR_PSW) in 696 696 let 〈 r1, r0 〉 ≝ 〈 get_index_v … 4 un 2 ?, get_index_v … 4 un 3 ? 〉 in 697 697 let offset ≝ … … 736 736 λcode_memory:M. 737 737 λs: PreStatus M code_memory. 738 let 〈 nu, nl 〉 ≝ split ? 4 4 (get_8051_sfr ?? s SFR_SP) in738 let 〈 nu, nl 〉 ≝ vsplit ? 4 4 (get_8051_sfr ?? s SFR_SP) in 739 739 let m ≝ get_index_v ?? nu O ? in 740 740 let r1 ≝ get_index_v ?? nu 1 ? in … … 761 761 λs: PreStatus M code_memory. 762 762 λv: Byte. 763 let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr ?? s SFR_SP) in763 let 〈 nu, nl 〉 ≝ vsplit … 4 4 (get_8051_sfr ?? s SFR_SP) in 764 764 let bit_zero ≝ get_index_v ?? nu O ? in 765 765 let bit_1 ≝ get_index_v ?? nu 1 ? in … … 785 785 match a return λx. bool_to_Prop (is_in ? [[ dptr ]] x) → Σs'. clock M ? s = clock M ? s' with 786 786 [ DPTR ⇒ λ_:True. 787 let 〈 bu, bl 〉 ≝ split … 8 8 v in787 let 〈 bu, bl 〉 ≝ vsplit … 8 8 v in 788 788 let status ≝ set_8051_sfr … s SFR_DPH bu in 789 789 let status ≝ set_8051_sfr … status SFR_DPL bl in … … 850 850  DIRECT d ⇒ 851 851 λdirect: True. 852 let 〈 nu, nl 〉 ≝ split ? 4 4 d in852 let 〈 nu, nl 〉 ≝ vsplit ? 4 4 d in 853 853 let bit_one ≝ get_index_v ? ? nu 0 ? in 854 let 〈 ignore, three_bits 〉 ≝ split ? 1 3 nu in854 let 〈 ignore, three_bits 〉 ≝ vsplit ? 1 3 nu in 855 855 match bit_one with 856 856 [ false ⇒ … … 861 861  INDIRECT i ⇒ 862 862 λindirect: True. 863 let 〈 nu, nl 〉 ≝ split ? 4 4 (get_register ?? s [[ false; false; i]]) in864 let 〈 bit_one_v, three_bits 〉 ≝ split ? 1 3 nu in863 let 〈 nu, nl 〉 ≝ vsplit ? 4 4 (get_register ?? s [[ false; false; i]]) in 864 let 〈 bit_one_v, three_bits 〉 ≝ vsplit ? 1 3 nu in 865 865 let bit_1 ≝ get_index_v ?? bit_one_v O ? in 866 866 match bit_1 with … … 895 895 [ DIRECT d ⇒ 896 896 λdirect: True. 897 let 〈 nu, nl 〉 ≝ split … 4 4 d in897 let 〈 nu, nl 〉 ≝ vsplit … 4 4 d in 898 898 let bit_one ≝ get_index_v ? ? nu 0 ? in 899 let 〈 ignore, three_bits 〉 ≝ split ? 1 3 nu in899 let 〈 ignore, three_bits 〉 ≝ vsplit ? 1 3 nu in 900 900 match bit_one with 901 901 [ true ⇒ set_bit_addressable_sfr ?? s d v … … 907 907 λindirect: True. 908 908 let register ≝ get_register ?? s [[ false; false; i ]] in 909 let 〈nu, nl〉 ≝ split ? 4 4 register in909 let 〈nu, nl〉 ≝ vsplit ? 4 4 register in 910 910 let bit_1 ≝ get_index_v … nu 0 ? in 911 let 〈ignore, three_bits〉 ≝ split ? 1 3 nu in911 let 〈ignore, three_bits〉 ≝ vsplit ? 1 3 nu in 912 912 match bit_1 with 913 913 [ false ⇒ … … 1004 1004 [ BIT_ADDR b ⇒ 1005 1005 λbit_addr: True. 1006 let 〈 nu, nl 〉 ≝ split … 4 4 b in1006 let 〈 nu, nl 〉 ≝ vsplit … 4 4 b in 1007 1007 let bit_1 ≝ get_index_v ? ? nu 0 ? in 1008 let 〈 bit_one_v, three_bits 〉 ≝ split ? 1 3 nu in1008 let 〈 bit_one_v, three_bits 〉 ≝ vsplit ? 1 3 nu in 1009 1009 match bit_1 with 1010 1010 [ true ⇒ … … 1023 1023  N_BIT_ADDR n ⇒ 1024 1024 λn_bit_addr: True. 1025 let 〈 nu, nl 〉 ≝ split … 4 4 n in1025 let 〈 nu, nl 〉 ≝ vsplit … 4 4 n in 1026 1026 let bit_1 ≝ get_index_v ? ? nu 0 ? in 1027 let 〈 bit_one_v, three_bits 〉 ≝ split ? 1 3 nu in1027 let 〈 bit_one_v, three_bits 〉 ≝ vsplit ? 1 3 nu in 1028 1028 match bit_1 with 1029 1029 [ true ⇒ … … 1061 1061 match a return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → Σs'. clock m cm s = clock m cm s' with 1062 1062 [ BIT_ADDR b ⇒ λbit_addr: True. 1063 let 〈nu, nl〉 ≝ split ? 4 4 (get_8051_sfr ?? s SFR_PSW) in1063 let 〈nu, nl〉 ≝ vsplit ? 4 4 (get_8051_sfr ?? s SFR_PSW) in 1064 1064 let bit_1 ≝ get_index_v ?? nu 0 ? in 1065 let 〈ignore, three_bits〉 ≝ split ? 1 3 nu in1065 let 〈ignore, three_bits〉 ≝ vsplit ? 1 3 nu in 1066 1066 match bit_1 return λ_. ? with 1067 1067 [ true ⇒ … … 1083 1083  CARRY ⇒ 1084 1084 λcarry: True. 1085 let 〈nu, nl〉 ≝ split ? 4 4 (get_8051_sfr ?? s SFR_PSW) in1085 let 〈nu, nl〉 ≝ vsplit ? 4 4 (get_8051_sfr ?? s SFR_PSW) in 1086 1086 let bit_1 ≝ get_index_v… nu 1 ? in 1087 1087 let bit_2 ≝ get_index_v… nu 2 ? in
Note: See TracChangeset
for help on using the changeset viewer.