Convert VHDL Monitor to PSL Approval

Question

I have an interesting question about PSL approval. Here is the VHDL monitoring process. This is a process dedicated to affirmation and therefore non-synthesizable. This monitor checks the current state of FSM and stores the values ​​of two registers: " input1 " and " reg136 ". Finally, it runs the " assert " assert 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 there a way to translate this monitor into a PSL (Property Specification Language) statement?

IMPORTANT : the registers "input1" and "reg136" can only be read when the state fsm is in state s0 and s22, respectively. Otherwise, the data contained in these registers does not apply to the approved variables "a" and "t34". As a result, the PSL statement must be able to read and store values ​​in the correct fsm states.

Thanks!

Answer 1

In fact, I think I found a way to do this using the prev PSL function.

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

This requires that fsm increment its state register by one per clock cycle or know how many hours it takes to transition from state s0 or s22 to state s85.

Can someone confirm that this will work? I don't have a PSL-ready simulator to test this ...