Commit b9dbd666 authored by Michael Munch's avatar Michael Munch
Browse files

Hide PSL in bus arb

parent fc8fcde4
......@@ -165,102 +165,95 @@ begin
FormalG : if Formal generate
begin
process (clk) begin
if (rising_edge(clk)) then
null;
end if;
end process;
-- psl default clock is rising_edge(clk);
stay_in_idle_until_br_received:
assert always (state = IDLE and vme_br_n_i = "1111")
|=> state = IDLE until vme_br_n_i /= "1111";
-- psl stay_in_idle_until_br_received:
-- assert always (state = IDLE and vme_br_n_i = "1111")
-- |=> state = IDLE until vme_br_n_i /= "1111";
assert always (state = IDLE and vme_br_n_i /= "1111")
|=> state = FIRE_BUS_GRANT;
if_single_br_on_0_received_accept_it:
assert always (state = FIRE_BUS_GRANT and vme_br_n_i = "1110")
|=> vme_bgout_n_o = "1110";
if_single_br_on_1_received_accept_it:
assert always (state = FIRE_BUS_GRANT and vme_br_n_i = "1101")
|=> vme_bgout_n_o = "1101";
if_single_br_on_2_received_accept_it:
assert always (state = FIRE_BUS_GRANT and vme_br_n_i = "1011")
|=> vme_bgout_n_o = "1011";
if_single_br_on_3_received_accept_it:
assert always (state = FIRE_BUS_GRANT and vme_br_n_i = "0111")
|=> vme_bgout_n_o = "0111";
if_br_received_on_both_3_and_0_pick_3:
assert always (state = FIRE_BUS_GRANT and vme_br_n_i = "0110")
|=> vme_bgout_n_o = "0111";
if_br_received_then_next_state_is_bbsy_wait:
assert always (state = FIRE_BUS_GRANT and vme_br_n_i /= "1111")
|=> state = BBSY_ASSERT_WAIT;
when_waiting_for_bbsy_wait_until_bbsy_received:
assert always (state = BBSY_ASSERT_WAIT and vme_bbsy_n_i = '1')
|=> state = BBSY_ASSERT_WAIT until vme_bbsy_n_i = '0' or n_wait = 0;
when_waiting_for_bbsy_time_out_returns_to_idle:
assert always (state = BBSY_ASSERT_WAIT and vme_bbsy_n_i = '1' and n_wait = 0)
|=> state = IDLE;
when_waiting_for_bbsy_and_it_assert_then_go_to_bus_granted:
assert always (state = BBSY_ASSERT_WAIT and vme_bbsy_n_i = '0' and n_wait > 0)
|=> state = BUS_GRANTED;
bus_granted_rescind_bgout:
assert always (state = BUS_GRANTED)
|=> vme_bgout_n_o = "1111";
if_bus_grant_0_and_req_on_1_then_bus_clear:
assert always (state = BUS_GRANTED and granted = 0
and vme_br_n_i = "1101" and vme_bbsy_n_i = '0')
|=> vme_bclr_n_o = '0';
if_bus_granted_to_1_then_requested_set_to_1:
assert always (state = BUS_GRANTED and granted = 0
and vme_br_n_i = "1101" and vme_bbsy_n_i = '0')
|=> requested = 1;
if_bus_grant_0_and_req_on_0_then_bus_clear:
assert always (state = BUS_GRANTED and granted = 0
and vme_br_n_i = "1110" and vme_bbsy_n_i = '0')
|=> vme_bclr_n_o = '0';
if_bus_grant_1_and_req_on_0_then_no_clear:
assert always (state = BUS_GRANTED and granted = 1
and vme_br_n_i = "1110" and vme_bbsy_n_i = '0')
|=> vme_bclr_n_o = '1';
if_bus_grant_3_and_req_on_3_then_bus_clear:
assert always (state = BUS_GRANTED and granted = 3
and vme_br_n_i = "0111" and vme_bbsy_n_i = '0')
|=> vme_bclr_n_o = '0' and state = BBSY_DEASSERT_WAIT;
remain_in_bbsy_deassert_atleast_4_cycles:
assert always (state = BBSY_DEASSERT_WAIT and n_bbsy_high = 0)
|=> state = BBSY_DEASSERT_WAIT until n_bbsy_high = c_N_BBSY_HIGH;
if_bus_willingly_released_go_to_cooldown:
assert always (state = BUS_GRANTED and vme_bbsy_n_i = '1')
|=> state = COOLDOWN and n_wait = c_N_BBSY_HIGH;
when_in_cool_down_stay_n_wait_cycles:
assert always (state = COOLDOWN)
|=> state = COOLDOWN until n_wait = 0;
move_from_cooldown_to_idle:
assert always (state = COOLDOWN and n_wait = 0)
|=> state = IDLE;
-- psl assert always (state = IDLE and vme_br_n_i /= "1111")
-- |=> state = FIRE_BUS_GRANT;
-- psl if_single_br_on_0_received_accept_it:
-- assert always (state = FIRE_BUS_GRANT and vme_br_n_i = "1110")
-- |=> vme_bgout_n_o = "1110";
-- psl if_single_br_on_1_received_accept_it:
-- assert always (state = FIRE_BUS_GRANT and vme_br_n_i = "1101")
-- |=> vme_bgout_n_o = "1101";
-- psl if_single_br_on_2_received_accept_it:
-- assert always (state = FIRE_BUS_GRANT and vme_br_n_i = "1011")
-- |=> vme_bgout_n_o = "1011";
-- psl if_single_br_on_3_received_accept_it:
-- assert always (state = FIRE_BUS_GRANT and vme_br_n_i = "0111")
-- |=> vme_bgout_n_o = "0111";
-- psl if_br_received_on_both_3_and_0_pick_3:
-- assert always (state = FIRE_BUS_GRANT and vme_br_n_i = "0110")
-- |=> vme_bgout_n_o = "0111";
-- psl if_br_received_then_next_state_is_bbsy_wait:
-- assert always (state = FIRE_BUS_GRANT and vme_br_n_i /= "1111")
-- |=> state = BBSY_ASSERT_WAIT;
-- psl when_waiting_for_bbsy_wait_until_bbsy_received:
-- assert always (state = BBSY_ASSERT_WAIT and vme_bbsy_n_i = '1')
-- |=> state = BBSY_ASSERT_WAIT until vme_bbsy_n_i = '0' or n_wait = 0;
-- psl when_waiting_for_bbsy_time_out_returns_to_idle:
-- assert always (state = BBSY_ASSERT_WAIT and vme_bbsy_n_i = '1' and n_wait = 0)
-- |=> state = IDLE;
-- psl when_waiting_for_bbsy_and_it_assert_then_go_to_bus_granted:
-- assert always (state = BBSY_ASSERT_WAIT and vme_bbsy_n_i = '0' and n_wait > 0)
-- |=> state = BUS_GRANTED;
-- psl bus_granted_rescind_bgout:
-- assert always (state = BUS_GRANTED)
-- |=> vme_bgout_n_o = "1111";
-- psl if_bus_grant_0_and_req_on_1_then_bus_clear:
-- assert always (state = BUS_GRANTED and granted = 0
-- and vme_br_n_i = "1101" and vme_bbsy_n_i = '0')
-- |=> vme_bclr_n_o = '0';
-- psl if_bus_granted_to_1_then_requested_set_to_1:
-- assert always (state = BUS_GRANTED and granted = 0
-- and vme_br_n_i = "1101" and vme_bbsy_n_i = '0')
-- |=> requested = 1;
-- psl if_bus_grant_0_and_req_on_0_then_bus_clear:
-- assert always (state = BUS_GRANTED and granted = 0
-- and vme_br_n_i = "1110" and vme_bbsy_n_i = '0')
-- |=> vme_bclr_n_o = '0';
-- psl if_bus_grant_1_and_req_on_0_then_no_clear:
-- assert always (state = BUS_GRANTED and granted = 1
-- and vme_br_n_i = "1110" and vme_bbsy_n_i = '0')
-- |=> vme_bclr_n_o = '1';
-- psl if_bus_grant_3_and_req_on_3_then_bus_clear:
-- assert always (state = BUS_GRANTED and granted = 3
-- and vme_br_n_i = "0111" and vme_bbsy_n_i = '0')
-- |=> vme_bclr_n_o = '0' and state = BBSY_DEASSERT_WAIT;
-- psl remain_in_bbsy_deassert_atleast_4_cycles:
-- assert always (state = BBSY_DEASSERT_WAIT and n_bbsy_high = 0)
-- |=> state = BBSY_DEASSERT_WAIT until n_bbsy_high = c_N_BBSY_HIGH;
-- psl if_bus_willingly_released_go_to_cooldown:
-- assert always (state = BUS_GRANTED and vme_bbsy_n_i = '1')
-- |=> state = COOLDOWN and n_wait = c_N_BBSY_HIGH;
-- psl when_in_cool_down_stay_n_wait_cycles:
-- assert always (state = COOLDOWN)
-- |=> state = COOLDOWN until n_wait = 0;
-- psl move_from_cooldown_to_idle:
-- assert always (state = COOLDOWN and n_wait = 0)
-- |=> state = IDLE;
end generate FormalG;
......
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