Skip to content

Instantly share code, notes, and snippets.

@tmeissner
Created January 5, 2024 16:26
Show Gist options
  • Save tmeissner/7f6d22e1c880c79874fcbfdab0ed7a55 to your computer and use it in GitHub Desktop.
Save tmeissner/7f6d22e1c880c79874fcbfdab0ed7a55 to your computer and use it in GitHub Desktop.
Example to check that each request has to be acked before next request
-- Example to check that each request has to be acked before next request
-- VHDL glue logic
process (clk) is
begin
if rising_edge(clk) then
if (not rst_n) then
req_active <= '0';
elsif (req) then
req_active <= '1';
elsif (ack) then
req_active <= '0';
end if;
end if;
end process;
-- PSL assumption about req and ack inputs
assume always (not rst_n_i -> not req_i);
assume always (req_active -> not req_i);
assume always (req_i -> next not not req_i);
assume always (eot_o and req_active -> next(ack));
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment