Commit 68a6a144 authored by Michael Munch's avatar Michael Munch
Browse files

Prepared PSL for data bus

parent 1e148181
Pipeline #15885 passed with stage
in 33 seconds
......@@ -12,11 +12,6 @@ vunit berr_testing (vme_data_bus(rtl))
{
-- If BERR* goes low when waiting for DTACK*
-- then return to IDLE.
when_berr_fires_then_we_go_idle:
assert always {l_berr_ok = '1' and state = DTACK_LOW_WAIT
and vme_berr_n_i = '0'}
|=> state = IDLE;
when_berr_fires_then_ds_and_as_is_rescinded:
assert always {state = DTACK_LOW_WAIT and vme_berr_n_i = '0'}
|-> vme_ds_n_o = "11" and vme_as_n_o = '0';
......
......@@ -237,7 +237,6 @@ architecture rtl of vme_data_bus is
signal l_am : am_vec_t;
signal l_addr_mode : addr_type_t;
signal l_transfer_mode : transfer_type_t;
signal l_berr_ok : std_logic;
-- Latched data
-- If READ_OP it stores the data read from slave.
......@@ -704,176 +703,170 @@ begin
end process;
-- psl default clock is rising_edge(clk);
restrict {{vme_iack_n_i = '1' and vme_berr_n_i = '1'}[+]};
-- Check that client input is latched
when_go_addr_is_latched:
assert always {int_vme_go = '1'
and transfer_mode /= TRANSFER_ERR
and addr_mode /= ADDR_ERR}
|=> l_addr = f_addr until busy = '0';
when_go_am_is_latched:
assert always {int_vme_go = '1'
and transfer_mode /= TRANSFER_ERR
and addr_mode /= ADDR_ERR}
|=> l_am = f_am until busy = '0';
when_go_berr_ok_is_latched:
assert always {int_vme_go = '1'
and transfer_mode /= TRANSFER_ERR
and addr_mode /= ADDR_ERR}
|=> l_berr_ok = f_berr_ok until busy = '0';
when_go_rw_is_latched:
assert always {int_vme_go = '1'
and transfer_mode /= TRANSFER_ERR
and addr_mode /= ADDR_ERR}
|=> l_rw = f_vme_rw until busy = '0';
-- We only check data next cycle.
-- This might be relatched
when_go_data_is_latch:
assert always {state = IDLE and int_vme_go = '1'
and transfer_mode /= TRANSFER_ERR
and addr_mode /= ADDR_ERR}
|=> l_data = f_data;
-- Maintain BUSY until back in IDLE
core_is_busy_until_idle:
assert always {state = IDLE; int_vme_go = '1'
and transfer_mode /= TRANSFER_ERR
and addr_mode /= ADDR_ERR}
|=> busy = '1' until state = IDLE;
when_unsupported_addr_mode_issue_error_code:
assert always {state = IDLE and int_vme_go = '1' and addr_mode = ADDR_ERR}
|=> int_err_code = c_ERR_ADDR_MODE
and state = IDLE_DELAY;
when_unsupported_transfer_mode_issue_error_code:
assert always {state = IDLE and int_vme_go = '1'
and transfer_mode = TRANSFER_ERR
and addr_mode /= ADDR_ERR}
|=> int_err_code = c_ERR_TRANSFER_MODE
and state = IDLE_DELAY;
-- If DTACK* is LOW after AS_DELAY,
-- then we must wait for data lines to clear.
core_will_not_start_until_dtack_high:
assert always {vme_dtack_n_i = '0' and state = AS_DELAY and n_wait=0}
|=> state = DTACK_HIGH_WAIT until vme_dtack_n_i = '1';
-- We maintain go_consumed high until end of AS_DELAY
go_consumed_is_signalled_until_as_delay:
assert always {state = IDLE and int_vme_go = '1'}
|=> int_go_consumed_strobe = '1' until state /= AS_DELAY;
-- Don't fire AS* during AS_DELAY
addr_strobe_are_not_fired_during_as_delay:
assert always {state = AS_DELAY}
|=> vme_as_n_o = '1' and vme_as_n_dir = c_PIN_IN
until state /= AS_DELAY;
-- AS* fires after we leave AS_DELAY
addr_strobe_are_fired_after_as_delay:
assert always {state = AS_DELAY and n_wait = 0}
|=> vme_as_n_o = '0' and vme_as_n_dir = c_PIN_OUT;
-- AS* fires after we leave AS_DELAY
if_dtack_is_asserted_in_as_then_we_wait_until_deasserted:
assert always {state = AS_DELAY and n_wait = 0 and vme_dtack_n_i = '0'}
|=> state = DTACK_HIGH_WAIT and vme_ds_n_o = "11"
until vme_dtack_n_i = '1';
-- Don't fire DS* during AS_DELAY
data_strobes_are_not_fired_during_as_delay:
assert always {state = AS_DELAY}
|=> vme_ds_n_o = "11" and vme_ds_n_dir = c_PIN_IN
until state /= AS_DELAY;
data_strobe_are_fired_with_as_when_data_placed:
assert always {vme_dtack_n_i = '1' and
state = AS_DELAY and l_rw = c_VME_WRITE
and data_placed = '1' and n_wait = 0}
|=> vme_ds_n_o = "00";
-- If writing and waiting for DTACK* HIGH,
-- then data is placed when satisfied.
when_writing_and_dtack_fires_place_data:
assert always {l_transfer_mode = SINGLE
and l_rw = c_VME_WRITE
and state = DTACK_HIGH_WAIT; vme_dtack_n_i = '1'}
|=> vme_data_o = l_data(31 downto 0);
-- If IDLE and GO given
-- and data lines are free (DTACK* = 1)
-- and we are writing.
-- Then place low 32 bits immideately
when_writing_and_dtack_is_high_then_data_is_placed:
assert always {int_vme_go = '1' and state = IDLE
and int_vme_rw = c_VME_WRITE and vme_dtack_n_i = '1'
and int_am_i = c_AM_A24_DATA}
|=> vme_data_o = l_data(31 downto 0)
until state = DTACK_LOW_WAIT or state = IDLE;
-- When writing MBLT the data will be placed on the bus
mblt_writing_data_is_placed_on_bus:
assert always {state = DTACK_HIGH_WAIT and l_transfer_mode = MBLT
and first_cycle = '1' and vme_dtack_n_i = '1'
and l_rw = c_VME_WRITE}
|=> vme_data_o = l_data(31 downto 0)
and vme_addr_o = l_data(63 downto 32);
-- When writing MBLT the data latched during BLT_WRITE_WAIT
-- is written to both addr and data pins
mblt_writing_data_is_placed_on_bus_second_time:
assert always {state = DTACK_HIGH_WAIT and l_transfer_mode = MBLT
and first_cycle = '0' and vme_dtack_n_i = '1'
and l_rw = c_VME_WRITE and f_blt_cycle > 0}
|=> vme_data_o = f_blt_data(31 downto 0)
and vme_addr_o = f_blt_data(63 downto 32);
-- If stopping BLT write transaction,
-- then return to IDLE
return_to_idle_if_stopping_blt_write:
assert always {state = BLT_WRITE_WAIT
and int_blt_decided = '1' and int_blt_continue = '0'}
|=> state = IDLE;
-- If stopping BLT read transaction,
-- then return to IDLE
return_to_idle_if_stopping_blt_read:
assert always {state = BLT_READ_WAIT
and int_blt_decided = '1' and int_blt_continue = '0'}
|=> state = IDLE;
-- When latching 32 or 16 bit data,
-- then low 32 bits are from data lines
-- and high 32 bits are set to 0.
data_is_latched_when_stable:
assert always {state = LATCH_DATA and n_wait = 0
and f_latch_data = f_latch_data2 and l_transfer_mode /= MBLT}
|-> l_data(31 downto 0) = f_latch_data(31 downto 0)
and l_data(63 downto 32) = "00000000000000000000000000000000";
-- When latching 64 bit data,
-- then low 32 bits are from data lines
-- and high 32 bits are from addr lines.
mblt_data_is_latched_when_stable:
assert always {state = LATCH_DATA
and f_latch_data = f_latch_data2 and l_transfer_mode = MBLT;
n_wait = 0}
|-> l_data(31 downto 0) = f_latch_data(31 downto 0)
and l_data(63 downto 32) = f_latch_data(63 downto 32);
-- psl restrict {{vme_iack_n_i = '1' and vme_berr_n_i = '1'}[+]};
-- -- Check that client input is latched
-- psl when_go_addr_is_latched:
-- assert always {int_vme_go = '1'
-- and transfer_mode /= TRANSFER_ERR
-- and addr_mode /= ADDR_ERR}
-- |=> l_addr = f_addr until busy = '0';
-- psl when_go_am_is_latched:
-- assert always {int_vme_go = '1'
-- and transfer_mode /= TRANSFER_ERR
-- and addr_mode /= ADDR_ERR}
-- |=> l_am = f_am until busy = '0';
-- psl when_go_rw_is_latched:
-- assert always {int_vme_go = '1'
-- and transfer_mode /= TRANSFER_ERR
-- and addr_mode /= ADDR_ERR}
-- |=> l_rw = f_vme_rw until busy = '0';
-- -- We only check data next cycle.
-- -- This might be relatched
-- psl when_go_data_is_latch:
-- assert always {state = IDLE and int_vme_go = '1'
-- and transfer_mode /= TRANSFER_ERR
-- and addr_mode /= ADDR_ERR}
-- |=> l_data = f_data;
-- -- Maintain BUSY until back in IDLE
-- psl core_is_busy_until_idle:
-- assert always {state = IDLE; int_vme_go = '1'
-- and transfer_mode /= TRANSFER_ERR
-- and addr_mode /= ADDR_ERR}
-- |=> busy = '1' until state = IDLE;
-- psl when_unsupported_addr_mode_issue_error_code:
-- assert always {state = IDLE and int_vme_go = '1' and addr_mode = ADDR_ERR}
-- |=> int_err_code = c_ERR_ADDR_MODE
-- and state = IDLE_DELAY;
-- psl when_unsupported_transfer_mode_issue_error_code:
-- assert always {state = IDLE and int_vme_go = '1'
-- and transfer_mode = TRANSFER_ERR
-- and addr_mode /= ADDR_ERR}
-- |=> int_err_code = c_ERR_TRANSFER_MODE
-- and state = IDLE_DELAY;
-- -- If DTACK* is LOW after AS_DELAY,
-- -- then we must wait for data lines to clear.
-- psl core_will_not_start_until_dtack_high:
-- assert always {vme_dtack_n_i = '0' and state = AS_DELAY and n_wait=0}
-- |=> state = DTACK_HIGH_WAIT until vme_dtack_n_i = '1';
-- -- We maintain go_consumed high until end of AS_DELAY
-- psl go_consumed_is_signalled_until_as_delay:
-- assert always {state = IDLE and int_vme_go = '1'}
-- |=> int_go_consumed_strobe = '1' until state /= AS_DELAY;
-- -- Don't fire AS* during AS_DELAY
-- psl addr_strobe_are_not_fired_during_as_delay:
-- assert always {state = AS_DELAY}
-- |=> vme_as_n_o = '1' and vme_as_n_dir = c_PIN_IN
-- until state /= AS_DELAY;
-- -- AS* fires after we leave AS_DELAY
-- psl addr_strobe_are_fired_after_as_delay:
-- assert always {state = AS_DELAY and n_wait = 0}
-- |=> vme_as_n_o = '0' and vme_as_n_dir = c_PIN_OUT;
-- -- AS* fires after we leave AS_DELAY
-- psl if_dtack_is_asserted_in_as_then_we_wait_until_deasserted:
-- assert always {state = AS_DELAY and n_wait = 0 and vme_dtack_n_i = '0'}
-- |=> state = DTACK_HIGH_WAIT and vme_ds_n_o = "11"
-- until vme_dtack_n_i = '1';
-- -- Don't fire DS* during AS_DELAY
-- psl data_strobes_are_not_fired_during_as_delay:
-- assert always {state = AS_DELAY}
-- |=> vme_ds_n_o = "11" and vme_ds_n_dir = c_PIN_IN
-- until state /= AS_DELAY;
-- psl data_strobe_are_fired_with_as_when_data_placed:
-- assert always {vme_dtack_n_i = '1' and
-- state = AS_DELAY and l_rw = c_VME_WRITE
-- and data_placed = '1' and n_wait = 0}
-- |=> vme_ds_n_o = "00";
-- -- If writing and waiting for DTACK* HIGH,
-- -- then data is placed when satisfied.
-- psl when_writing_and_dtack_fires_place_data:
-- assert always {l_transfer_mode = SINGLE
-- and l_rw = c_VME_WRITE
-- and state = DTACK_HIGH_WAIT; vme_dtack_n_i = '1'}
-- |=> vme_data_o = l_data(31 downto 0);
-- -- If IDLE and GO given
-- -- and data lines are free (DTACK* = 1)
-- -- and we are writing.
-- -- Then place low 32 bits immideately
-- psl when_writing_and_dtack_is_high_then_data_is_placed:
-- assert always {int_vme_go = '1' and state = IDLE
-- and int_vme_rw = c_VME_WRITE and vme_dtack_n_i = '1'
-- and int_am_i = c_AM_A24_DATA}
-- |=> vme_data_o = l_data(31 downto 0)
-- until state = DTACK_LOW_WAIT or state = IDLE;
-- -- When writing MBLT the data will be placed on the bus
-- psl mblt_writing_data_is_placed_on_bus:
-- assert always {state = DTACK_HIGH_WAIT and l_transfer_mode = MBLT
-- and first_cycle = '1' and vme_dtack_n_i = '1'
-- and l_rw = c_VME_WRITE}
-- |=> vme_data_o = l_data(31 downto 0)
-- and vme_addr_o = l_data(63 downto 32);
-- -- When writing MBLT the data latched during BLT_WRITE_WAIT
-- -- is written to both addr and data pins
-- psl mblt_writing_data_is_placed_on_bus_second_time:
-- assert always {state = DTACK_HIGH_WAIT and l_transfer_mode = MBLT
-- and first_cycle = '0' and vme_dtack_n_i = '1'
-- and l_rw = c_VME_WRITE and f_blt_cycle > 0}
-- |=> vme_data_o = f_blt_data(31 downto 0)
-- and vme_addr_o = f_blt_data(63 downto 32);
-- -- If stopping BLT write transaction,
-- -- then return to IDLE
-- psl return_to_idle_if_stopping_blt_write:
-- assert always {state = BLT_WRITE_WAIT
-- and int_blt_decided = '1' and int_blt_continue = '0'}
-- |=> state = IDLE;
-- -- If stopping BLT read transaction,
-- -- then return to IDLE
-- psl return_to_idle_if_stopping_blt_read:
-- assert always {state = BLT_READ_WAIT
-- and int_blt_decided = '1' and int_blt_continue = '0'}
-- |=> state = IDLE;
-- -- When latching 32 or 16 bit data,
-- -- then low 32 bits are from data lines
-- -- and high 32 bits are set to 0.
-- psl data_is_latched_when_stable:
-- assert always {state = LATCH_DATA and n_wait = 0
-- and f_latch_data = f_latch_data2 and l_transfer_mode /= MBLT}
-- |-> l_data(31 downto 0) = f_latch_data(31 downto 0)
-- and l_data(63 downto 32) = "00000000000000000000000000000000";
-- -- When latching 64 bit data,
-- -- then low 32 bits are from data lines
-- -- and high 32 bits are from addr lines.
-- psl mblt_data_is_latched_when_stable:
-- assert always {state = LATCH_DATA
-- and f_latch_data = f_latch_data2 and l_transfer_mode = MBLT;
-- n_wait = 0}
-- |-> l_data(31 downto 0) = f_latch_data(31 downto 0)
-- and l_data(63 downto 32) = f_latch_data(63 downto 32);
-- If BLT write is continued,
-- then new data is latched.
if_continueing_blt_write_then_latch_new_data:
assert always {state = BLT_WRITE_WAIT
and int_blt_decided = '1' and int_blt_continue = '1'}
|=> l_data = f_blt_data;
-- -- If BLT write is continued,
-- -- then new data is latched.
-- psl if_continueing_blt_write_then_latch_new_data:
-- assert always {state = BLT_WRITE_WAIT
-- and int_blt_decided = '1' and int_blt_continue = '1'}
-- |=> l_data = f_blt_data;
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