Commit 1e148181 authored by Michael Munch's avatar Michael Munch
Browse files

Hide client arb PSL

parent b9dbd666
......@@ -261,118 +261,118 @@ begin
-- psl 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);
-- -- Two clients may not be active at the same time
-- psl not_two_live: assert always not (live_1 and live_2);
-- psl not_two_active: assert always not (active_1 and active_2);
-- psl 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';
-- -- Don't start clients when VME core is busy
-- psl busy_dont_start_1: assert always {vc_busy = '1'} |-> not start_1 until vc_busy = '0';
-- psl 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;
-- -- When we have started client 1 then prefer 2 until it runs
-- psl if_start_1_pref_2: assert always {start_1} |=> not prefer_1 until start_2;
-- psl 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;
-- -- If both clients request access then we pick our favourite
-- psl 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;
-- psl 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
-- psl 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;
-- psl 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
-- psl p1_vme_addr: assert always {p1_go}
-- |=> eventually! vc_int_addr = p1_int_addr ;
-- psl p1_vme_data_i: assert always {p1_go}
-- |=> eventually! vc_int_data_i = p1_int_data_i ;
-- psl p1_vme_am_i: assert always {p1_go}
-- |=> eventually! vc_int_am_i = p1_int_am_i ;
-- psl p1_vme_rw: assert always {p1_go}
-- |=> eventually! vc_int_vme_rw = p1_int_vme_rw ;
-- psl p1_vme_go: assert always {p1_go}
-- |=> eventually! vc_int_vme_go = p1_int_vme_go ;
-- psl p1_vme_blt_deci: assert always {p1_go}
-- |=> eventually! vc_int_blt_decided = p1_int_blt_decided ;
-- psl p1_vme_blt_cont: assert always {p1_go}
-- |=> eventually! vc_int_blt_continue = p1_int_blt_continue ;
-- psl 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
-- psl p2_vme_addr: assert always {p2_go}
-- |=> eventually! vc_int_addr = p2_int_addr ;
-- psl p2_vme_data_i: assert always {p2_go}
-- |=> eventually! vc_int_data_i = p2_int_data_i ;
-- psl p2_vme_am_i: assert always {p2_go}
-- |=> eventually! vc_int_am_i = p2_int_am_i ;
-- psl p2_vme_rw: assert always {p2_go}
-- |=> eventually! vc_int_vme_rw = p2_int_vme_rw ;
-- psl p2_vme_go: assert always {p2_go}
-- |=> eventually! vc_int_vme_go = p2_int_vme_go ;
-- psl p2_vme_blt_deci: assert always {p2_go}
-- |=> eventually! vc_int_blt_decided = p2_int_blt_decided ;
-- psl p2_vme_blt_cont: assert always {p2_go}
-- |=> eventually! vc_int_blt_continue = p2_int_blt_continue ;
-- psl p2_vme_berr_ok: assert always {p2_go}
-- |=> eventually! vc_int_berr_ok = p2_int_berr_ok ;
-- -- Data strobes are routed to live client
-- psl p1_get_d_strobe: assert always {live_1}
-- |=> p1_int_data_strobe = vc_int_data_strobe until not live_1;
-- psl 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
-- psl p1_get_go_strobe: assert always {live_1}
-- |=> p1_int_go_consumed_strobe = vc_int_go_consumed_strobe until not live_1;
-- psl 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
-- psl p1_get_blt_strobe: assert always {live_1}
-- |=> p1_int_blt_decision_strobe = vc_int_blt_decision_strobe until not live_1;
-- psl 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;
-- -- Latched data tracks input while active and strobed
-- psl 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;
-- psl 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
-- psl 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;
-- psl 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