Commit 31c9bafd authored by Michael Munch's avatar Michael Munch
Browse files

Formal verifaction of latched inputs

parent 9c213426
Pipeline #13957 passed with stage
in 52 seconds
vunit no_double_active_client (vme_cli_arb(rtl))
{
default clock is rising_edge(clk);
assert always not (live_1 and live_2);
assert always not (active_1 and active_2);
}
vunit not_two_busy_client (vme_cli_arb(rtl))
{
default clock is rising_edge(clk);
assert not (p1_busy and p2_busy);
}
-- If the core is busy then we do NOT start new clients
vunit do_not_start_while_busy (vme_cli_arb(rtl))
{
default clock is rising_edge(clk);
assert always {vc_busy = '1'} |-> not start_1 until vc_busy = '0';
assert always {vc_busy = '1'} |-> not start_1 until vc_busy = '0';
}
vunit prefer_other_guys (vme_cli_arb(rtl))
{
default clock is rising_edge(clk);
assert always {start_1} |=> not prefer_1 until start_2;
assert always {start_2} |=> prefer_1 until start_1;
}
vunit we_select_consistently (vme_cli_arb(rtl))
{
default clock is rising_edge(clk);
assert always {p1_go = '1' and p2_go = '1' and not prefer_1 and vc_busy = '0'}
|=> start_2 until active_2;
assert always {p1_go = '1' and p2_go = '1' and prefer_1 and vc_busy = '0'}
|=> start_1 until active_1;
}
vunit data_output_tracks_live_data (vme_cli_arb(rtl))
{
default clock is rising_edge(clk);
assert always {active_1; vc_int_data_strobe = '1'}
|=> p1_int_data_o = vc_int_data_o
until! vc_int_data_strobe = '0' or not live_1;
assert always {active_2; vc_int_data_strobe = '1'}
|=> p2_int_data_o = vc_int_data_o
until! vc_int_data_strobe = '0' or not live_2;
}
-- vunit data_output_tracks_live_data (vme_cli_arb(rtl))
-- {
-- default clock is rising_edge(clk);
-- assert always {active_1 and vc_busy = '1' and vc_int_data_strobe = '1'}
-- |=> next p1_int_data_o_latched = vc_int_data_o;
-- }
vunit arbiter_should_latch_data (vme_cli_arb(rtl))
{
default clock is falling_edge(clk);
assert always {active_1; vc_int_data_strobe = '1'}
|=> eventually! p1_int_data_o_latched = vc_int_data_o;
assert always {active_2; vc_int_data_strobe = '1'}
|=> eventually! p2_int_data_o_latched = vc_int_data_o;
}
vunit p1_signals_are_eventually_sent_to_vme_while_p1_active (vme_cli_arb(rtl))
{
default clock is falling_edge(clk);
assert always {p1_go}
|=> eventually! vc_int_addr = p1_int_addr ;
assert always {p1_go}
|=> eventually! vc_int_data_i = p1_int_data_i ;
assert always {p1_go}
|=> eventually! vc_int_am_i = p1_int_am_i ;
assert always {p1_go}
|=> eventually! vc_int_vme_rw = p1_int_vme_rw ;
assert always {p1_go}
|=> eventually! vc_int_vme_go = p1_int_vme_go ;
assert always {p1_go}
|=> eventually! vc_int_blt_decided = p1_int_blt_decided ;
assert always {p1_go}
|=> eventually! vc_int_berr_ok = p1_int_berr_ok ;
}
vunit p2_signals_are_eventually_sent_to_vme_while_p2_active (vme_cli_arb(rtl))
{
default clock is falling_edge(clk);
assert always {p2_go}
|=> eventually! vc_int_addr = p2_int_addr ;
assert always {p2_go}
|=> eventually! vc_int_data_i = p2_int_data_i ;
assert always {p2_go}
|=> eventually! vc_int_am_i = p2_int_am_i ;
assert always {p2_go}
|=> eventually! vc_int_vme_rw = p2_int_vme_rw ;
assert always {p2_go}
|=> eventually! vc_int_vme_go = p2_int_vme_go ;
assert always {p2_go}
|=> eventually! vc_int_blt_decided = p2_int_blt_decided ;
assert always {p2_go}
|=> eventually! vc_int_berr_ok = p2_int_berr_ok ;
}
......@@ -6,10 +6,9 @@ depth 20
smtbmc z3
[script]
ghdl -fpsl --std=08 -gformal=true vme_pkg.vhd vme_cli_arb.vhd formal_vme_cli_arb.vhd -e vme_cli_arb
ghdl -fpsl --std=08 -gformal=true vme_pkg.vhd vme_cli_arb.vhd -e vme_cli_arb
prep -top vme_cli_arb
[files]
vme_cli_arb.vhd
vme_pkg.vhd
test/formal_vme_cli_arb.vhd
......@@ -10,6 +10,10 @@ use work.vme_pkg.all;
-- to be processed).
entity vme_cli_arb is
generic (
-- To synth formal verification
formal : boolean := true
);
port (
signal clk : in std_logic;
......@@ -22,8 +26,8 @@ entity vme_cli_arb is
signal p1_int_data_strobe : out std_logic := c_DATA_CLEAR;
signal p1_int_go_consumed_strobe : out std_logic := '0';
signal p1_int_blt_decision_strobe : out std_logic := '0';
signal p1_int_err_code : out ERR_CODE := OK;
signal p1_int_err_code : out ERR_CODE := OK;
signal p1_int_addr : in vme_addr_t;
signal p1_int_data_i : in vme_vec_64_t;
signal p1_int_am_i : in am_vec_t;
......@@ -31,22 +35,22 @@ entity vme_cli_arb is
signal p1_int_vme_go : in std_logic;
signal p1_int_blt_decided : in std_logic;
signal p1_int_blt_continue : in std_logic;
signal p1_int_blt_continue : in std_logic;
signal p1_int_berr_ok : in std_logic;
signal p1_go : in std_logic;
-- Signals to/from the second client.
signal p2_busy : out std_logic := '0';
signal p2_int_data_o : out vme_vec_64_t;
signal p2_int_data_strobe : out std_logic := c_DATA_CLEAR;
signal p2_int_go_consumed_strobe : out std_logic := '0';
signal p2_int_blt_decision_strobe : out std_logic := '0';
signal p2_int_err_code : out ERR_CODE := OK;
signal p2_int_err_code : out ERR_CODE := OK;
signal p2_int_addr : in vme_addr_t;
signal p2_int_data_i : in vme_vec_64_t;
signal p2_int_am_i : in am_vec_t;
......@@ -54,11 +58,11 @@ entity vme_cli_arb is
signal p2_int_vme_go : in std_logic;
signal p2_int_blt_decided : in std_logic;
signal p2_int_blt_continue : in std_logic;
signal p2_int_blt_continue : in std_logic;
signal p2_int_berr_ok : in std_logic;
signal p2_go : in std_logic;
signal p2_go : in std_logic;
-- Signals to/from the VME core.
-- Directions inverted relative to the core.
......@@ -69,8 +73,8 @@ entity vme_cli_arb is
signal vc_int_data_strobe : in std_logic := c_DATA_CLEAR;
signal vc_int_go_consumed_strobe : in std_logic := '0';
signal vc_int_blt_decision_strobe : in std_logic := '0';
signal vc_int_err_code : in ERR_CODE := OK;
signal vc_int_err_code : in ERR_CODE := OK;
signal vc_int_addr : out vme_addr_t;
signal vc_int_data_i : out vme_vec_64_t;
signal vc_int_am_i : out am_vec_t;
......@@ -78,7 +82,7 @@ entity vme_cli_arb is
signal vc_int_vme_go : out std_logic;
signal vc_int_blt_decided : out std_logic;
signal vc_int_blt_continue : out std_logic;
signal vc_int_blt_continue : out std_logic;
signal vc_int_berr_ok : out std_logic
......@@ -95,7 +99,7 @@ entity vme_cli_arb is
-- -- Single-cycle strobe:
-- signal int_data_strobe : out std_logic := c_DATA_CLEAR;
);
end entity;
......@@ -131,11 +135,11 @@ architecture rtl of vme_cli_arb is
-- no longer busy?
signal prefer_1 : boolean := false;
signal p1_int_data_o_latched : vme_vec_64_t := (others => '1');
signal p2_int_data_o_latched : vme_vec_64_t := (others => '1');
signal p1_int_data_o_latched : vme_vec_64_t := (others => '0');
signal p2_int_data_o_latched : vme_vec_64_t := (others => '0');
signal p1_int_err_code_latched : ERR_CODE := OK;
signal p2_int_err_code_latched : ERR_CODE := OK;
signal p2_int_err_code_latched : ERR_CODE := OK;
begin
want_1 <= (p1_go = '1' and p2_go = '0') or (p1_go = '1' and prefer_1);
......@@ -148,13 +152,13 @@ begin
-- (Not really needed.)
live_1 <= (active_1 and vc_busy = '1') or start_1;
live_2 <= (active_2 and vc_busy = '1') or start_2;
process (clk)
begin
if (rising_edge(clk)) then
cnt <= cnt + 1;
if (vc_busy = '0') then
active_1 <= false;
active_2 <= false;
......@@ -172,7 +176,7 @@ begin
-- We select on active instead of live, since active is cheaper (comes
-- directly from a flip-flop, instead of logic), and
-- vc_int_data_strobe will not come on the first cycle.
-- vc_int_data_strobe will not come on the first cycle.
if (active_1 and vc_int_data_strobe = '1') then
p1_int_data_o_latched <= vc_int_data_o;
p1_int_err_code_latched <= vc_int_err_code;
......@@ -187,11 +191,11 @@ begin
-- Signals to the VME core are taken from the live client:
-- If no client is live, we (arbitrarily) take the signals from
-- client 2. This does not matter, since the VME core will
-- only react to anything if the 'go' signal is given.
vc_int_addr <= p1_int_addr when live_1 else p2_int_addr;
vc_int_data_i <= p1_int_data_i when live_1 else p2_int_data_i;
vc_int_am_i <= p1_int_am_i when live_1 else p2_int_am_i;
......@@ -206,7 +210,7 @@ begin
-- TODO: All the selects below could use active_1 / active_2 instead
-- of live_1 / live_2, since the signals from the VME core
-- will not happen on the first cycle we are active!
-- Data is passed directly through on the cycle they have been latched.
-- Otherwise, take the latched value:
p1_int_data_o <= vc_int_data_o when (live_1 and vc_int_data_strobe = '1') else
......@@ -235,11 +239,141 @@ begin
p1_busy <= '1' when live_1 else '0';
p2_busy <= '1' when live_2 else '0';
-- assert (always active_1 and vc_int_data_strobe = '1' -> next
-- p1_int_data_o_latched = vc_int_data_o
-- until vc_int_data_strobe = '0' or not active_1) @rising_edge(clk);
FormalG : if Formal generate
-- VHDL helper vars
signal l_data : vme_vec_64_t := (others => '0');
signal l_err_code : ERR_CODE := OK;
begin
-- *_latched output will lack input by one clock cycle.
-- GHDL does not have prev() operator,
-- so latch things here for comparison.
process (clk)
begin
if (rising_edge(clk)) then
l_data <= vc_int_data_o;
l_err_code <= vc_int_err_code;
end if;
end process;
default clock is rising_edge(clk);
-- Two clients may not be active at the same time
not_two_live: assert always not (live_1 and live_2);
not_two_active: assert always not (active_1 and active_2);
not_two_busy: assert not (p1_busy and p2_busy);
-- Don't start clients when VME core is busy
busy_dont_start_1: assert always {vc_busy = '1'} |-> not start_1 until vc_busy = '0';
busy_dont_start_2: assert always {vc_busy = '1'} |-> not start_1 until vc_busy = '0';
-- When we have started client 1 then prefer 2 until it runs
if_start_1_pref_2: assert always {start_1} |=> not prefer_1 until start_2;
if_start_2_pref_1: assert always {start_2} |=> prefer_1 until start_1;
-- If both clients request access then we pick our favourite
pick_pref_client_1: assert always
{p1_go = '1' and p2_go = '1' and not prefer_1 and vc_busy = '0'}
|=> start_2 until active_2;
pick_pref_client_2: assert always
{p1_go = '1' and p2_go = '1' and prefer_1 and vc_busy = '0'}
|=> start_1 until active_1;
-- While client is live it data output tracks live data
live_track_1:
assert always {active_1; vc_int_data_strobe = '1'}
|=> p1_int_data_o = vc_int_data_o
until vc_int_data_strobe = '0' or not live_1;
live_track_2:
assert always {active_2; vc_int_data_strobe = '1'}
|=> p2_int_data_o = vc_int_data_o
until vc_int_data_strobe = '0' or not live_2;
-- If we sent p1_go then the VME core will eventually receive it
p1_vme_addr: assert always {p1_go}
|=> eventually! vc_int_addr = p1_int_addr ;
p1_vme_data_i: assert always {p1_go}
|=> eventually! vc_int_data_i = p1_int_data_i ;
p1_vme_am_i: assert always {p1_go}
|=> eventually! vc_int_am_i = p1_int_am_i ;
p1_vme_rw: assert always {p1_go}
|=> eventually! vc_int_vme_rw = p1_int_vme_rw ;
p1_vme_go: assert always {p1_go}
|=> eventually! vc_int_vme_go = p1_int_vme_go ;
p1_vme_blt_deci: assert always {p1_go}
|=> eventually! vc_int_blt_decided = p1_int_blt_decided ;
p1_vme_blt_cont: assert always {p1_go}
|=> eventually! vc_int_blt_continue = p1_int_blt_continue ;
p1_vme_berr_ok: assert always {p1_go}
|=> eventually! vc_int_berr_ok = p1_int_berr_ok ;
-- If we sent p2_go then the VME core will eventually receive it
p2_vme_addr: assert always {p2_go}
|=> eventually! vc_int_addr = p2_int_addr ;
p2_vme_data_i: assert always {p2_go}
|=> eventually! vc_int_data_i = p2_int_data_i ;
p2_vme_am_i: assert always {p2_go}
|=> eventually! vc_int_am_i = p2_int_am_i ;
p2_vme_rw: assert always {p2_go}
|=> eventually! vc_int_vme_rw = p2_int_vme_rw ;
p2_vme_go: assert always {p2_go}
|=> eventually! vc_int_vme_go = p2_int_vme_go ;
p2_vme_blt_deci: assert always {p2_go}
|=> eventually! vc_int_blt_decided = p2_int_blt_decided ;
p2_vme_blt_cont: assert always {p2_go}
|=> eventually! vc_int_blt_continue = p2_int_blt_continue ;
p2_vme_berr_ok: assert always {p2_go}
|=> eventually! vc_int_berr_ok = p2_int_berr_ok ;
-- Data strobes are routed to live client
p1_get_d_strobe: assert always {live_1}
|=> p1_int_data_strobe = vc_int_data_strobe until not live_1;
p2_get_d_strobe: assert always {live_2}
|=> p2_int_data_strobe = vc_int_data_strobe until not live_2;
-- Go strobes are routed to live client
p1_get_go_strobe: assert always {live_1}
|=> p1_int_go_consumed_strobe = vc_int_go_consumed_strobe until not live_1;
p2_get_go_strobe: assert always {live_2}
|=> p2_int_go_consumed_strobe = vc_int_go_consumed_strobe until not live_2;
-- BLT decision strobes are routed to live client
p1_get_blt_strobe: assert always {live_1}
|=> p1_int_blt_decision_strobe = vc_int_blt_decision_strobe until not live_1;
p2_get_blt_strobe: assert always {live_2}
|=> p2_int_blt_decision_strobe = vc_int_blt_decision_strobe until not live_2;
-- Latched data tracks input while active and strobed
p1_tracks_data: assert always
{active_1 and vc_busy = '1' and vc_int_data_strobe = '1'}
|=> p1_int_data_o_latched = l_data
until vc_int_data_strobe = '0' or not active_1;
p2_tracks_data: assert always
{active_2 and vc_busy = '1' and vc_int_data_strobe = '1'}
|=> p2_int_data_o_latched = l_data
until vc_int_data_strobe = '0' or not active_2;
-- Latched error tracks input while active and strobed
p1_tracks_err: assert always
{active_1 and vc_busy = '1' and vc_int_data_strobe = '1'}
|=> p1_int_err_code_latched = l_err_code
until vc_int_data_strobe = '0' or not active_1;
p2_tracks_err: assert always
{active_2 and vc_busy = '1' and vc_int_data_strobe = '1'}
|=> p2_int_err_code_latched = l_err_code
until vc_int_data_strobe = '0' or not active_2;
end generate FormalG;
end architecture;
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment