(******************************************************************************* * IMITATOR MODEL * * Title : spsmall * Description : Model with observer (to check whether tCKQ is conform with ST specification) * Correctness : s <= 166 * Scalable : * Generated : * Categories : Hardware ; Industrial * Source : Project ANR Valmem * bibkey : CEFX09 ; Andre10 * Author : ST-Microelectronics (design) * Modeling : LSV (timings by LIP6) * Input by : Emmanuelle Encrenaz, Laurent Fribourg, Étienne André * License : Creative Commons Attribution-ShareAlike 4.0 International (CC BY-SA 4.0) * * Created : < 2007 * Last modified : 2020/08/19 * Model version : * * IMITATOR version : 3 ******************************************************************************) var s, x_net27, x_wela, x_net13a, x_net45, x_d_int, x_en_latchd, x_en_latchwen, x_wen_h, x_d_h, x_observer : clock; (* d_up_q_0, d_up_net27, d_up_d_inta, d_dn_d_inta, d_up_wela, d_dn_wela, d_up_net45a, d_dn_net45a, d_up_net13a, d_dn_net13a, d_up_net45, d_dn_net45, d_up_d_int, d_dn_d_int, d_up_en_latchd, d_dn_en_latchd, d_up_en_latchwen, d_dn_en_latchwen, d_up_wen_h, d_dn_wen_h, d_up_d_h, d_dn_d_h, tHI, tLO, tsetupd, tsetupwen : parameter; -- 28 parameters*) d_up_q_0 = 21, d_up_net27 = 0, d_up_d_inta = 22, d_dn_d_inta = 45, d_up_wela = 0, d_dn_wela = 22, d_up_net45a = 5, d_dn_net45a = 4, d_up_net13a = 19, d_dn_net13a = 13, d_up_net45 = 21, d_dn_net45 = 22, d_up_d_int = 14, d_dn_d_int = 18, d_up_en_latchd = 28, d_dn_en_latchd = 32, d_up_en_latchwen = 5, d_dn_en_latchwen = 4, d_up_wen_h = 11, d_dn_wen_h = 8, d_up_d_h = 95, d_dn_d_h = 66, tHI = 45, tLO = 65, tsetupd (*65 .. 110*), tsetupwen (*0 .. 66*) : parameter; (*2 parameters only*) (* second_cycle -- becomes 1 at the beginning of the second clock cycle -- : discrete;*) (************************************************************) automaton abs_net27 (* ######### ABSTRACTION MANUELLE DE net27 ######### -- ######### et incorporation de retard_q0 ######### -- ######### ce qui supprime l'autom. ret_q_0 ######*) (************************************************************) synclabs: down_wela, up_wela, down_d_inta, up_d_inta, qUp; loc init_abs_net27 : invariant True when True sync up_d_inta goto A_abs_net27; when True sync down_wela goto C_abs_net27; when True sync up_wela goto init_abs_net27; when True sync down_d_inta goto init_abs_net27; loc A_abs_net27 : invariant True when True sync down_wela do {x_net27 := 0} goto B_abs_net27; when True sync up_wela goto A_abs_net27; when True sync up_d_inta goto A_abs_net27; when True sync down_d_inta goto C_abs_net27; loc B_abs_net27 : invariant x_net27 <= d_up_net27 + d_up_q_0 when True sync down_wela goto B_abs_net27; when True sync up_wela goto C_abs_net27; when True sync up_d_inta goto C_abs_net27; when True sync down_d_inta goto B_abs_net27; when x_net27 = d_up_net27+ d_up_q_0 sync qUp (*--sync up_net27*) do {} goto C_abs_net27; loc C_abs_net27 : invariant True when True sync down_wela goto C_abs_net27; when True sync up_wela goto C_abs_net27; when True sync down_d_inta goto C_abs_net27; when True sync up_d_inta goto C_abs_net27; end (*not_net27*) (************************************************************) automaton f2_wela (* wela <= net45a or net13a*) (************************************************************) synclabs: up_net45a, down_net45a, up_net13a, down_net13a, up_wela, down_wela; loc e_00_0_wela : invariant True when True sync up_net45a do {x_wela := 0} goto e_01_X_wela; when True sync up_net13a do {x_wela := 0} goto e_10_X_wela; when True sync down_net45a do {} goto e_00_0_wela; when True sync down_net13a do {} goto e_00_0_wela; loc e_01_1_wela : invariant True when True sync down_net45a do {x_wela := 0} goto e_00_X_wela; when True sync up_net13a do {x_wela := 0} goto e_11_X_wela; when True sync up_net45a do {} goto e_01_1_wela; when True sync down_net13a do {} goto e_01_1_wela; loc e_10_1_wela : invariant True when True sync up_net45a do {x_wela := 0} goto e_11_X_wela; when True sync down_net13a do {x_wela := 0} goto e_00_X_wela; when True sync down_net45a do {} goto e_10_1_wela; when True sync up_net13a do {} goto e_10_1_wela; loc e_11_1_wela : invariant True when True sync down_net45a do {x_wela := 0} goto e_10_X_wela; when True sync down_net13a do {x_wela := 0} goto e_01_X_wela; when True sync up_net45a do {} goto e_11_1_wela; when True sync up_net13a do {} goto e_11_1_wela; loc e_00_X_wela: invariant x_wela <= d_dn_wela when True sync up_net45a do {x_wela := 0} goto e_01_X_wela; when True sync up_net13a do {x_wela := 0} goto e_10_X_wela; when True sync down_net45a do {} goto e_00_X_wela; when True sync down_net13a do {} goto e_00_X_wela; when x_wela = d_dn_wela sync down_wela do {} goto e_00_0_wela; loc e_01_X_wela: invariant x_wela <= d_up_wela when True sync down_net45a do {x_wela := 0} goto e_00_X_wela; when True sync up_net13a do {x_wela := 0} goto e_11_X_wela; when True sync up_net45a do {} goto e_01_X_wela; when True sync down_net13a do {} goto e_01_X_wela; when x_wela = d_up_wela sync up_wela do {} goto e_01_1_wela; loc e_10_X_wela: invariant x_wela <= d_up_wela when True sync up_net45a do {x_wela := 0} goto e_11_X_wela; when True sync down_net13a do {x_wela := 0} goto e_00_X_wela; when True sync down_net45a do {} goto e_10_X_wela; when True sync up_net13a do {} goto e_10_X_wela; when x_wela = d_up_wela sync up_wela do {} goto e_10_1_wela; loc e_11_X_wela: invariant x_wela <= d_up_wela when True sync down_net45a do {x_wela := 0} goto e_10_X_wela; when True sync down_net13a do {x_wela := 0} goto e_01_X_wela; when True sync up_net45a do {} goto e_11_X_wela; when True sync up_net13a do {} goto e_11_X_wela; when x_wela = d_up_wela sync up_wela do {} goto e_11_1_wela; end (*f2_wela*) (************************************************************) automaton not_net13a (************************************************************) synclabs: down_ck, up_ck, down_net13a, up_net13a; loc init_not_net13a : invariant True when True sync up_ck do {x_net13a := 0} goto A_not_net13a; when True sync down_ck do {x_net13a := 0} goto B_not_net13a; loc A_not_net13a : invariant x_net13a <= d_dn_net13a when True sync down_ck do {x_net13a := 0} goto B_not_net13a; when x_net13a = d_dn_net13a sync down_net13a goto init_not_net13a; loc B_not_net13a : invariant x_net13a <= d_up_net13a when True sync up_ck do {x_net13a := 0} goto A_not_net13a; when x_net13a = d_up_net13a sync up_net13a goto init_not_net13a; end (*not_net13a*) (* INCORPORATION delai net45a entraine la suppression de l'automate retard_net45a *) (************************************************************) automaton reg_net45 (************************************************************) synclabs: down_wen_h, up_wen_h, (* inputs (data)*) down_en_latchwen, up_en_latchwen, (* inputs (enable)*) down_net45a, up_net45a ; (* outputs*) loc e0d0_U_reg_net45: invariant True when True sync down_en_latchwen do {} goto e0d0_U_reg_net45; when True sync down_wen_h do {} goto e0d0_U_reg_net45; when True sync up_en_latchwen do {x_net45 := 0} goto e1d0_X_reg_net45; when True sync up_wen_h do {} goto e0d1_U_reg_net45; loc e1d0_X_reg_net45: invariant x_net45 <= d_dn_net45 + d_dn_net45a when True sync down_wen_h do {} goto e1d0_X_reg_net45; when True sync up_en_latchwen do {} goto e1d0_X_reg_net45; when True sync down_en_latchwen do {} goto e0d0_U_reg_net45; when True sync up_wen_h do {x_net45 := 0} goto e1d1_X_reg_net45; when x_net45 = d_dn_net45 + d_dn_net45a sync down_net45a do {} goto e1d0_0_reg_net45; loc e1d0_0_reg_net45: invariant True when True sync down_wen_h do {} goto e1d0_0_reg_net45; when True sync down_en_latchwen do {} goto e0d0_U_reg_net45; when True sync up_en_latchwen do {} goto e1d0_0_reg_net45; when True sync up_wen_h do {x_net45 := 0} goto e1d1_X_reg_net45; loc e0d1_U_reg_net45: invariant True when True sync up_wen_h do {} goto e0d1_U_reg_net45; when True sync down_en_latchwen do {} goto e0d1_U_reg_net45; when True sync up_en_latchwen do {x_net45 := 0} goto e1d1_X_reg_net45; when True sync down_wen_h do {} goto e0d0_U_reg_net45; loc e1d1_X_reg_net45: invariant x_net45 <= d_up_net45 + d_up_net45a when True sync down_en_latchwen do {} goto e0d1_U_reg_net45; when True sync up_wen_h do {} goto e1d1_X_reg_net45; when True sync up_en_latchwen do {} goto e1d1_X_reg_net45; when True sync down_wen_h do {x_net45 := 0} goto e1d0_X_reg_net45; when x_net45 = d_up_net45 + d_up_net45a sync up_net45a goto e1d1_1_reg_net45; loc e1d1_1_reg_net45: invariant True when True sync down_en_latchwen do {} goto e0d1_U_reg_net45; when True sync up_en_latchwen do {} goto e1d1_1_reg_net45; when True sync down_wen_h do {x_net45 := 0} goto e1d0_X_reg_net45; when True sync up_wen_h do {} goto e1d1_1_reg_net45; end (*reg_net45*) (* INCORPORATION delai d_inta entraine la suppression de l'automate retard_d_inta *) (************************************************************) automaton reg_d_int (************************************************************) synclabs: down_d_h, up_d_h, (* inputs (data)*) down_en_latchd, up_en_latchd, (* inputs (enable)*) down_d_inta, up_d_inta ; (* outputs*) loc e0d0_U_reg_d_int: invariant True when True sync down_en_latchd do {} goto e0d0_U_reg_d_int; when True sync down_d_h do {} goto e0d0_U_reg_d_int; when True sync up_en_latchd do {x_d_int := 0} goto e1d0_X_reg_d_int; when True sync up_d_h do {} goto e0d1_U_reg_d_int; loc e1d0_X_reg_d_int: invariant x_d_int <= d_dn_d_int + d_dn_d_inta when True sync down_d_h do {} goto e1d0_X_reg_d_int; when True sync up_en_latchd do {} goto e1d0_X_reg_d_int; when True sync down_en_latchd do {} goto e0d0_U_reg_d_int; when True sync up_d_h do {x_d_int := 0} goto e1d1_X_reg_d_int; when x_d_int = d_dn_d_int + d_dn_d_inta sync down_d_inta goto e1d0_0_reg_d_int; loc e1d0_0_reg_d_int: invariant True when True sync down_d_h do {} goto e1d0_0_reg_d_int; when True sync down_en_latchd do {} goto e0d0_U_reg_d_int; when True sync up_en_latchd do {} goto e1d0_0_reg_d_int; when True sync up_d_h do {x_d_int := 0} goto e1d1_X_reg_d_int; loc e0d1_U_reg_d_int: invariant True when True sync up_d_h do {} goto e0d1_U_reg_d_int; when True sync down_en_latchd do {} goto e0d1_U_reg_d_int; when True sync up_en_latchd do {x_d_int := 0} goto e1d1_X_reg_d_int; when True sync down_d_h do {} goto e0d0_U_reg_d_int; loc e1d1_X_reg_d_int: invariant x_d_int <= d_up_d_int + d_up_d_inta when True sync down_en_latchd do {} goto e0d1_U_reg_d_int; when True sync up_d_h do {} goto e1d1_X_reg_d_int; when True sync up_en_latchd do {} goto e1d1_X_reg_d_int; when True sync down_d_h do {x_d_int := 0} goto e1d0_X_reg_d_int; when x_d_int = d_up_d_int + d_up_d_inta sync up_d_inta do {} goto e1d1_1_reg_d_int; loc e1d1_1_reg_d_int: invariant True when True sync down_en_latchd do {} goto e0d1_U_reg_d_int; when True sync up_en_latchd do {} goto e1d1_1_reg_d_int; when True sync down_d_h do {x_d_int := 0} goto e1d0_X_reg_d_int; when True sync up_d_h do {} goto e1d1_1_reg_d_int; end (*reg_d_int*) (************************************************************) automaton not_en_latchd (************************************************************) synclabs: down_ck, up_ck, down_en_latchd, up_en_latchd; loc init_not_en_latchd : invariant True when True sync up_ck do {x_en_latchd := 0} goto A_not_en_latchd; when True sync down_ck do {x_en_latchd := 0} goto B_not_en_latchd; loc A_not_en_latchd : invariant x_en_latchd <= d_dn_en_latchd when True sync down_ck do {x_en_latchd := 0} goto B_not_en_latchd; when x_en_latchd = d_dn_en_latchd sync down_en_latchd goto init_not_en_latchd; loc B_not_en_latchd : invariant x_en_latchd <= d_up_en_latchd when True sync up_ck do {x_en_latchd := 0} goto A_not_en_latchd; when x_en_latchd = d_up_en_latchd sync up_en_latchd goto init_not_en_latchd; end (*not_en_latchd*) (************************************************************) automaton not_en_latchwen (************************************************************) synclabs: down_ck, up_ck, down_en_latchwen, up_en_latchwen; loc init_not_en_latchwen : invariant True when True sync up_ck do {x_en_latchwen := 0} goto A_not_en_latchwen; when True sync down_ck do {x_en_latchwen := 0} goto B_not_en_latchwen; loc A_not_en_latchwen : invariant x_en_latchwen <= d_dn_en_latchwen when True sync down_ck do {x_en_latchwen := 0} goto B_not_en_latchwen; when x_en_latchwen = d_dn_en_latchwen sync down_en_latchwen goto init_not_en_latchwen; loc B_not_en_latchwen : invariant x_en_latchwen <= d_up_en_latchwen when True sync up_ck do {x_en_latchwen := 0} goto A_not_en_latchwen; when x_en_latchwen = d_up_en_latchwen sync up_en_latchwen goto init_not_en_latchwen; end (*not_en_latchwen*) (************************************************************) automaton retard_wen_h (************************************************************) synclabs: down_wen, up_wen, down_wen_h, up_wen_h; loc init_ret_wen_h : invariant True when True sync up_wen do {x_wen_h := 0} goto A_ret_wen_h; when True sync down_wen do {x_wen_h := 0} goto B_ret_wen_h; loc A_ret_wen_h : invariant x_wen_h <= d_up_wen_h when True sync down_wen do {x_wen_h := 0} goto B_ret_wen_h; when x_wen_h = d_up_wen_h sync up_wen_h goto init_ret_wen_h; loc B_ret_wen_h : invariant x_wen_h <= d_dn_wen_h when True sync up_wen do {x_wen_h := 0} goto A_ret_wen_h; when x_wen_h = d_dn_wen_h sync down_wen_h goto init_ret_wen_h; end (*not_wen_h*) (************************************************************) automaton retard_d_h (************************************************************) synclabs: down_d_0, up_d_0, down_d_h, up_d_h; loc init_ret_d_h : invariant True when True sync up_d_0 do {x_d_h := 0} goto A_ret_d_h; when True sync down_d_0 do {x_d_h := 0} goto B_ret_d_h; loc A_ret_d_h : invariant x_d_h <= d_up_d_h when True sync down_d_0 do {x_d_h := 0} goto B_ret_d_h; when x_d_h = d_up_d_h sync up_d_h goto init_ret_d_h; loc B_ret_d_h : invariant x_d_h <= d_dn_d_h when True sync up_d_0 do {x_d_h := 0} goto A_ret_d_h; when x_d_h = d_dn_d_h sync down_d_h goto init_ret_d_h; end (*not_d_h*) (************************************************************) automaton env (************************************************************) synclabs: up_d_0, down_d_0, up_wen, down_wen, down_ck, up_ck; loc init_env : invariant s <= tHI + tLO - tsetupd when s = tHI + tLO - tsetupd sync up_d_0 goto env1; loc env1 : invariant s <= tHI when s = tHI sync down_ck goto env2; loc env2 : invariant s <= tHI + tLO - tsetupwen when s = tHI + tLO - tsetupwen sync down_wen goto env3; loc env3 : invariant s <= tHI + tLO when s = tHI + tLO sync up_ck goto env3bis; (* env4 modified*) (* RAJOUT PAR ETIENNE ET ROMAIN 2010/09/09*) loc env3bis : invariant s <= 2tHI + 2tLO - tsetupd when s = 2tHI + 2tLO - tsetupd sync down_d_0 goto env4; loc env4 : invariant s <= 2 tHI + tLO when s = 2 tHI + tLO sync down_ck goto env5; loc env5 : invariant s <= 2 tHI + 2 tLO when s = 2 tHI + 2 tLO sync up_ck do {} goto env6; (* end_of_cycle := 1*) loc env6 : invariant True (* when True goto env6; *) end (*env*) (************************************************************) automaton observer (************************************************************) synclabs: qUp, CHECKED_______GOOD, CHECKED_______BAD, CHECKED_______TOO_LATE ; loc waiting : invariant True (* -- when s < 2 tHI + tLO sync up_d_inta do {} goto waiting; *) (* -- when s >= 2 tHI + tLO & s <= tHI + tLO + 109 sync up_d_inta do {x_observer := 0} goto soon_good; *) (* -- when s >= 2 tHI + tLO & s > tHI + tLO + 109 sync up_d_inta do {x_observer := 0} goto soon_bad; *) when s <= 166 sync qUp do {x_observer := 0} goto soon_good; (*-- tHI + tLO + 56*) when s > 166 sync qUp do {x_observer := 0} goto soon_bad; (*-- tHI + tLO + 56*) when s = 2tHI + 2tLO sync CHECKED_______TOO_LATE do {x_observer := 0} goto observer_bad; loc soon_bad : invariant x_observer <= 0 when x_observer = 0 sync CHECKED_______BAD goto observer_bad; loc soon_good : invariant x_observer <= 0 when x_observer = 0 sync CHECKED_______GOOD goto observer_good; loc observer_bad : invariant True loc observer_good : invariant True end (*observer*) (************************************************************) (* Initial state *) (************************************************************) init := (*------------------------------------------------------------*) (* Initial location *) (*------------------------------------------------------------*) & loc[abs_net27] = init_abs_net27 & loc[f2_wela] = e_01_1_wela & loc[not_net13a] = init_not_net13a & loc[reg_net45] = e0d1_U_reg_net45 & loc[reg_d_int] = e0d0_U_reg_d_int & loc[not_en_latchd] = init_not_en_latchd & loc[not_en_latchwen] = init_not_en_latchwen & loc[retard_wen_h] = init_ret_wen_h & loc[retard_d_h] = init_ret_d_h & loc[env] = init_env & loc[observer] = waiting (*------------------------------------------------------------*) (* Initial clock constraints *) (*------------------------------------------------------------*) & s = 0 & x_wela = 0 & x_net13a = 0 & x_net45 = 0 & x_d_int = 0 & x_en_latchd = 0 & x_en_latchwen = 0 & x_wen_h = 0 & x_d_h = 0 (* -- & end_of_cycle = 0 *) (* -- delais pour SP1 (cf. WSEAS06, Fig.5) *) & tsetupd >= 0 & tsetupwen >= 0 (* ---START PI0--- (* & tsetupd = 100 & tsetupwen = 65*) -- -- VALEURS RAPPORT ABDEL -- & tHI = 45 -- & tLO = 65 -- & tsetupd = 96 -- & tsetupwen = 29 -- VALEURS DATASHEET SP1 -- & tHI = 45 -- & tLO = 65 -- & tsetupd = 108 -- & tsetupwen = 48 ---END PI0---*) (* -- CONTRAINTE DE IMITATOR 1 -- & 0 <= d_up_wela -- & 0 <= d_up_en_latchwen -- & d_up_en_latchd < d_dn_net45 + d_dn_net45a + d_up_en_latchwen -- & tLO + d_dn_wen_h < tsetupwen + d_up_en_latchd -- & d_dn_en_latchd < d_dn_net13a + d_dn_wela -- & tLO <= tsetupd -- & d_dn_net45 + d_dn_net45a + d_up_en_latchwen < d_up_d_int + d_up_en_latchd + d_up_d_inta -- & tLO < tsetupwen + d_up_net13a -- & d_up_d_int + d_up_d_inta + d_up_en_latchd < tLO -- & d_dn_net13a + d_dn_wela < tHI -- & d_up_net13a + d_up_wela + tsetupwen < tLO + d_dn_wen_h -- & tLO + d_up_d_h < d_dn_d_int + d_up_en_latchd + d_dn_d_inta + tsetupd -- & d_up_d_int + d_up_d_h + d_up_d_inta < tsetupd + d_dn_en_latchd -- & d_up_net27 + d_dn_net13a + d_up_q_0 + d_dn_wela < tHI + d_up_net13a -- & tsetupwen + d_up_en_latchwen < tLO -- & d_up_d_h < tsetupd -- & tsetupd < tLO + tHI -- & tsetupd + d_dn_net13a < d_up_d_int + d_up_d_inta + d_up_d_h -- & tHI + d_up_en_latchwen < d_dn_wela + d_up_net27 + d_dn_net13a + d_up_q_0 -- & tsetupd + d_dn_net45a + d_dn_net45 + d_dn_wen_h + d_up_wela < tsetupwen + d_up_d_h -- & 0 <= d_dn_en_latchwen -- & tLO + d_dn_wen_h < d_up_net45 + d_up_net45a + tsetupwen + d_up_en_latchwen -- & d_dn_en_latchwen < d_dn_net13a*) ; (************************************************************) (* The end *) (************************************************************) end