1(*load "bossLib"; load "pairSyntax"; load "boolSyntax"; *) 2 3(* 4once this has been compiled, model checking can be done interactively as follows: 5 6app load ["holCheck","amba_apb"]; 7val apb1 = amba_apb.mk_apb(); (* init the defs *) 8val apb2 = holCheck.holCheck apb1 handle ex => Raise ex; 9List.map (isSome o #2) (valOf (modelTools.get_results apb2)); (* should be all true *) 10 11model checking is delibrately not part of the compile because it takes too long and this is a demo 12*) 13structure amba_apb = 14struct 15 16local 17 18open Globals HolKernel Parse goalstackLib 19 20open boolSyntax bossLib Ho_Rewrite Tactical Tactic PairRules pairTheory 21open ctl2muTheory cearTools amba_apbTheory commonTools bddTools ctlTheory ctlSyntax ksTools modelTools mod16Theory amba_common 22 23in 24 25val R1rp = SIMP_RULE arith_ss ([FST,SND,TRANS_APB_M_def,TRANS_APB_S_def,TRANS_BUS_def,PSEL_def,SDATA_def,SADDR_def]@mod16defs) TRANS_APB_def; 26 27local 28 29 val 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,sdata_0:bool,saddr_0:bool,sdata_1:bool,saddr_1:bool)`` 30 val T1rp = [(".",rhs (concl(Drule.SPEC_ALL R1rp)))] 31 val bvmp = List.map (with_flag (show_types,false) term_to_string) ((pairSyntax.strip_pair state)@(pairSyntax.strip_pair (mk_primed_state state))) 32 33 (* initial states *) 34 infixr 5 C_AND infixr 5 C_OR infixr 2 C_IMP infix C_IFF 35 36 fun apb_AP s = C_AP state (mk_bool_var s) 37 38 val ctl_initp = (C_NOT(apb_AP "psel")) C_AND (C_NOT(apb_AP "penable")) 39 40 fun intpow x y = Real.trunc(Math.pow(Real.fromInt x,Real.fromInt y)) 41 42 fun apb_PSEL_proj i = if i<4 then apb_AP ("psel_"^(int_to_string i)) else failwith ("apb_PSEL_proj arg out of range") 43 44 fun apb_PSEL' n k = 45 if k=0 then 46 if n=1 then apb_AP "psel_0" else C_NOT(apb_AP "psel_0") 47 else if n >= intpow 2 k then apb_PSEL_proj k 48 else C_NOT(apb_PSEL_proj k) C_AND (apb_PSEL' (if n >= intpow 2 k then n-(intpow 2 k) else n) (k-1)) 49 50 fun apb_PSEL x = apb_PSEL' x 3 51 52 fun apb_SADDR x = if x<2 then (apb_AP ("saddr_"^(int_to_string x))) else failwith ("apb_SADDR arg out of range") 53 fun apb_SDATA x = if x<2 then (apb_AP ("sdata_"^(int_to_string x))) else failwith ("apb_SDATA arg out of range") 54 55 (* AG (~penable /\ psel /\ pwrite /\ PSEL x ==> AX AX sdata x = mdata) coherence + latency in write cycle *) 56 fun ctl_latw n = C_AG ((list_C_AND [C_NOT(apb_AP "penable"),apb_AP "psel",apb_AP "pwrite",apb_PSEL n]) 57 C_IMP ((C_AX (C_AX (apb_SDATA n))) C_IFF (apb_AP "mdata"))) 58 59 (* AG (~penable /\ psel /\ ~pwrite /\ PSEL x ==> AX AX mdata = sdata x) coherence + latency in read cycle *) 60 fun ctl_latr n = C_AG ((list_C_AND [C_NOT(apb_AP "penable"),apb_AP "psel",C_NOT(apb_AP "pwrite"),apb_PSEL n]) 61 C_IMP ((C_AX (C_AX (apb_AP "mdata")) C_IFF (apb_SDATA n)))) 62 63 (* AG (AF (psel ==> AX penable)) (the imp is there (not conj) because psel may never assert but that's not deadlock)*) 64 val ctl_dlp = C_AG (C_AF ((apb_AP "psel") C_IMP (C_AX (apb_AP "penable")))) 65 66 val ctl_latr_list = List.tabulate(2,fn n => ("ctl_latr"^(int_to_string n),ctl_latr n)) 67 val ctl_latw_list = List.tabulate(2,fn n => ("ctl_latw"^(int_to_string n),ctl_latw n)) 68in 69 70fun mk_apb() = ((set_init (rhs (concl(Drule.SPEC_ALL INIT_APB_def)))) o (set_trans T1rp) o (set_flag_ric true) o 71 (set_name "apb") o (set_vord bvmp)o (set_state state) o 72 (set_props ([("ctl_initp",ctl_initp),("ctl_dlp", ctl_dlp)]@ctl_latr_list@ctl_latw_list))) empty_model 73 74end 75 76(* additional vars used by bridge (not sure if I really need this since not doing any model checking *) 77val bvmb = ["hsel_1","hsel_1'","haddr_0","haddr_0'","hreadyout","hreadyout'","hresp_0","hresp_0'","hresp_1","hresp_1'","hws0","hws0'","hws1","hws1'","hws2","hws2'","hws3","hws3'","htrans_0","htrans_0'","htrans_1","htrans_1'","hburst_0","hburst_0'","bb2","bb2'"]; 78 79 80end 81end 82