1 2open HolKernel boolLib bossLib Parse ppc_Lib; val _ = new_theory "ppc_tests"; 3 4 5(* add 1,2,3 *) 6val _ = ppc_test "7C221A14" 7 [("PC","A0000000"),("GPR1","4444"),("GPR2","2222"),("GPR3","3333"),("CTR","123AA"), 8 ("A0000000","7C"),("A0000001","22"),("A0000002","1A"),("A0000003","14"),("A0000FFF","88"),("CARRY","T")] 9 [("PC","A0000004"),("GPR1","5555"),("GPR2","2222"),("GPR3","3333"),("CTR","123AA"), 10 ("A0000000","7C"),("A0000001","22"),("A0000002","1A"),("A0000003","14"),("A0000FFF","88"),("CARRY","T")] 11 12(* subfic 19, 26, -2 *) 13val _ = ppc_test "227AFFFE" 14 [("PC","A0344560"),("GPR26","11"),("GPR19","222"),("LR","FFFF"), 15 ("A0344560","22"),("A0344561","7A"),("A0344562","FF"),("A0344563","FE"),("A0000FFF","88"),("CARRY","T")] 16 [("PC","A0344564"),("GPR26","11"),("GPR19","FFFFFFED"),("LR","FFFF"), 17 ("A0344560","22"),("A0344561","7A"),("A0344562","FF"),("A0344563","FE"),("A0000FFF","88"),("CARRY","T")] 18 19(* sthx 2, 26, 4 *) 20val _ = ppc_test "7C5A232E" 21 [("PC","A0344560"),("GPR26","4000A0"),("GPR2","AABBCCDD"),("GPR4","8"), 22 ("A0344560","7C"),("A0344561","5A"),("A0344562","23"),("A0344563","2E"),("CARRY","T"), 23 ("4000A8","00"),("4000A9","00")] 24 [("PC","A0344564"),("GPR26","4000A0"),("GPR2","AABBCCDD"),("GPR4","8"), 25 ("A0344560","7C"),("A0344561","5A"),("A0344562","23"),("A0344563","2E"),("CARRY","T"), 26 ("4000A8","CC"),("4000A9","DD")] 27 28(* lwz 19, 234(26) *) 29val _ = ppc_test "827A00EA" 30 [("PC","A0344560"),("GPR26","400006"),("GPR19","8"), 31 ("A0344560","82"),("A0344561","7A"),("A0344562","00"),("A0344563","EA"),("CR02","T"), 32 ("4000F0","11"),("4000F1","22"),("4000F2","33"),("4000F3","44")] 33 [("PC","A0344564"),("GPR26","400006"),("GPR19","11223344"), 34 ("A0344560","82"),("A0344561","7A"),("A0344562","00"),("A0344563","EA"),("CR02","T"), 35 ("4000F0","11"),("4000F1","22"),("4000F2","33"),("4000F3","44")] 36 37 38val _ = export_theory (); 39