Hi,
I’m getting an assertion fail for a simple rising edge D flip flop in behavior2. I’ve only just started in SystemVerliog and assertions and I’m not sure why behavior2 I’m getting “Check ‘sva/inst_dff_property_suite/a_behavior2’ unchanged, still fails within 1 cycles from reset.”
library IEEE;
use IEEE.std_logic_1164.all;
entity dff is
port(
clk : in std_ulogic;
d_i : in std_ulogic;
q_o : out std_ulogic
);
end dff;
architecture rtl of dff is
begin
process is
begin
wait until clk'event and clk = '1';
q_o <= d_i;
end process;
end rtl;
In reply to Ehm:
Below is an image from my SVA Handbook that explains the $past. Because $pastgets the value of a previous clock cycle(s), you need to modify the assertion to evaluate it when $past(expression) has the provlue for that expression. Thus, I would mofiy the properties as follows:
##1 q_o == $past(d_i);
##2 q_o == $past(d_i,2);
Keep in mind that every leading clocking event you have an attempt. Thus,
##1 q_o == $past(d_i); // cycle 1 attempt will evaluate the q_o == $past(d_i) one cycle later (at cycle 2). cyele 2 attempt will evaluate at q_o == $past(d_i) at cycle 3, and so on.
##2 q_o == $past(d_i,2); // cycle 1 attempt will do the same 2 cycles later.
If you need to evaluate the value after reset time, then you'll need something like
apD_reset_async: assert property(@ (posedge clk) $fell(reset) |-> q_o ==1'b0 ); // reset is active hi, async reset.
apD_reset_sync: assert property(@ (posedge clk) $fell(reset) |=> q_o ==1'b0 ); // reset is active hi, synchronous reset.