1(* ========================================================================= *)
2(* FILE          : iclass_compScript.sml                                     *)
3(* DESCRIPTION   : Provides theorems for evaluating the models during        *)
4(*                 verification.                                             *)
5(* AUTHOR        : (c) Anthony Fox, University of Cambridge                  *)
6(* DATE          : 2005                                                      *)
7(* ========================================================================= *)
8
9(* interactive use:
10 app load ["armTheory", "coreTheory", "lemmasTheory"];
11*)
12
13open HolKernel boolLib bossLib;
14open Q pairTheory;
15open armTheory coreTheory lemmasTheory;
16
17val _ = new_theory "iclass_comp";
18
19(* ------------------------------------------------------------------------- *)
20
21val std_ss = std_ss ++ boolSimps.LET_ss;
22
23val classes = [`unexec`,`swp`,`mrs_msr`,`data_proc`,`reg_shift`,`ldr`,`str`,
24               `br`,`swi_ex`,`cdp_und`,`mrc`,`mcr`,`ldc`,`stc`];
25
26val basic_rws =
27  [FST,SND,LET_THM,UNCURRY_DEF,io_onestepTheory.ADVANCE_def,
28   iseq_distinct,GSYM iseq_distinct];
29
30val basic_rws2 = basic_rws @ [iclass_EQ_iclass,iclass2num_thm];
31
32val the_rws =
33  [RP_def,PCWA_def,RWA_def,PIPEBLL_def,BUSA_def,BUSB_def,BORROW_def,COUNT1_def,
34   MUL1_def,MSHIFT,NOPC_def,NMREQ_def,NEWINST_def,NXTIS_def,DIN_def,AREG_def,
35   NBW_def,NRW_def,NBS_def,MASK_def,SCTRLREGWRITE_def,PSRFBWRITE_def,
36   ALUAWRITE_def,ALUBWRITE_def,PSRWA_def];
37
38val the_rws2 =
39  [ALU6_def,FIELD_def,SHIFTER_def,RAA_def,RBA_def,PSRA_def,PSRDAT_def];
40
41val SPEC_SIMP =
42  (GEN_ALL o
43   RIGHT_CONV_RULE (SIMP_CONV (std_ss++rewrites basic_rws2) []) o
44   SPEC_ALL);
45
46fun SIMP_SPEC tm = (SPEC_SIMP o SPEC tm);
47fun SIMP_SPECL tm = (SPEC_SIMP o SPECL tm);
48fun map_rws rws ic = map (SIMP_SPEC ic) rws;
49
50val constant_fold_ldm_stm =
51  let val l = map (map_rws ((tl the_rws) @ (tl the_rws2))) [`ldm`,`stm`] in
52    [[SIMP_SPEC `ldm` BASELATCH_def,SIMP_SPECL [`ldm`,`tn`] ALU6_def,
53      SIMP_SPECL [`ldm`,`tm`] ALU6_def] @ (hd l),hd (tl l)]
54  end;
55
56val constant_fold_mul =
57  [(SIMP_SPECL [`mla_mul`,`tn`] ALU6_def) :: map_rws (the_rws @ (tl the_rws2))
58   `mla_mul`];
59
60val constant_fold =
61  (map (map_rws the_rws) classes) @
62   constant_fold_ldm_stm @
63   constant_fold_mul;
64
65(* Used for ALU evaluation *)
66val constant_fold_alu =
67 [SIMP_SPEC `br` OFFSET_def,SIMP_SPEC `swi_ex` OFFSET_def] @
68  List.concat (map (map_rws the_rws2)
69   [`swp`,`mrs_msr`,`data_proc`,`reg_shift`,`ldr`,`str`,
70    `br`,`swi_ex`,`mrc`,`ldc`,`stc`]);
71
72val thms = save_thm("iclass_comp_thms",
73  LIST_CONJ (map LIST_CONJ constant_fold));
74
75val ldm_stm_thms = save_thm("ldm_stm_comp_thms",
76  LIST_CONJ (map LIST_CONJ constant_fold_ldm_stm));
77
78val mul_thms = save_thm("mul_comp_thms",LIST_CONJ (hd constant_fold_mul));
79val alu_thms = save_thm("alu_comp_thms",LIST_CONJ constant_fold_alu);
80
81(* ------------------------------------------------------------------------- *)
82
83val _ = export_theory();
84