D-Flip Flop Assertion Fail

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.”

Assertion code:


module dff_property_suite (clk,d_i,q_o);

input logic clk;
input logic d_i;
input logic q_o;

// define properties 

property behavior1;
  q_o == $past(d_i);
endproperty

property behavior2;
  q_o == $past(d_i,2);
endproperty

// tell the tool what properties to check

a_behavior1: assert property (@(posedge clk) behavior1);
a_behavior2: assert property (@(posedge clk) behavior2);

endmodule

VHDL logic:


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;


Thanks

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. 
 

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home


  1. VF Horizons:PAPER: SVA Alternative for Complex Assertions - SystemVerilog - Verification Academy
  2. http://systemverilog.us/vf/SolvingComplexUsersAssertions.pdf
  3. “Using SVA for scoreboarding and TB designs”
    http://systemverilog.us/papers/sva4scoreboarding.pdf
  4. “Assertions Instead of FSMs/logic for Scoreboarding and Verification”
    https://verificationacademy.com/verification-horizons/october-2013-volume-9-issue-3
  5. SVA in a UVM Class-based Environment
    https://verificationacademy.com/verification-horizons/february-2013-volume-9-issue-1/SVA-in-a-UVM-Class-based-Environment