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