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