1
2(* Definitions for AMBA SoC bus protocol. See AMBA Specification v2.0 from ARM for details  *)
3(* This file mainly demos composing of model checked APB and AHB theorems using HOL *)
4
5open HolKernel Parse boolLib bossLib
6
7val _ = new_theory "amba"
8
9(* app load ["bddTools","amba_apb_def","mod16Theory","amba_ahb_def","decompTools","envTheory"]; *)
10
11open boolSyntax bossLib Ho_Rewrite Tactical Tactic PairRules pairSyntax Drule
12open amba_ahbTheory amba_apbTheory amba_common bddTools mod16Theory commonTools decompTools ksTheory muSyntaxTheory setLemmasTheory envTheory
13
14val ahb_nm = 8;  (* 1..16 *)
15val ahb_ns = 16; (* 1..16 *)
16
17(*----------------------- Bridging -------------------------- *)
18
19val Rb_state = list_mk_pair((strip_pair Rpm_state)@(strip_pair Rs_state))
20val Rb_state' = ksTools.mk_primed_state Rb_state
21
22(* AHB-APB bridge is just the conjunction of the APB master with a generic AHB slave *)
23(* Note that the actual bridging code has been abstracted out. We just assume the master and slave handle their
24   syncing correctly. This code can be added in later, if required: all its signals can be hidden, so it doesn't matter *)
25val Rb = Define `TRANS_B (^Rb_state,^Rb_state') =
26         TRANS_APB_M (^Rpm_state,^Rpm_state') /\
27         TRANS_AHB_S ^(fromMLnum (ahb_ns-1)) (^Rs_state,^Rs_state')
28`;
29
30val Ib = Define `INIT_B (^Rb_state) = T`;
31
32val I1pb = Define `INIT_APB_B (^Rb_state) = ^(rhs(concl(Drule.SPEC_ALL INIT_APB_def)))`;
33
34(* APB transition relation with master substituted by the bridge with ahb vars hidden away by exists quant*)
35val R1pb = Define `TRANS_APB_B (^Rp_state,^Rp_state') =
36(^(list_mk_exists((strip_pair Rs_state)@(strip_pair Rs_state'),lhs(concl(Drule.SPEC_ALL Rb))))) /\
37^(list_mk_conj(List.tabulate(num_apb_slaves,fn n => lhs(concl(Drule.SPEC_ALL (SPEC (fromMLnum n) TRANS_APB_S_def))))))  /\
38^(list_mk_conj(List.tabulate(num_apb_slaves,fn n => lhs(concl(Drule.SPEC_ALL (SPEC (fromMLnum n) TRANS_BUS_def))))))
39`;
40
41val r1hbt = (list_mk_exists
42    ((strip_pair bbv)@(strip_pair bbv')@(strip_pair hwsv)@(strip_pair hwsv'),
43     list_mk_conj [``INIT_AHB (^I1h_state) ==> (MOD16_IS_ZERO (^bbv') /\ MOD16_IS_ZERO (^hwsv'))``,
44                   lhs(concl(Drule.SPEC_ALL TRANS_CNT_def)),
45                   (list_mk_exists
46                    ((strip_pair mask_vars)@(strip_pair mask_vars'),
47                     list_mk_conj [``INIT_AHB (^I1h_state) ==> NO_MASK (^mask_vars)``,
48                                   lhs(concl(Drule.SPEC_ALL (SPEC (fromMLnum (nm-1)) (GEN ``n:num`` TRANS_A_def)))),
49                                   list_mk_exists((strip_pair transm_vars)@(strip_pair transm_vars')
50                                                  @(strip_pair burstm_vars)@(strip_pair burstm_vars'),
51                                                  (list_mk_conj[``INIT_AHB (^I1h_state) ==>
52                                                                  !m. m<16 ==> IDLEM m (^transm_vars)``,
53                                                                list_mk_conj(List.tabulate(nm,
54                                                                        fn n => lhs(concl(Drule.SPEC_ALL
55                                                                        (SPEC (fromMLnum n) TRANS_AHB_M_def))))),
56                                                                lhs(concl(Drule.SPEC_ALL TRANS_X_def))]))])),
57                   list_mk_exists
58                   ((strip_pair slvsplt_vars)@(strip_pair slvsplt_vars'),
59                    list_mk_conj([``INIT_AHB (^I1h_state) ==> NO_HSLVSPLT (^slvsplt_vars)``,
60                                    ``^(list_mk_exists((strip_pair Rpm_state)@(strip_pair Rpm_state'),
61                                       (lhs(concl(Drule.SPEC_ALL Rb)))))``,
62                                  list_mk_conj(List.tabulate(ns-1,fn n => lhs(concl(Drule.SPEC_ALL
63                                                                        (SPEC (fromMLnum n) TRANS_AHB_S_def)
64    ))))]))]))
65
66(* AHB transition relation with one generic slave replaced by the bridge with apb signals hidden *)
67val R1hb = Define `TRANS_AHB_B (^R1h_state,^R1h_state') = ^r1hbt`; (*FIXME: ML chokes if I put the term itself here*)
68
69(* theorems *)
70
71val maindefs = [TRANS_AHB_M_def,TRANS_X_def,(*TRANS_D_def,*)TRANS_CNT_def,TRANS_AHB_S_def,amba_ahb_I1rh]
72val abbrev_defs = [IDLE_def,BUSY_def,NOSEQ_def,SEQ_def,OKAY_def,ERROR_def,RETRY_def,SPLIT_def,SINGLE_def,INC4_def,
73                   INC4M_def,BURSTM0_def,TRANSM0_def,TRANSM1_def,IDLEM_def,BUSYM_def,NOSEQM_def,SEQM_def,ALL_SPLIT_def,
74                   MASK_def,BUSREQ_def,HSPLIT_def,NO_BUSREQ_def,NO_HSPLIT_def,NO_MASK_def,INIT_GRANT_def,GRANT_def,
75                   INIT_MASTER_def, MASTER_def,HSLVSPLT_def,SLVSPLT_def,NO_HSLVSPLT_def,HSEL_def,BB_INC_def,WS_INC_def]
76
77val unroll_ahb_CONV2 = unroll_ahb_CONV maindefs TRANS_A_def abbrev_defs
78
79(* APB is the same as APB with bridge instead of master whose ahb signals are hidden *)
80val apb1 = save_thm("APB_BRIDGE",prove(``^(lhs(concl (Drule.SPEC_ALL TRANS_APB_def))) = ^(lhs(concl (Drule.SPEC_ALL R1pb)))``,
81REWRITE_TAC [TRANS_APB_def,R1pb,Rb]
82THEN EQ_TAC THENL [
83STRIP_TAC THEN CONJ_TAC THENL [
84  REPEAT (CONV_TAC (Conv.LAST_EXISTS_CONV Conv.EXISTS_AND_CONV))
85  THEN CONJ_TAC THENL [
86    ASM_REWRITE_TAC [],
87    MAP_EVERY EXISTS_TAC (exv (fst (strip_exists(fst(dest_conj(rhs(concl (Drule.SPEC_ALL R1pb)))))))
88    (findAss (rhs(concl (Drule.SPEC_ALL
89                             (unroll_ahb_CONV2 (rhs(concl(Drule.SPEC_ALL(SPEC (fromMLnum (ns-1)) TRANS_AHB_S_def))))))))))
90    THEN (CONV_TAC unroll_ahb_CONV2)
91    THEN EVAL_TAC
92    ],
93  ASM_REWRITE_TAC []
94  ],
95REPEAT STRIP_TAC THEN ASM_REWRITE_TAC []
96]));
97
98(* AHB is the same as AHB with bridge as a generic slave whose apb signals are hidden *)
99val ahb1 = save_thm("AHB_BRIDGE",prove(``^(lhs(concl (Drule.SPEC_ALL TRANS_AHB_def))) = ^(lhs(concl (Drule.SPEC_ALL R1hb)))``,
100PURE_REWRITE_TAC [TRANS_AHB_def,R1hb,Rb]
101THEN EQ_TAC THENL [
102 STRIP_TAC
103 THEN MAP_EVERY EXISTS_TAC ((strip_pair bbv)@(strip_pair bbv')@(strip_pair hwsv)@(strip_pair hwsv'))
104 THEN REPEAT CONJ_TAC THEN PURE_ASM_REWRITE_TAC [] THENL [
105  MAP_EVERY EXISTS_TAC ((strip_pair mask_vars)@(strip_pair mask_vars'))
106  THEN REPEAT CONJ_TAC THEN PURE_ASM_REWRITE_TAC []
107  THEN MAP_EVERY EXISTS_TAC ((strip_pair transm_vars)@(strip_pair transm_vars')
108                                                  @(strip_pair burstm_vars)@(strip_pair burstm_vars'))
109  THEN REPEAT CONJ_TAC THEN PURE_ASM_REWRITE_TAC [],
110  MAP_EVERY EXISTS_TAC ((strip_pair slvsplt_vars)@(strip_pair slvsplt_vars'))
111  THEN REPEAT CONJ_TAC THEN PURE_ASM_REWRITE_TAC []
112  THEN MAP_EVERY EXISTS_TAC (exv ((strip_pair Rpm_state)@(strip_pair Rpm_state'))
113     (findAss (rhs(concl (Drule.SPEC_ALL TRANS_APB_M_def)))))
114  THEN REWRITE_TAC [TRANS_APB_M_def]
115 ],
116 STRIP_TAC
117 THEN MAP_EVERY EXISTS_TAC ((strip_pair bbv)@(strip_pair bbv')@(strip_pair hwsv)@(strip_pair hwsv'))
118 THEN REPEAT CONJ_TAC THEN PURE_ASM_REWRITE_TAC [] THENL [
119  MAP_EVERY EXISTS_TAC ((strip_pair mask_vars)@(strip_pair mask_vars'))
120  THEN REPEAT CONJ_TAC THEN PURE_ASM_REWRITE_TAC []
121  THEN MAP_EVERY EXISTS_TAC ((strip_pair transm_vars)@(strip_pair transm_vars')
122                                                  @(strip_pair burstm_vars)@(strip_pair burstm_vars'))
123  THEN REPEAT CONJ_TAC THEN PURE_ASM_REWRITE_TAC [],
124  MAP_EVERY EXISTS_TAC ((strip_pair slvsplt_vars)@(strip_pair slvsplt_vars'))
125  THEN REPEAT CONJ_TAC THEN PURE_ASM_REWRITE_TAC []
126 ]
127]));
128
129(*----------------------- Parallel synchronous composition -------------------------- *)
130
131val S01 = rhs(concl (SPEC_ALL INIT_APB_def))
132val TS1 = [(".",rhs(concl (SPEC_ALL TRANS_APB_def)))]
133val S02 = rhs(concl (SPEC_ALL INIT_AHB_def))
134val TS2 = [(".",rhs(concl (SPEC_ALL TRANS_AHB_def)))]
135val nm1 = "apb"
136val nm2 = "ahb"
137val cst = mk_prod(type_of (rand(lhs(concl(SPEC_ALL INIT_APB_def)))),
138                                type_of (rand(lhs(concl(SPEC_ALL INIT_AHB_def))))) (*type of state of product model*)
139val env = inst [alpha|->cst] ``EMPTY_ENV``
140
141val (gpscth,ks1_def,s1,s2) = mk_gen_par_sync_comp_thm S01 TS1 nm1 S02 TS2 nm2 env
142
143val _ = save_thm("APB_LIFT",gpscth) (* if well-formed f holds in APB then it holds in APB x AHB *)
144val _ = save_thm("amba_ks1_def",ks1_def)
145val _ = Define `amba_s1 (^s1) = T`
146val _ = Define `amba_s2 (^s2) = T`
147
148(*
149now we can call (inan interactive session)
150
151mk_par_sync_comp_thm (amba_gpscth,amba_ks1_def,
152                      rand(lhs(concl (SPEC_ALL amba_s1_def))), (* s1 *)
153                      rand(lhs(concl (SPEC_ALL amba_s2_def)))) (* s2 *)
154                      f NONE
155
156for some APB property f
157*)
158
159val _ = export_theory()
160