1structure amba_common =
2struct
3
4local
5
6open HolKernel Parse boolLib bossLib
7
8open bossLib pairSyntax boolSyntax
9open mod16Theory commonTools
10
11in
12
13(* APB *)
14
15val num_apb_slaves = 2; (* this is not completely general yet: PSEL definition only allows upto 16 slaves *)
16
17val Rpm_state = ``(paddr:bool,pwrite:bool,psel:bool,psel_3:bool,psel_2:bool,psel_1:bool,psel_0:bool,penable:bool,pdata:bool,mdata:bool,maddr:bool)``
18val Rpm_state' = ksTools.mk_primed_state Rpm_state;
19
20val Rps_state = ``(paddr:bool,pwrite:bool,psel:bool,psel_3:bool,psel_2:bool,psel_1:bool,psel_0:bool,penable:bool,pdata:bool,sdata_0:bool,saddr_0:bool,sdata_1:bool,saddr_1:bool)``
21val Rps_state' = ksTools.mk_primed_state Rps_state;
22
23val Rp_state = list_mk_pair((strip_pair Rpm_state)@[``sdata_0:bool``,``saddr_0:bool``,``sdata_1:bool``,``saddr_1:bool``])
24val Rp_state' = ksTools.mk_primed_state Rp_state
25
26(* AHB *)
27
28val nm = 8; (*  2..16 *)
29val nb = 16; (* 4 or 16 *)
30val ns = 16; (* 1..16 *)
31val nw = 16; (* 4 or 16 *)
32
33val mk_bool_pair = pairSyntax.list_mk_pair o (List.map mk_bool_var)
34
35val bbv = mk_bool_pair ["bb3","bb2","bb1","bb0"]
36
37val hwsv = mk_bool_pair ["hws3","hws2","hws1","hws0"]
38
39val burstm_vars = mk_bool_pair ["hburstm_15_0","hburstm_14_0","hburstm_13_0","hburstm_12_0","hburstm_11_0","hburstm_10_0","hburstm_9_0","hburstm_8_0","hburstm_7_0","hburstm_6_0","hburstm_5_0","hburstm_4_0","hburstm_3_0","hburstm_2_0","hburstm_1_0","hburstm_0_0"]
40val burstm_vars' = ksTools.mk_primed_state burstm_vars
41
42val transm_vars = mk_bool_pair ["htransm_15_0","htransm_14_0","htransm_13_0","htransm_12_0","htransm_11_0","htransm_10_0","htransm_9_0","htransm_8_0","htransm_7_0","htransm_6_0","htransm_5_0","htransm_4_0","htransm_3_0","htransm_2_0","htransm_1_0","htransm_0_0","htransm_15_1","htransm_14_1","htransm_13_1","htransm_12_1","htransm_11_1","htransm_10_1","htransm_9_1","htransm_8_1","htransm_7_1","htransm_6_1","htransm_5_1","htransm_4_1","htransm_3_1","htransm_2_1","htransm_1_1","htransm_0_1"];
43val transm_vars' = ksTools.mk_primed_state transm_vars
44
45val split_varsl = List.map mk_bool_var ["hsplit_15","hsplit_14","hsplit_13","hsplit_12","hsplit_11","hsplit_10","hsplit_9","hsplit_8","hsplit_7","hsplit_6","hsplit_5","hsplit_4","hsplit_3","hsplit_2","hsplit_1","hsplit_0"];
46val split_vars = list_mk_pair split_varsl
47
48val mask_varsl = List.map mk_bool_var ["hmask_15","hmask_14","hmask_13","hmask_12","hmask_11","hmask_10","hmask_9","hmask_8","hmask_7","hmask_6","hmask_5","hmask_4","hmask_3","hmask_2","hmask_1","hmask_0"];
49val mask_vars = list_mk_pair mask_varsl
50
51val busreq_varsl = List.map mk_bool_var ["hbusreq_15","hbusreq_14","hbusreq_13","hbusreq_12","hbusreq_11","hbusreq_10","hbusreq_9","hbusreq_8","hbusreq_7","hbusreq_6","hbusreq_5","hbusreq_4","hbusreq_3","hbusreq_2","hbusreq_1","hbusreq_0"];
52val busreq_vars = list_mk_pair busreq_varsl
53
54val split_vars' = ksTools.mk_primed_state split_vars
55val mask_vars' = ksTools.mk_primed_state mask_vars
56val busreq_vars' = ksTools.mk_primed_state busreq_vars
57
58val nbrr = list_mk_conj(List.map mk_neg (List.drop(busreq_varsl,16-nm)))
59
60val nhsr = list_mk_conj(List.map mk_neg (List.drop(split_varsl,16-nm)))
61
62val nmr = list_mk_conj(List.map mk_neg (List.drop(mask_varsl,16-nm)))
63
64val grant_vars = mk_bool_pair ["hgrant_3","hgrant_2","hgrant_1","hgrant_0"];
65val grant_vars' = ksTools.mk_primed_state grant_vars
66
67val master_vars = mk_bool_pair ["hmaster_3","hmaster_2","hmaster_1","hmaster_0"];
68val master_vars' = ksTools.mk_primed_state master_vars
69
70val hselvl = ["hsel_3","hsel_2","hsel_1","hsel_0"];
71val hselv = mk_bool_pair hselvl
72val hselv' = ksTools.mk_primed_state hselv
73
74(* need 4 vars since slave 0 who is split capable can split on any one of 16 masters
75   at the moment we allow slaves to split on only one master at most. otherwise we need 16 vars here *)
76val slvsplt_varsl = List.map (fn l => "hslvsplt_"^(int_to_string (hd l))^"_"^(int_to_string (last l))) (cartprod [List.tabulate(ns,I),rev (List.tabulate(4,I))])
77val slvsplt_vars = mk_bool_pair slvsplt_varsl
78val slvsplt_vars' = ksTools.mk_primed_state slvsplt_vars
79val ssv = fromMLlist (List.map list_mk_pair (multi_part ((length slvsplt_varsl) div ns) (List.map mk_bool_var slvsplt_varsl)))
80
81val nss =  list_mk_conj(List.map (mk_neg o mk_bool_var) slvsplt_varsl);
82
83val bbv' = ksTools.mk_primed_state bbv
84val htransv = mk_bool_pair ["htrans_0","htrans_1"]
85val hrespv = mk_bool_pair ["hresp_0","hresp_1"]
86val hwsv' = ksTools.mk_primed_state hwsv
87
88val Im_state = list_mk_pair(List.concat (List.map strip_pair [htransv,busreq_vars]))
89
90val Is_state = list_mk_pair(List.concat (List.map strip_pair [``(haddr_0:bool,hreadyout:bool)``,
91                                                              hrespv,split_vars,hselv]))
92
93val Ia_state = list_mk_pair(List.concat (List.map strip_pair [``hreadyout:bool``,grant_vars,master_vars,busreq_vars]))
94
95val Ra_state = list_mk_pair(List.concat
96                                (List.map strip_pair [``hreadyout:bool``,grant_vars,master_vars,
97                                                      mask_vars,busreq_vars,htransv]))
98val Ra_state2 = list_mk_pair(List.concat (List.map strip_pair [``hreadyout:bool``,grant_vars,master_vars,
99                                                               busreq_vars,htransv]))
100val Ra_state' = ksTools.mk_primed_state Ra_state
101
102val Rm_state =  list_mk_pair(List.concat (List.map strip_pair [``hreadyout:bool``,grant_vars,transm_vars,busreq_vars,
103                                                               hrespv,burstm_vars,bbv,mask_vars,split_vars,master_vars]))
104val Rm_state2 =  list_mk_pair(List.concat (List.map strip_pair [``hreadyout:bool``,grant_vars,busreq_vars,hrespv,
105                                                                split_vars,master_vars]))
106val Rm_state' = ksTools.mk_primed_state Rm_state
107
108val Rs_state = list_mk_pair(List.concat (List.map strip_pair  [``hreadyout:bool``,hselv,hrespv,hwsv,htransv,
109                                                               ``hburst_0:bool``,slvsplt_vars,split_vars,grant_vars,master_vars]))
110val Rs_state2 = list_mk_pair(List.concat (List.map strip_pair  [``hreadyout:bool``,hselv,hrespv,htransv,
111                                                               ``hburst_0:bool``,split_vars,grant_vars,master_vars]))
112val Rs_state' = ksTools.mk_primed_state Rs_state
113
114
115val Rx_state =  list_mk_pair(List.concat (List.map strip_pair [``hreadyout:bool``,grant_vars,transm_vars,burstm_vars,
116                                                               htransv,``hburst_0:bool``]))
117val Rx_state2 =  list_mk_pair(List.concat (List.map strip_pair [``hreadyout:bool``,grant_vars,htransv,``hburst_0:bool``]))
118val Rx_state' = ksTools.mk_primed_state Rx_state
119
120val Rd_state =  list_mk_pair(List.concat (List.map strip_pair [``hreadyout:bool``,hselv,``haddr_0:bool``]))
121val Rd_state' = ksTools.mk_primed_state Rd_state
122
123
124val RCn_state =  list_mk_pair(List.concat (List.map strip_pair [``hreadyout:bool``,htransv,bbv,hwsv]))
125val RCn_state2 =  list_mk_pair(List.concat (List.map strip_pair [``hreadyout:bool``,htransv]))
126val RCn_state' = ksTools.mk_primed_state RCn_state
127
128val I1h_state =  list_mk_pair(undup Term.var_compare
129                                    (List.concat (List.map strip_pair [Im_state,Is_state,Ia_state,Ra_state2,RCn_state2,
130                                                                       Rm_state2,Rx_state2,(*Rd_state,*)Rs_state2])))
131val R1h_state = I1h_state
132val R1h_state' = ksTools.mk_primed_state R1h_state
133
134val mod16defs = [MOD16_ZERO_def,MOD16_ONE_def,MOD16_IS_ZERO_def,MOD16_IS_ONE_def,MOD16_INC_def,MOD16_HOLD_def,dest_mod16,
135                 dest_mod16r,dest_mod16_tup,FST_COND,SND_COND,MOD16_IS_16_def,xor_def,MOD16_N2B_def,MOD16_N2B'_def,
136                 MOD16_PROJ_def]
137val m16b = [MOD16_ZERO_def,MOD16_ONE_def,MOD16_IS_ZERO_def,MOD16_IS_ONE_def,MOD16_INC_def,
138            MOD16_INC4_def,MOD16_HOLD_def,FST_COND,SND_COND, MOD16_IS_16_def,xor_def]
139val m16n2b = [MOD16_N2B_15,MOD16_N2B_14,MOD16_N2B_13,MOD16_N2B_12,MOD16_N2B_11,MOD16_N2B_10,MOD16_N2B_9,MOD16_N2B_8,
140              MOD16_N2B_7,MOD16_N2B_6,MOD16_N2B_5,MOD16_N2B_4,MOD16_N2B_3,MOD16_N2B_2,MOD16_N2B_1,MOD16_N2B_0]
141val m16exp = [MOD16_FORALL_EXPAND16,MOD16_FORALL_EXPAND4,MOD16_FORALL_EXPAND8]
142
143(* unroll abstract model into purely boolean model *)
144fun unroll_ahb_CONV maindefs Adef abbrev_defs t =
145            (PURE_ONCE_REWRITE_CONV maindefs
146             THENC NCONV nm (PURE_ONCE_REWRITE_CONV [Adef])
147             THENC UNCHANGED_CONV (REWRITE_CONV abbrev_defs)
148              THENC UNCHANGED_CONV (SIMP_CONV (pure_ss++BETA_ss) m16exp)
149               THENC UNCHANGED_CONV (SIMP_CONV (pure_ss++numSimps.REDUCE_ss) ([COND_CLAUSES]))
150               THENC UNCHANGED_CONV (SIMP_CONV (pure_ss++EL_ss) (m16n2b))
151               THENC UNCHANGED_CONV (SIMP_CONV (pure_ss++pairSimps.PAIR_ss) ([dest_mod16r2,dest_mod16_tup]@m16b))) t
152
153
154end
155end
156