Translating a VHDL monitor into a PSL assertion

Question

Hello,

I have an interesting question about PSL assertion. Here is a VHDL monitor process. It is a process dedicated to an assertion, and thus a non-synthesizable one. This monitor checks the current FSM state and stores the values of two registers: "input1" and "reg136". Finally, it triggers an "assert" statement to compare the values of these registers.

process (clk)
  variable var_a : signed(7 downto 0);
  variable var_b : signed(7 downto 0);
begin
  if (rising_edge(clk)) then
    case state is
      when s0 =>
        var_a := signed(input1);
      when s22 =>
        var_t34 := signed(reg136);
      when s85 =>
        assert (var_t34 < var_a)
          report "Assertion xxx failed :
                            (t34 < a)";
    end case;
  end if;
end process;

Question is: is there a way to translate this monitor into a PSL (Property Specification Language) assertion ?

IMPORTANT: the registers "input1" and "reg136" can only be read when the fsm state is at state s0 and s22 respectively. Otherwise, the data contained in these registers does not belong to the asserted variables "a" and "t34". As a result, a PSL statement wouls need a way to read and store the values on the right fsm states.

Thank you !

Answer 1

Actually, I think I found a way to do that using the prev PSL function.

assert always (state = s85) -> (prev(reg136, 85-22) < prev(input1, 85-0)) @rising_edge(clk)

It requires the fsm to increment its state register by one on each clock cycle or to know how many clock cycles are needed to go from state s0 or s22 to state s85.

Can someone confirm that this would work ? I do not have a PSL-ready simulator to check this...