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?
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).
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).
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 ?