Changeset 2172 for src/ASM/Test.ma
- Timestamp:
- Jul 10, 2012, 2:39:38 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Test.ma
r2171 r2172 1 (**************************************************************************)2 (* ___ *)3 (* ||M|| *)4 (* ||A|| A project by Andrea Asperti *)5 (* ||T|| *)6 (* ||I|| Developers: *)7 (* ||T|| The HELM team. *)8 (* ||A|| http://helm.cs.unibo.it *)9 (* \ / *)10 (* \ / This file is distributed under the terms of the *)11 (* v GNU General Public License Version 2 *)12 (* *)13 (**************************************************************************)14 15 1 include "ASM/Assembly.ma". 16 2 include "ASM/Interpret.ma". … … 316 302 // 317 303 qed. 318 319 definition sfr_of_Byte: Byte → option (SFR8051 + SFR8052) ≝ 320 λb: Byte. 321 let address ≝ nat_of_bitvector … b in 322 if (eqb address 128) then None ? 323 else if (eqb address 144) then Some … (inl … SFR_P1) 324 else if (eqb address 160) then None ? 325 else if (eqb address 176) then Some … (inl … SFR_P3) 326 else if (eqb address 153) then Some … (inl … SFR_SBUF) 327 else if (eqb address 138) then Some … (inl … SFR_TL0) 328 else if (eqb address 139) then Some … (inl … SFR_TL1) 329 else if (eqb address 140) then Some … (inl … SFR_TH0) 330 else if (eqb address 141) then Some … (inl … SFR_TH1) 331 else if (eqb address 200) then Some … (inr … SFR_T2CON) 332 else if (eqb address 202) then Some … (inr … SFR_RCAP2L) 333 else if (eqb address 203) then Some … (inr … SFR_RCAP2H) 334 else if (eqb address 204) then Some … (inr … SFR_TL2) 335 else if (eqb address 205) then Some … (inr … SFR_TH2) 336 else if (eqb address 135) then Some … (inl … SFR_PCON) 337 else if (eqb address 136) then Some … (inl … SFR_TCON) 338 else if (eqb address 137) then Some … (inl … SFR_TMOD) 339 else if (eqb address 152) then Some … (inl … SFR_SCON) 340 else if (eqb address 168) then Some … (inl … SFR_IE) 341 else if (eqb address 184) then Some … (inl … SFR_IP) 342 else if (eqb address 129) then Some … (inl … SFR_SP) 343 else if (eqb address 130) then Some … (inl … SFR_DPL) 344 else if (eqb address 131) then Some … (inl … SFR_DPH) 345 else if (eqb address 208) then Some … (inl … SFR_PSW) 346 else if (eqb address 224) then Some … (inl … SFR_ACC_A) 347 else if (eqb address 240) then Some … (inl … SFR_ACC_B) 348 else None ?. 349 350 definition set_bit_addressable_sfr: 351 ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. Byte → Byte → 352 PreStatus M code_memory ≝ 353 λM: Type[0]. 354 λcode_memory:M. 355 λs: PreStatus M code_memory. 356 λb: Byte. 357 λv: Byte. 358 match sfr_of_Byte b with 359 [ None ⇒ match not_implemented in False with [ ] 360 | Some sfr8051_8052 ⇒ 361 match sfr8051_8052 with 362 [ inl sfr ⇒ 363 match sfr with 364 [ SFR_P1 ⇒ 365 let status_1 ≝ set_8051_sfr ?? s SFR_P1 v in 366 set_p1_latch ?? s v 367 | SFR_P3 ⇒ 368 let status_1 ≝ set_8051_sfr ?? s SFR_P3 v in 369 set_p3_latch ?? s v 370 | _ ⇒ set_8051_sfr ?? s sfr v ] 371 | inr sfr ⇒ set_8052_sfr ?? s sfr v ]]. 372 304 373 305 definition map_address_Byte_using_internal_pseudo_address_map ≝ 374 306 λM,sigma,d,v. … … 376 308 [ None ⇒ v 377 309 | Some sfr8051_8052 ⇒ 378 match sfr8051_8052 with 379 [ inl sfr ⇒ 380 map_address_using_internal_pseudo_address_map M sigma sfr v 381 | inr _ ⇒ v ]]. 310 match sfr8051_8052 with 311 [ inl sfr ⇒ 312 map_address_using_internal_pseudo_address_map M sigma sfr v 313 | inr _ ⇒ v 314 ] 315 ]. 382 316 383 317 lemma set_bit_addressable_sfr_status_of_pseudo_status': … … 390 324 =status_of_pseudo_status M code_memory 391 325 (set_bit_addressable_sfr pseudo_assembly_program code_memory s d v) sigma policy). 326 whd in match map_address_Byte_using_internal_pseudo_address_map; 392 327 whd in match set_bit_addressable_sfr; 393 whd in match map_address_Byte_using_internal_pseudo_address_map;394 328 normalize nodelta 395 329 @(let M ≝ pseudo_assembly_program in … … 412 346 | _ ⇒ set_8051_sfr ?? s sfr v ] 413 347 | inr sfr ⇒ set_8052_sfr ?? s sfr v ]]) 414 normalize nodelta415 /2 by refl, set_8051_sfr_status_of_pseudo_status, set_8052_sfr_status_of_pseudo_status/416 whd in match map_address_using_internal_pseudo_address_map; normalize nodelta //348 normalize nodelta 349 /2 by refl, set_8051_sfr_status_of_pseudo_status, set_8052_sfr_status_of_pseudo_status/ 350 whd in match map_address_using_internal_pseudo_address_map; normalize nodelta // 417 351 qed. 418 352 … … 610 544 map_address_using_internal_pseudo_address_map M sigma SFR_ACC_A v 611 545 | _ ⇒ v ]. 612 613 definition set_arg_8: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. ∀addr: [[ direct ; indirect ; registr ;614 acc_a ; acc_b ; ext_indirect ;615 ext_indirect_dptr ]]. Byte → PreStatus M code_memory ≝616 λm, cm, s, a, v.617 match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;618 acc_a ; acc_b ; ext_indirect ;619 ext_indirect_dptr ]] x) →620 PreStatus m cm621 with622 [ DIRECT d ⇒623 λdirect: True.624 let 〈 bit_one, seven_bits 〉 ≝ vsplit ? 1 7 d in625 match head' … bit_one with626 [ true ⇒ set_bit_addressable_sfr ?? s (true:::seven_bits) v627 | false ⇒628 let memory ≝ insert ? 7 seven_bits v (low_internal_ram ?? s) in629 set_low_internal_ram ?? s memory630 ]631 | INDIRECT i ⇒632 λindirect: True.633 let register ≝ get_register ?? s [[ false; false; i ]] in634 let 〈bit_one, seven_bits〉 ≝ vsplit ? 1 7 register in635 match head' … bit_one with636 [ false ⇒637 let memory ≝ insert … seven_bits v (low_internal_ram ?? s) in638 set_low_internal_ram ?? s memory639 | true ⇒640 let memory ≝ insert … seven_bits v (high_internal_ram ?? s) in641 set_high_internal_ram ?? s memory642 ]643 | REGISTER r ⇒ λregister: True. set_register ?? s r v644 | ACC_A ⇒ λacc_a: True. set_8051_sfr ?? s SFR_ACC_A v645 | ACC_B ⇒ λacc_b: True. set_8051_sfr ?? s SFR_ACC_B v646 | EXT_INDIRECT e ⇒647 λext_indirect: True.648 let address ≝ get_register ?? s [[ false; false; e ]] in649 let padded_address ≝ pad 8 8 address in650 let memory ≝ insert ? 16 padded_address v (external_ram ?? s) in651 set_external_ram ?? s memory652 | EXT_INDIRECT_DPTR ⇒653 λext_indirect_dptr: True.654 let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in655 let memory ≝ insert ? 16 address v (external_ram ?? s) in656 set_external_ram ?? s memory657 | _ ⇒658 λother: False.659 match other in False with [ ]660 ] (subaddressing_modein … a).661 546 662 547 (*CSC: move elsewhere*) … … 767 652 >external_ram_status_of_pseudo_status @set_external_ram_status_of_pseudo_status ] 768 653 qed. 769 770 definition get_bit_addressable_sfr:771 ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. Byte → bool → Byte ≝772 λM: Type[0].773 λcode_memory:M.774 λs: PreStatus M code_memory.775 λb: Byte.776 λl: bool.777 match sfr_of_Byte b with778 [ None ⇒ match not_implemented in False with [ ]779 | Some sfr8051_8052 ⇒780 match sfr8051_8052 with781 [ inl sfr ⇒782 match sfr with783 [ SFR_P1 ⇒784 if l then785 p1_latch … s786 else787 get_8051_sfr … s SFR_P1788 | SFR_P3 ⇒789 if l then790 p3_latch … s791 else792 get_8051_sfr … s SFR_P3793 | _ ⇒ get_8051_sfr … s sfr794 ]795 | inr sfr ⇒ get_8052_sfr M code_memory s sfr796 ]797 ].798 799 definition get_arg_8: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → bool → [[ direct ; indirect ; registr ;800 acc_a ; acc_b ; data ; acc_dptr ;801 acc_pc ; ext_indirect ;802 ext_indirect_dptr ]] → Byte ≝803 λm, cm, s, l, a.804 match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;805 acc_a ; acc_b ; data ; acc_dptr ;806 acc_pc ; ext_indirect ;807 ext_indirect_dptr ]] x) → ? with808 [ ACC_A ⇒ λacc_a: True. get_8051_sfr ?? s SFR_ACC_A809 | ACC_B ⇒ λacc_b: True. get_8051_sfr ?? s SFR_ACC_B810 | DATA d ⇒ λdata: True. d811 | REGISTER r ⇒ λregister: True. get_register ?? s r812 | EXT_INDIRECT_DPTR ⇒813 λext_indirect_dptr: True.814 let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in815 lookup ? 16 address (external_ram ?? s) (zero 8)816 | EXT_INDIRECT e ⇒817 λext_indirect: True.818 let address ≝ get_register ?? s [[ false; false; e ]] in819 let padded_address ≝ pad 8 8 address in820 lookup ? 16 padded_address (external_ram ?? s) (zero 8)821 | ACC_DPTR ⇒822 λacc_dptr: True.823 let dptr ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in824 let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in825 let 〈carry, address〉 ≝ half_add 16 dptr padded_acc in826 lookup ? 16 address (external_ram ?? s) (zero 8)827 | ACC_PC ⇒828 λacc_pc: True.829 let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in830 let 〈 carry, address 〉 ≝ half_add 16 (program_counter ?? s) padded_acc in831 lookup ? 16 address (external_ram ?? s) (zero 8)832 | DIRECT d ⇒833 λdirect: True.834 let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 d in835 match head' … hd with836 [ true ⇒ get_bit_addressable_sfr m cm s (true:::seven_bits) l837 | false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero …)838 ]839 | INDIRECT i ⇒840 λindirect: True.841 let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 (get_register … s [[false;false;i]]) in842 match head' … hd with843 [ true ⇒ lookup ? 7 seven_bits (high_internal_ram … s) (zero …)844 | false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero …)845 ]846 | _ ⇒ λother.847 match other in False with [ ]848 ] (subaddressing_modein … a).849 654 850 655 lemma p1_latch_status_of_pseudo_status: … … 1081 886 qed. 1082 887 1083 definition get_arg_1: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → [[ bit_addr ; n_bit_addr ; carry ]] →1084 bool → bool ≝1085 λm, cm, s, a, l.1086 match a return λx. bool_to_Prop (is_in ? [[ bit_addr ;1087 n_bit_addr ;1088 carry ]] x) → ? with1089 [ BIT_ADDR b ⇒1090 λbit_addr: True.1091 let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 b in1092 match head' … bit_1 with1093 [ true ⇒1094 let address ≝ nat_of_bitvector … seven_bits in1095 let d ≝ address ÷ 8 in1096 let m ≝ address mod 8 in1097 let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in1098 let sfr ≝ get_bit_addressable_sfr ?? s trans l in1099 get_index_v … sfr m ?1100 | false ⇒1101 let address ≝ nat_of_bitvector … seven_bits in1102 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in1103 let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in1104 get_index_v … t (modulus address 8) ?1105 ]1106 | N_BIT_ADDR n ⇒1107 λn_bit_addr: True.1108 let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 n in1109 match head' … bit_1 with1110 [ true ⇒1111 let address ≝ nat_of_bitvector … seven_bits in1112 let d ≝ address ÷ 8 in1113 let m ≝ address mod 8 in1114 let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in1115 let sfr ≝ get_bit_addressable_sfr ?? s trans l in1116 ¬(get_index_v … sfr m ?)1117 | false ⇒1118 let address ≝ nat_of_bitvector … seven_bits in1119 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in1120 let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in1121 ¬(get_index_v … t (modulus address 8) ?)1122 ]1123 | CARRY ⇒ λcarry: True. get_cy_flag ?? s1124 | _ ⇒ λother.1125 match other in False with [ ]1126 ] (subaddressing_modein … a).1127 @modulus_less_than1128 qed.1129 1130 888 definition map_bit_address_mode_using_internal_pseudo_address_map_get ≝ 1131 889 λM:internal_pseudo_address_map.λcm: pseudo_assembly_program.λs:PreStatus ? cm.λsigma: Word → Word. λaddr. λl. … … 1250 1008 qed. 1251 1009 1252 definition set_arg_1': ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. [[bit_addr; carry]] → Bit → Σs':PreStatus M code_memory. clock ? code_memory s = clock ? code_memory s' ≝1253 λm: Type[0].1254 λcm.1255 λs: PreStatus m cm.1256 λa: [[bit_addr; carry]].1257 λv: Bit.1258 match a return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → Σs'. clock m cm s = clock m cm s' with1259 [ BIT_ADDR b ⇒ λbit_addr: True.1260 let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in1261 match head' … bit_1 with1262 [ true ⇒1263 let address ≝ nat_of_bitvector … seven_bits in1264 let d ≝ address ÷ 8 in1265 let m ≝ address mod 8 in1266 let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in1267 let sfr ≝ get_bit_addressable_sfr … s t true in1268 let new_sfr ≝ set_index … sfr m v ? in1269 set_bit_addressable_sfr … s new_sfr t1270 | false ⇒1271 let address ≝ nat_of_bitvector … seven_bits in1272 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in1273 let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in1274 let n_bit ≝ set_index … t (modulus address 8) v ? in1275 let memory ≝ insert ? 7 address' n_bit (low_internal_ram ?? s) in1276 set_low_internal_ram … s memory1277 ]1278 | CARRY ⇒1279 λcarry: True.1280 let 〈ignore, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in1281 let new_psw ≝ v:::seven_bits in1282 set_8051_sfr ?? s SFR_PSW new_psw1283 | _ ⇒1284 λother: False.1285 match other in False with1286 [ ]1287 ] (subaddressing_modein … a).1288 try (repeat @le_S_S @le_O_n)1289 try @modulus_less_than1290 /by/1291 cases daemon (* XXX: russell type for preservation of clock on set_bit_addressable_sfr *)1292 qed.1293 1294 definition set_arg_1:1295 ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → [[bit_addr; carry]] →1296 Bit → PreStatus M code_memory ≝ set_arg_1'.1297 1298 1010 definition map_bit_address_mode_using_internal_pseudo_address_map_set_1 ≝ 1299 1011 λM: internal_pseudo_address_map. … … 1372 1084 status_of_pseudo_status M cm (set_arg_1 … cm ps addr b) sigma policy. 1373 1085 whd in match set_arg_1; normalize nodelta 1374 whd in match set_arg_1'; normalize nodelta1375 1086 whd in match map_bit_address_mode_using_internal_pseudo_address_map_set_1; normalize nodelta 1376 1087 whd in match map_bit_address_mode_using_internal_pseudo_address_map_set_2; normalize nodelta … … 1433 1144 ] 1434 1145 qed. 1146 1147 lemma clock_status_of_pseudo_status: 1148 ∀M,cm,sigma,policy,s. 1149 clock … 1150 (code_memory_of_pseudo_assembly_program cm sigma policy) 1151 (status_of_pseudo_status M cm s sigma policy) 1152 = clock … cm s. 1153 // 1154 qed. 1155 1156 lemma set_clock_status_of_pseudo_status: 1157 ∀M,cm,sigma,policy,s,v. 1158 set_clock … 1159 (code_memory_of_pseudo_assembly_program cm sigma policy) 1160 (status_of_pseudo_status M cm s sigma policy) v 1161 = status_of_pseudo_status M cm (set_clock … cm s v) sigma policy. 1162 // 1163 qed.
Note: See TracChangeset
for help on using the changeset viewer.