Example to check that each request has to be acked before next request

test.vhd

-- 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));