Unwanted trigger of assertion

I have a design that takes an input bit (in),operation mode (mode) and a load signal (ld), when the load is active for two clock cycles an output is generated and a signal called valid is driven high.

I wrote this sequence and property to check the timing of the valid signal

sequence seq;
		(ld==1) and (mode==1) ##1 (ld==1) and (mode==1) ;
endsequence

property QPSK;
		@(posedge clk)
	        seq |=>  valid==1;
endproperty

The issue is that if ld is high for 4 consecutive clock cycles the property triggers 3 times instead of two, is there a way to use a counter in the property or any workaround to solve this issue?

In reply to Battawi:

Two possible solutions


sequence seq;
		(ld==1) and (mode==1) ##1 (ld==1) and (mode==1) ;
endsequence
// [Ben] DOn't use the sequence "and" since you are addressing a logical "and"
//       Use the &&
// Since solution Require ld to have a rise, probably NOT WHAT YOU WANT
// I provide it as an option, depending upon your requirements 
property QPSK_with_rose; // 
		@(posedge clk)
	    $rose(ld) ##1 ld |=> valid; // 
endproperty

Another option WITH CONSECUTIVE LOADS


bit ld_venb=1'b1; // If==1 then enable the start of 2 consecutive loads
               // ld_venb==load verification enable 
function void ld_set(bit v);
   ld_venb=v; 
endfunction
property QPSK;  
    @(posedge clk)
    (ld && ld_venb, ld_set(0)) ##1 (1'b1, ld_set(1)) ##0 ld |=> valid;  
endproperty
// 1) if(ld && ld_venb) set the ld_venb==0 to disable the start of 
//    another new assertion attempt at the next cycle.
//    Remember that at every clocking event  there is a new attempt 
//    at the assertion, irrespective of other previously started assertions. 
//    If(ld==0) at the attempt, the ld_venb remains a 1'b1. 
// 2) at the next cycle, regardless of the value of ld at the 2nd cycle,
//    enable the  the start of another new assertion attempt 
//    at the next cycle (i.e., the 3rd cycle). 

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr


  1. SVA Alternative for Complex Assertions
    Verification Horizons - March 2018 Issue | Verification Academy
  2. SVA: Package for dynamic and range delays and repeats | Verification Academy
  3. SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy

In reply to ben@SystemVerilog.us:

The second solution works for both cases even if ld rises for the first time.
Thanks for the help I really appreciate it

In reply to ben@SystemVerilog.us:

In reply to Battawi:
Two possible solutions


sequence seq;
(ld==1) and (mode==1) ##1 (ld==1) and (mode==1) ;
endsequence
// [Ben] DOn't use the sequence "and" since you are addressing a logical "and"
//       Use the &&
// Since solution Require ld to have a rise, probably NOT WHAT YOU WANT
// I provide it as an option, depending upon your requirements 
property QPSK_with_rose; // 
@(posedge clk)
$rose(ld) ##1 ld |=> valid; // 
endproperty

Another option WITH CONSECUTIVE LOADS


bit ld_venb=1'b1; // If==1 then enable the start of 2 consecutive loads
// ld_venb==load verification enable 
function void ld_set(bit v);
ld_venb=v; 
endfunction
property QPSK;  
@(posedge clk)
(ld && ld_venb, ld_set(0)) ##1 (1'b1, ld_set(1)) ##0 ld |=> valid;  
endproperty
// 1) if(ld && ld_venb) set the ld_venb==0 to disable the start of 
//    another new assertion attempt at the next cycle.
//    Remember that at every clocking event  there is a new attempt 
//    at the assertion, irrespective of other previously started assertions. 
//    If(ld==0) at the attempt, the ld_venb remains a 1'b1. 
// 2) at the next cycle, regardless of the value of ld at the 2nd cycle,
//    enable the  the start of another new assertion attempt 
//    at the next cycle (i.e., the 3rd cycle). 

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr


  1. SVA Alternative for Complex Assertions
    https://verificationacademy.com/news/verification-horizons-march-2018-issue
  2. SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
  3. 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

Incase of load being high for 4 consecutive clk cycles, I am trying to understand the sequence of events for the second clk cycle.
As per the code, in the second clock cycle, ld_venb is being set to 1 by calling ld_set(1). In the same cycle, assertion triggers again, checking for ld && ld_venb.
Would the function call happen after the antecedent check?. What would be the sequence of events in this delta cycle ?

In reply to verif_gal:


(ld && ld_venb, ld_set(0)) ##1 (1'b1, ld_set(1)) ##0 ld |=> valid;  
       t0     t1     t2       t3
-------+------+-------+-------+------+
ld        1   |   1   |   1   |   1  |
ld_venb   1   |0      |1      |
valid     1   |   1   |   1   |
attempt       True    False   True
assertion                     PASS
t1 has a successful attempt, Assertion for tha attemt PASS at t3
t2 has a failed attempt, assertionfor that attempt is vacuous