(* -*-sml-*- *) (*****************************************************************************) (* Sanity checking "ExecuteSemantics": a derived executable semantics *) (* Not for compiling. *) (*****************************************************************************) val _ = loadPath := "../official-semantics" :: "../regexp" :: !loadPath; val _ = app load ["bossLib","intLib","regexpLib","ExecuteTools"]; val _ = quietdec := true; open bossLib regexpLib; val _ = quietdec := false; fun pth t = let val () = print ("\n" ^ thm_to_string t ^ "\n\n") in t end; val EVAL = pth o bossLib.EVAL; val Define = pth o bossLib.Define; (****************************************************************************** * Set the trace level of the regular expression library: * 0: silent * 1: 1 character (either - or +) for each list element processed * 2: matches as they are discovered * 3: transitions as they are calculated * 4: internal state of the automata ******************************************************************************) val _ = set_trace "regexpTools" 2; (****************************************************************************** * Set default parsing to natural numbers rather than integers ******************************************************************************) val _ = intLib.deprecate_int(); (****************************************************************************** * Examples ******************************************************************************) (****************************************************************************** * [{s0};{s1};{s2}] |= [f1 U f2] (f1, f2 arbitrary formulas) ******************************************************************************) val _ = EVAL ``UF_SEM (FINITE[s0;s1;s2]) (F_UNTIL(f1,f2))``; (****************************************************************************** * [{s0};{s1};{s2}] |= [b1 U b2] (b1, b2 arbitrary boolean expressions ) ******************************************************************************) val _ = EVAL ``UF_SEM (FINITE[s0;s1;s2]) (F_UNTIL(F_BOOL b1, F_BOOL b2))``; (****************************************************************************** * [{s0};{s1};{s2}] |= [p1 U p2] (p1, p2 arbitrary atomic propositions) ******************************************************************************) val _ = EVAL ``UF_SEM (FINITE[s0;s1;s2]) (F_UNTIL(F_BOOL(B_PROP p1), F_BOOL(B_PROP p2)))``; (****************************************************************************** * [{s0};{s1};{s2}] |= {1}(2) ******************************************************************************) val _ = EVAL ``UF_SEM (FINITE[s0;s1;s2]) (F_UNTIL(F_BOOL(B_PROP 1), F_BOOL(B_PROP 2)))``; (****************************************************************************** * [{1};{1};{2}] |= {1}(2) ******************************************************************************) val _ = EVAL ``UF_SEM (FINITE[{1};{1};{2}]) (F_UNTIL(F_BOOL(B_PROP 1), F_BOOL(B_PROP 2)))``; (****************************************************************************** * [{1};{3};{2}] |= {1}(2) ******************************************************************************) val _ = EVAL ``UF_SEM (FINITE[{1};{3};{2}]) (F_UNTIL(F_BOOL(B_PROP 1), F_BOOL(B_PROP 2)))``; (* Can't evaluate a variable regular expression using automata! EVAL ``UF_SEM (FINITE[s0;s1;s2]) (F_SUFFIX_IMP(r,f))``; EVAL ``UF_SEM (FINITE[{1};{3};{2}]) (F_SUFFIX_IMP(r,f))``; *) (****************************************************************************** * [{1};{2};{3}] |= {n}(f) ******************************************************************************) val _ = EVAL ``UF_SEM (FINITE[{1};{2};{3}]) (F_SUFFIX_IMP (S_BOOL (B_PROP n), f))``; (****************************************************************************** * [{1};{2};{3}] |= {n}(p) ******************************************************************************) val _ = EVAL ``UF_SEM (FINITE[{1};{2};{3}]) (F_SUFFIX_IMP (S_BOOL (B_PROP n), F_BOOL(B_PROP p)))``; (****************************************************************************** * [{1};{2};{3}] |= {[*]}(f) ******************************************************************************) val _ = EVAL ``UF_SEM (FINITE[{1};{2};{3}]) (F_SUFFIX_IMP (S_REPEAT S_TRUE, f))``; (****************************************************************************** * [{1};{2};{3}] |= {[*]}(p) ******************************************************************************) val _ = EVAL ``UF_SEM (FINITE[{1};{2};{3}]) (F_SUFFIX_IMP (S_REPEAT S_TRUE, F_BOOL(B_PROP p)))``; (****************************************************************************** * [{p};{p};{p}] |= {[*]}(p) ******************************************************************************) val _ = EVAL ``UF_SEM (FINITE[{p};{p};{p}]) (F_SUFFIX_IMP (S_REPEAT S_TRUE, F_BOOL(B_PROP p)))``; (****************************************************************************** * [{p1};{p2};{p3}] |= {[*]}(p) ******************************************************************************) val _ = EVAL ``UF_SEM (FINITE[{p1};{p2};{p3}]) (F_SUFFIX_IMP (S_REPEAT S_TRUE, F_BOOL(B_PROP p)))``; (****************************************************************************** * [{1};{2};{3};{4};{5};{6};{7};{8};{9}] |= {3}(f) ******************************************************************************) val _ = EVAL ``UF_SEM (FINITE[{1};{2};{3};{4};{5};{6};{7};{8};{9}]) (F_SUFFIX_IMP(S_BOOL(B_PROP 3), f))``; (****************************************************************************** * [{1};{2};{3};{4};{5};{6};{7};{8};{9}] |= {[*];2;3}(f) ******************************************************************************) val _ = EVAL ``UF_SEM (FINITE[{1};{2};{3};{4};{5};{6};{7};{8};{9}]) (F_SUFFIX_IMP (S_CAT(S_REPEAT S_TRUE, S_CAT(S_BOOL (B_PROP 2),S_BOOL (B_PROP 3))), f))``; (****************************************************************************** * [{1};{2};{3};{4};{5};{6};{7};{8};{9}] |= {[*];2:3}(f) ******************************************************************************) val _ = EVAL ``UF_SEM (FINITE[{1};{2};{3};{4};{5};{6};{7};{8};{9}]) (F_SUFFIX_IMP (S_CAT(S_REPEAT S_TRUE, S_FUSION(S_BOOL (B_PROP 2),S_BOOL (B_PROP 3))), f))``; (****************************************************************************** * [{1};{2};{3};{4};{5};{6};{7};{8};{9}] |= {[*];2;3;[*]}(f) ******************************************************************************) val _ = EVAL ``UF_SEM (FINITE[{1};{2};{3};{4};{5};{6};{7};{8};{9}]) (F_SUFFIX_IMP (S_CAT(S_REPEAT S_TRUE, S_CAT(S_CAT(S_BOOL (B_PROP 2),S_BOOL (B_PROP 3)), S_REPEAT S_TRUE)), f))``; (****************************************************************************** * [{1};{2};{3}] |= {[*];3} ******************************************************************************) val _ = EVAL ``US_SEM [{1};{2};{3}] (S_CAT(S_REPEAT S_TRUE, S_BOOL(B_PROP 3)))``; (****************************************************************************** * [{1};{2};{3}] |= {[*];2} ******************************************************************************) val _ = EVAL ``US_SEM [{1};{2};{3}] (S_CAT(S_REPEAT S_TRUE, S_BOOL(B_PROP 2)))``; (****************************************************************************** * [{1};{2};{3}] |= {[*];2;[*]} ******************************************************************************) val _ = EVAL ``US_SEM [{1};{2};{3};{4};{5}] (S_CAT(S_REPEAT S_TRUE, S_CAT(S_BOOL(B_PROP 2), S_REPEAT S_TRUE)))``; (****************************************************************************** * [{1};{2};{3};{4};{5};{6};{7};{8};{9}] |= {1|3} |-> {[*];3}! ******************************************************************************) val _ = EVAL ``UF_SEM (FINITE[{1};{2};{3};{4};{5};{6};{7};{8};{9}]) (F_STRONG_IMP ((S_OR (S_BOOL (B_PROP 1), S_BOOL (B_PROP 3))), (S_CAT (S_REPEAT S_TRUE, S_BOOL (B_PROP 3)))))``; (****************************************************************************** * [{1};{1};{1};{1};{1};{1};{1};{1};{1}] |= always{1} ******************************************************************************) val _ = EVAL ``UF_SEM (FINITE[{1};{1};{1};{1};{1};{1};{1};{1};{1}]) (F_SERE_ALWAYS(S_BOOL(B_PROP 1)))``; (****************************************************************************** * [{1};{1};{1};{1};{1};{1};{1};{1};{1}] |= always{1;1} ******************************************************************************) val _ = EVAL ``UF_SEM (FINITE[{1};{1};{1};{1};{1};{1};{1};{1};{1}]) (F_SERE_ALWAYS(S_CAT(S_BOOL(B_PROP 1), S_BOOL(B_PROP 1))))``; (****************************************************************************** * [{1};{2};{3};{4};{4;5};{4;6};{4;7};{4;8};{4;9}] |= always{4;4} ******************************************************************************) val _ = EVAL ``UF_SEM (FINITE[{1};{2};{3};{4};{4;5};{4;6};{4;7};{4;8};{4;9}]) (F_SERE_ALWAYS(S_CAT(S_BOOL(B_PROP 4), S_BOOL(B_PROP 4))))``; (****************************************************************************** * [{1};{2};{3};{4};{4};{6};{7};{8};{9}] |= never{4;3} ******************************************************************************) val _ = EVAL ``UF_SEM (FINITE[{1};{2};{3};{4};{4};{6};{7};{8};{9}]) (F_SERE_NEVER(S_CAT(S_BOOL(B_PROP 4), S_BOOL(B_PROP 3))))``; (****************************************************************************** * [{1};{2};{3};{4};{4};{6};{7};{8};{9}] |= never{3;4} ******************************************************************************) val _ = EVAL ``UF_SEM (FINITE[{1};{2};{3};{4};{4};{6};{7};{8};{9}]) (F_SERE_NEVER(S_CAT(S_BOOL(B_PROP 3), S_BOOL(B_PROP 4))))``; (****************************************************************************** quietdec:=true;; loadPath := "../official-semantics" :: "../regexp" :: !loadPath; app load ["res_quanTools","PropertiesTheory"]; open PSLPathTheory; val resq_SS = simpLib.merge_ss [res_quanTools.resq_SS, rewrites [num_to_def,xnum_to_def,IN_DEF,num_to_def,xnum_to_def,LENGTH_def]]; quietdec:=false; val UF_SEM_SUFFIX_IMP_FALSE = store_thm ("UF_SEM_SUFFIX_IMP_FALSE", ``UF_SEM w (F_SUFFIX_IMP(r, F_BOOL B_FALSE)) = !j::(0 to LENGTH w). ~(US_SEM (SEL w (0,j)) r)``, RW_TAC (std_ss++resq_SS) [UF_SEM_def,B_SEM]); ******************************************************************************) (****************************************************************************** * Generated this from a Verilog model of the BUF example in * Chapter 4 of FoCs User's Manual (see test.v) * (www.haifa.il.ibm.com/projects/verification/focs/) ******************************************************************************) (****************************************************************************** * String version * val StoB_REQ = ``"StoB_REQ"``; * val BtoS_ACK = ``"BtoS_ACK"``; * val BtoR_REQ = ``"BtoR_REQ"``; * val RtoB_ACK = ``"RtoB_ACK"``; ******************************************************************************) (****************************************************************************** * Num version ******************************************************************************) val StoB_REQ_def = Define `StoB_REQ = 0`; val BtoS_ACK_def = Define `BtoS_ACK = 1`; val BtoR_REQ_def = Define `BtoR_REQ = 2`; val RtoB_ACK_def = Define `RtoB_ACK = 3`; quietdec := true; val SimRun_def = Define `SimRun = [{}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}; {StoB_REQ}; {StoB_REQ; BtoS_ACK}; {BtoS_ACK}; {BtoS_ACK; BtoR_REQ}; {BtoS_ACK; BtoR_REQ; RtoB_ACK}; {BtoS_ACK; RtoB_ACK}; {}]`; quietdec := false; (* A pure computeLib version *) (****************************************************************************** * SimRun |= {[*]; StoB_REQ; [*]} ******************************************************************************) val _ = time EVAL ``US_SEM SimRun (S_CAT(S_REPEAT S_TRUE, S_CAT(S_BOOL(B_PROP StoB_REQ), S_REPEAT S_TRUE)))``; (****************************************************************************** * SimRun |= {[*]; StoB_REQ; StoB_REQ; [*]} ******************************************************************************) val _ = time EVAL ``US_SEM SimRun (S_CAT(S_REPEAT S_TRUE, S_CAT(S_CAT(S_BOOL(B_PROP StoB_REQ),S_BOOL(B_PROP StoB_REQ)), S_REPEAT S_TRUE)))``; (****************************************************************************** * SimRun |= {[*]; StoB_REQ; BtoR_REQ; [*]} ******************************************************************************) val _ = time EVAL ``US_SEM SimRun (S_CAT(S_REPEAT S_TRUE, S_CAT(S_CAT(S_BOOL(B_PROP StoB_REQ),S_BOOL(B_PROP BtoR_REQ)), S_REPEAT S_TRUE)))``; (****************************************************************************** * The following 4 properties make up the vunit * four_phase_handshake_left of page 19 of the FoCs User's Manual * with "never r" replaced by "{r}(F)" ******************************************************************************) (****************************************************************************** * {[*]; !StoB_REQ & BtoS_ACK; StoB_REQ}(F) ******************************************************************************) val _ = time EVAL ``UF_SEM (FINITE SimRun) (F_SUFFIX_IMP (S_CAT(S_REPEAT S_TRUE, S_CAT(S_BOOL(B_AND(B_NOT(B_PROP StoB_REQ), B_PROP BtoS_ACK)), S_BOOL(B_PROP StoB_REQ))), F_BOOL B_FALSE))``; (****************************************************************************** * FINITE SimRun |= {[*]; StoB_REG & !BtoS_ACK; !StoB_REQ}(F) ******************************************************************************) val _ = time EVAL ``UF_SEM (FINITE SimRun) (F_SUFFIX_IMP (S_CAT(S_REPEAT S_TRUE, S_CAT(S_BOOL(B_AND(B_PROP StoB_REQ, B_NOT(B_PROP BtoS_ACK))), S_BOOL(B_NOT(B_PROP StoB_REQ)))), F_BOOL B_FALSE))``; (****************************************************************************** * FINITE SimRun |= {[*]; !BtoS_ACK & !StoB_REQ; BtoS_ACK}(F) ******************************************************************************) val _ = time EVAL ``UF_SEM (FINITE SimRun) (F_SUFFIX_IMP (S_CAT(S_REPEAT S_TRUE, S_CAT(S_BOOL(B_AND(B_NOT(B_PROP BtoS_ACK), B_NOT(B_PROP StoB_REQ))), S_BOOL(B_PROP BtoS_ACK))), F_BOOL B_FALSE))``; (****************************************************************************** * {[*]; BtoS_ACK & StoB_REQ; !BtoS_ACK}(F) ******************************************************************************) val _ = time EVAL ``UF_SEM (FINITE SimRun) (F_SUFFIX_IMP (S_CAT(S_REPEAT S_TRUE, S_CAT(S_BOOL(B_AND(B_PROP BtoS_ACK, B_PROP StoB_REQ)), S_BOOL(B_NOT(B_PROP BtoS_ACK)))), F_BOOL B_FALSE))``; (****************************************************************************** * Make "&" into an infix for F_AND ******************************************************************************) val _ = set_fixity "&" (Infixl 500); val F_AND_IX_def = xDefine "F_AND_IX" `$& f1 f2 = F_AND(f1,f2)`; (****************************************************************************** * A single property characterising a four-phase handshake ******************************************************************************) val FOUR_PHASE_def = Define `FOUR_PHASE req ack = F_SUFFIX_IMP (S_CAT(S_REPEAT S_TRUE, S_CAT(S_BOOL(B_AND(B_NOT(B_PROP req), B_PROP ack)), S_BOOL(B_PROP req))), F_BOOL B_FALSE) & F_SUFFIX_IMP (S_CAT(S_REPEAT S_TRUE, S_CAT(S_BOOL(B_AND(B_PROP req, B_NOT(B_PROP ack))), S_BOOL(B_NOT(B_PROP req)))), F_BOOL B_FALSE) & F_SUFFIX_IMP (S_CAT(S_REPEAT S_TRUE, S_CAT(S_BOOL(B_AND(B_NOT(B_PROP ack), B_NOT(B_PROP req))), S_BOOL(B_PROP ack))), F_BOOL B_FALSE) & F_SUFFIX_IMP (S_CAT(S_REPEAT S_TRUE, S_CAT(S_BOOL(B_AND(B_PROP ack, B_PROP req)), S_BOOL(B_NOT(B_PROP ack)))), F_BOOL B_FALSE)`; (****************************************************************************** * vunit four_phase_handskake_left (page 19, FoCs User's Manual) * FOUR_PHASE StoB_REQ BtoS_ACK ******************************************************************************) val _ = time EVAL ``UF_SEM (FINITE SimRun) (FOUR_PHASE StoB_REQ BtoS_ACK)``; (****************************************************************************** * vunit four_phase_handskake_right (page 20, FoCs User's Manual) * FOUR_PHASE BtoR_REQ RtoB_ACK ******************************************************************************) val _ = time EVAL ``UF_SEM (FINITE SimRun) (FOUR_PHASE BtoR_REQ RtoB_ACK)``; (****************************************************************************** * f1 before f2 = [not f2 W (f1 & not f2)] ******************************************************************************) val F_BEFORE_def = Define `F_BEFORE(f1,f2) = F_W(F_NOT f2, F_AND(f1, F_NOT f2))`; (****************************************************************************** * FINITE SimRun |= StoB_REQ before BtoS_ACK ******************************************************************************) val _ = time EVAL ``UF_SEM (FINITE SimRun) (F_BEFORE(F_BOOL(B_PROP StoB_REQ), F_BOOL(B_PROP BtoS_ACK)))``; (****************************************************************************** * FINITE SimRun |= BtoS_ACK before StoB_REQ ******************************************************************************) val _ = time EVAL ``UF_SEM (FINITE SimRun) (F_BEFORE(F_BOOL(B_PROP BtoS_ACK), F_BOOL(B_PROP StoB_REQ)))``; (****************************************************************************** * FINITE SimRun |= {[*]}(StoB_REQ before BtoS_ACK) ******************************************************************************) val _ = time EVAL ``UF_SEM (FINITE SimRun) (F_SUFFIX_IMP (S_REPEAT S_TRUE, F_BEFORE(F_BOOL(B_PROP StoB_REQ), F_BOOL(B_PROP BtoS_ACK))))``; (****************************************************************************** * FINITE SimRun |= {[*]}(BtoS_ACK before StoB_REQ) ******************************************************************************) val _ = time EVAL ``UF_SEM (FINITE SimRun) (F_SUFFIX_IMP (S_REPEAT S_TRUE, F_BEFORE(F_BOOL(B_PROP BtoS_ACK), F_BOOL(B_PROP StoB_REQ))))``; (****************************************************************************** * Make ";;" into an infix for S_CAT ******************************************************************************) val _ = set_fixity ";;" (Infixl 500); val S_CAT_IX_def = xDefine "S_CAT_IX" `$;; r1 r2 = S_CAT(r1,r2)`; (****************************************************************************** * FINITE SimRun |= {[*];!BtoS_ACK;BtoS_ACK}(F) ******************************************************************************) val _ = time EVAL ``UF_SEM (FINITE SimRun) (F_SUFFIX_IMP ((S_REPEAT(S_BOOL B_TRUE) ;; S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; S_BOOL(B_PROP BtoS_ACK)), F_BOOL B_FALSE))``; (****************************************************************************** * FINITE SimRun |= {[*];!BtoS_ACK;BtoS_ACK;[*];!BtoS_ACK;BtoS_ACK}(F) ******************************************************************************) val _ = time EVAL ``UF_SEM (FINITE SimRun) (F_SUFFIX_IMP ((S_REPEAT(S_BOOL B_TRUE) ;; S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; S_BOOL(B_PROP BtoS_ACK) ;; S_REPEAT(S_BOOL B_TRUE) ;; S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; S_BOOL(B_PROP BtoS_ACK)), F_BOOL B_FALSE))``; (****************************************************************************** * FINITE SimRun |= {[*];BtoS_ACK;[RtoB_ACK];BtoS_ACK}(F) ******************************************************************************) val _ = time EVAL ``UF_SEM (FINITE SimRun) (F_SUFFIX_IMP ((S_REPEAT(S_BOOL B_TRUE) ;; S_BOOL(B_PROP BtoS_ACK) ;; S_REPEAT(S_BOOL(B_PROP RtoB_ACK)) ;; S_BOOL(B_PROP BtoS_ACK)), F_BOOL B_FALSE))``; (****************************************************************************** * FINITE SimRun |= {[*];!BtoS_ACK;BtoS_ACK;[RtoB_ACK];!BtoS_ACK;BtoS_ACK}(F) ******************************************************************************) val _ = time EVAL ``UF_SEM (FINITE SimRun) (F_SUFFIX_IMP ((S_REPEAT(S_BOOL B_TRUE) ;; S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; S_BOOL(B_PROP BtoS_ACK) ;; S_REPEAT(S_BOOL(B_PROP RtoB_ACK)) ;; S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; S_BOOL(B_PROP BtoS_ACK)), F_BOOL B_FALSE))``; (****************************************************************************** * FINITE SimRun |= {[*];BtoS_ACK;[!RtoB_ACK];BtoS_ACK}(F) ******************************************************************************) val _ = time EVAL ``UF_SEM (FINITE SimRun) (F_SUFFIX_IMP ((S_REPEAT(S_BOOL B_TRUE) ;; S_BOOL(B_PROP BtoS_ACK) ;; S_REPEAT(S_BOOL(B_NOT(B_PROP RtoB_ACK))) ;; S_BOOL(B_PROP BtoS_ACK)), F_BOOL B_FALSE))``; (****************************************************************************** * FINITE SimRun |= {[*];!BtoS_ACK;BtoS_ACK;[!RtoB_ACK];!BtoS_ACK;BtoS_ACK}(F) ******************************************************************************) val _ = time EVAL ``UF_SEM (FINITE SimRun) (F_SUFFIX_IMP ((S_REPEAT(S_BOOL B_TRUE) ;; S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; S_BOOL(B_PROP BtoS_ACK) ;; S_REPEAT(S_BOOL(B_NOT(B_PROP RtoB_ACK))) ;; S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; S_BOOL(B_PROP BtoS_ACK)), F_BOOL B_FALSE))``; (****************************************************************************** * FINITE SimRun * |= {[*];!BtoS_ACK;BtoS_ACK;[*];!RtoB_ACK;RtoB_ACK;[*];!BtoS_ACK;BtoS_ACK}(F) ******************************************************************************) val _ = time EVAL ``UF_SEM (FINITE SimRun) (F_SUFFIX_IMP ((S_REPEAT(S_BOOL B_TRUE) ;; S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; S_BOOL(B_PROP BtoS_ACK) ;; S_REPEAT(S_BOOL(B_TRUE)) ;; S_BOOL(B_NOT(B_PROP RtoB_ACK)) ;; S_BOOL(B_PROP RtoB_ACK) ;; S_REPEAT(S_BOOL(B_TRUE)) ;; S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; S_BOOL(B_PROP BtoS_ACK)), F_BOOL B_FALSE))``; (****************************************************************************** * SimRun * |= {[*];!BtoS_ACK;BtoS_ACK; * [BtoS_ACK];[!BtoS_ACK]; * ((!RtoB_ACK;RtoB_ACK;)&&(!BtoS_ACK;!BtoS_ACK)); * [!BtoS_ACK];BtoS_ACK} ******************************************************************************) val _ = time EVAL ``US_SEM SimRun ((S_REPEAT(S_BOOL B_TRUE) ;; S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; S_BOOL(B_PROP BtoS_ACK) ;; S_REPEAT(S_BOOL(B_PROP BtoS_ACK));; S_REPEAT(S_BOOL(B_NOT(B_PROP BtoS_ACK)));; S_AND((S_BOOL(B_NOT(B_PROP RtoB_ACK)) ;; S_BOOL(B_PROP RtoB_ACK)), (S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; S_BOOL(B_NOT(B_PROP BtoS_ACK)))) ;; S_REPEAT(S_BOOL(B_NOT(B_PROP BtoS_ACK)));; S_BOOL(B_PROP BtoS_ACK)))``; (****************************************************************************** * FINITE SimRun * |= {[*];!BtoS_ACK;BtoS_ACK; * [BtoS_ACK];[!BtoS_ACK]; * ((!RtoB_ACK;RtoB_ACK;)&&(!BtoS_ACK;!BtoS_ACK)); * [!BtoS_ACK];BtoS_ACK} * (F) ******************************************************************************) val _ = time EVAL ``UF_SEM (FINITE SimRun) (F_SUFFIX_IMP ((S_REPEAT(S_BOOL B_TRUE) ;; S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; S_BOOL(B_PROP BtoS_ACK) ;; S_REPEAT(S_BOOL(B_PROP BtoS_ACK));; S_REPEAT(S_BOOL(B_NOT(B_PROP BtoS_ACK)));; S_AND((S_BOOL(B_NOT(B_PROP RtoB_ACK)) ;; S_BOOL(B_PROP RtoB_ACK)), (S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; S_BOOL(B_NOT(B_PROP BtoS_ACK)))) ;; S_REPEAT(S_BOOL(B_NOT(B_PROP BtoS_ACK)));; S_BOOL(B_PROP BtoS_ACK)), F_BOOL B_FALSE))``; (****************************************************************************** * FINITE SimRun * |= {[*];!BtoS_ACK;BtoS_ACK; * [BtoS_ACK];[!BtoS_ACK]; * ((!RtoB_ACK;RtoB_ACK;)&&(!BtoS_ACK;!BtoS_ACK)); * [!BtoS_ACK];BtoS_ACK} * (T) ******************************************************************************) val _ = time EVAL ``UF_SEM (FINITE SimRun) (F_SUFFIX_IMP ((S_REPEAT(S_BOOL B_TRUE) ;; S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; S_BOOL(B_PROP BtoS_ACK) ;; S_REPEAT(S_BOOL(B_PROP BtoS_ACK));; S_REPEAT(S_BOOL(B_NOT(B_PROP BtoS_ACK)));; S_AND((S_BOOL(B_NOT(B_PROP RtoB_ACK)) ;; S_BOOL(B_PROP RtoB_ACK)), (S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; S_BOOL(B_NOT(B_PROP BtoS_ACK)))) ;; S_REPEAT(S_BOOL(B_NOT(B_PROP BtoS_ACK)));; S_BOOL(B_PROP BtoS_ACK)), F_BOOL B_TRUE))``; (****************************************************************************** * FINITE SimRun * |= {[*];!BtoS_ACK; * BtoS_ACK; * [BtoS_ACK&!RtoB_ACK]; * [!BtoS_ACK&!RoB_ACK]; * BtoS_ACK} * (F) ******************************************************************************) val _ = time EVAL ``UF_SEM (FINITE SimRun) (F_SUFFIX_IMP ((S_REPEAT(S_BOOL B_TRUE) ;; S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; S_BOOL(B_PROP BtoS_ACK) ;; S_REPEAT(S_BOOL(B_AND(B_PROP BtoS_ACK, B_NOT(B_PROP RtoB_ACK)))) ;; S_REPEAT(S_BOOL(B_AND(B_NOT(B_PROP BtoS_ACK), B_NOT(B_PROP RtoB_ACK)))) ;; S_BOOL(B_PROP BtoS_ACK)), F_BOOL B_FALSE))``; (****************************************************************************** * FINITE SimRun |= (!BtoS_ACK & X BtoS_ACK) before (!RtoB_ACK & X RtoB_ACK) ******************************************************************************) val _ = time EVAL ``UF_SEM (FINITE SimRun) (F_BEFORE (F_AND(F_NOT(F_BOOL(B_PROP RtoB_ACK)), F_NEXT(F_BOOL(B_PROP RtoB_ACK))), F_AND(F_NOT(F_BOOL(B_PROP BtoS_ACK)), F_NEXT(F_BOOL(B_PROP BtoS_ACK)))))``; (****************************************************************************** * FINITE SimRun * |= {[*]; !BtoS_ACK; BtoS_ACK; true} * ((!RtoB_ACK & X RtoB_ACK) before (!BtoS_ACK & X BtoS_ACK)) ******************************************************************************) val _ = time EVAL ``UF_SEM (FINITE SimRun) (F_SUFFIX_IMP ((S_REPEAT(S_BOOL B_TRUE) ;; S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; S_BOOL(B_PROP BtoS_ACK) ;; S_BOOL B_TRUE), F_BEFORE (F_AND(F_NOT(F_BOOL(B_PROP RtoB_ACK)), F_NEXT(F_BOOL(B_PROP RtoB_ACK))), F_AND(F_NOT(F_BOOL(B_PROP BtoS_ACK)), F_NEXT(F_BOOL(B_PROP BtoS_ACK))))))``; (****************************************************************************** * FINITE SimRun * |= {[*]; !RtoB_ACK; RtoB_ACK; true} * ((!BtoS_ACK & X BtoS_ACK) before (!RtoB_ACK & X RtoB_ACK)) ******************************************************************************) val _ = time EVAL ``UF_SEM (FINITE SimRun) (F_SUFFIX_IMP ((S_REPEAT(S_BOOL B_TRUE) ;; S_BOOL(B_NOT(B_PROP RtoB_ACK)) ;; S_BOOL(B_PROP RtoB_ACK) ;; S_BOOL B_TRUE), F_BEFORE (F_AND(F_NOT(F_BOOL(B_PROP BtoS_ACK)), F_NEXT(F_BOOL(B_PROP BtoS_ACK))), F_AND(F_NOT(F_BOOL(B_PROP RtoB_ACK)), F_NEXT(F_BOOL(B_PROP RtoB_ACK))))))``; (****************************************************************************** * FINITE SimRun * |= {[*]; !BtoS_ACK; BtoS_ACK} * ((!RtoB_ACK & X RtoB_ACK) before (!BtoS_ACK & X BtoS_ACK)) ******************************************************************************) val _ = time EVAL ``UF_SEM (FINITE SimRun) (F_SUFFIX_IMP ((S_REPEAT(S_BOOL B_TRUE) ;; S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;; S_BOOL(B_PROP BtoS_ACK)), F_BEFORE (F_AND(F_NOT(F_BOOL(B_PROP RtoB_ACK)), F_NEXT(F_BOOL(B_PROP RtoB_ACK))), F_AND(F_NOT(F_BOOL(B_PROP BtoS_ACK)), F_NEXT(F_BOOL(B_PROP BtoS_ACK))))))``; (****************************************************************************** * FINITE SimRun * |= {[*]; !RtoB_ACK; RtoB_ACK} * ((!BtoS_ACK & X BtoS_ACK) before (!RtoB_ACK & X RtoB_ACK)) ******************************************************************************) val _ = time EVAL ``UF_SEM (FINITE SimRun) (F_SUFFIX_IMP ((S_REPEAT(S_BOOL B_TRUE) ;; S_BOOL(B_NOT(B_PROP RtoB_ACK)) ;; S_BOOL(B_PROP RtoB_ACK)), F_BEFORE (F_AND(F_NOT(F_BOOL(B_PROP BtoS_ACK)), F_NEXT(F_BOOL(B_PROP BtoS_ACK))), F_AND(F_NOT(F_BOOL(B_PROP RtoB_ACK)), F_NEXT(F_BOOL(B_PROP RtoB_ACK))))))``; (****************************************************************************** * Generating checkers from formulas. * An example from the Accellera PSL reference manual, page 45. * Mentioned in Joe Hurd's ARG Lunch, 4 November 2003. ******************************************************************************) val pureDefine = with_flag (computeLib.auto_import_definitions, false) Define; val a_def = pureDefine `a = 0`; val b_def = pureDefine `b = 1`; val c_def = pureDefine `c = 2`; val alpha = map Term [`a`,`b`,`c`]; val prop = ``F_AND (F_BOOL (B_PROP c), F_NEXT (F_W (F_BOOL (B_PROP a), F_BOOL (B_PROP b))))``; val prop_sere = time EVAL ``checker ^prop``; val sere = rhs (concl prop_sere); val sere_re = time EVAL ``sere2regexp ^sere``; val re = rhs (concl sere_re); val dfa = verilog_dfa {alphabet = alpha, name = "Checker1", regexp = re}; val _ = print ("\n\n" ^ dfa ^ "\n\n");