Commit 5dfdd5b5 authored by Michael Munch's avatar Michael Munch
Browse files

Added formal verifaction

parent 1e3a72ff
vunit_out
\ No newline at end of file
vunit_out
vme_cli_arb
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 ;
}
[options]
mode bmc
depth 20
[engines]
smtbmc
[script]
ghdl -fpsl --std=08 -gformal=true vme_pkg.vhd vme_cli_arb.vhd formal_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
......@@ -111,6 +111,7 @@ architecture rtl of vme_cli_arb is
-- In case we are not busy, which client would we like to
-- make active (if any).
signal cnt : integer range 0 to 256:= 0;
signal want_1 : boolean;
signal want_2 : boolean;
......@@ -130,8 +131,8 @@ 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;
signal p2_int_data_o_latched : vme_vec_64_t;
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_err_code_latched : ERR_CODE := OK;
signal p2_int_err_code_latched : ERR_CODE := OK;
......@@ -152,6 +153,8 @@ begin
begin
if (rising_edge(clk)) then
cnt <= cnt + 1;
if (vc_busy = '0') then
active_1 <= false;
active_2 <= false;
......@@ -232,6 +235,11 @@ 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);
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