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