Hi ,
I was trying to understand the working of below code :
bit clk , sig ;
initial forever #5 clk = !clk ;
property intersct ;
@(posedge clk) $rose(sig) |-> sig[*4] intersect 1[*10] ; // Working of consequent ??
endproperty
assert property( intersct );
initial begin
#04 ; sig = 1 ;
#90 ;
#5 ; $finish();
end
I notice the assertion fails at t:35 which I am not sure why ?
intersect operator requires that both left sequence and right sequence start and end at the same time .
On changing the stimulus to :
initial begin
#04 ; sig = 1 ;
#40 ; sig = 0 ; // sig[*4] is True from t:5 to t:35 .
#60 ;
#5 ; $finish();
end
The output remains the same i.e assertion fails at t:35
In reply to Have_A_Doubt:
as you wrote: intersect operator requires that both left sequence and right sequence start and end at the same time .
You have *sig[*4] intersect 1[10]. These are NOT of the same length.
Change the code to
**sig[4] intersect 1[1:10]
Here the 1[*1:10] has many threads, including the 1[*4] as an option. EPWave Waveform Viewer wave (1) - EDA Playground code
Ben Cohen Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
Hi Ben ,
Yes I do understand that the right sequence should be *1[4:10] , but even when using 1[*10] why is it that assertion fails at t:35 specifically ? i.e how is the consequent evaluated ?
(1) For the 1st stimulus , ‘sig’ is True throughout simulation :
initial begin
#04 ; sig = 1 ;
#90 ;
#5 ; $finish();
end
sig[*1] is True at t:5 , sig[*2] is True at t:15 , sig[*3] is True at t:25 , sig[*4] is True at t:35 .
My understanding is that the intersect operator fails as soon as either the left or right sequence is false , so at t:45 wouldn’t sig[*4] be considered false ?
(2) For the 2nd stimulus , ‘sig’ is False at t:45 :
initial begin
#04 ; sig = 1 ;
#40 ; sig = 0 ;
#60 ;
#5 ; $finish();
end
As ‘sig’ is false at t:45 , I expected the assertion to fail at t:45 .
Yet I see the assertion fails at t:35
In reply to Have_A_Doubt:
sig[*4:10] intersect 1[*10]
This means that sig must occur 4 to 10 times IN exactly 10 cycles.
If you the sequence (sig sig sig sig !sig)
Here the 1[*1:10] has many threads, including the 1[*4] as an option.
I am not sure I understand your question. However, you need the 1[*1:10].
With 1[*10] the sequence on the left hand side of the intersect MUSt match 10 cycles. (2) - EDA Playground // code EPWave Waveform Viewer // wave
sig[*4:10] intersect 1[*10]
You are asking that sig[*4] (in 4 cycles coincides 10 cycles; obviously false.
That consequent is only true with sig==1 in 10 consecutive cycles.
module m;
bit clk , sig ;
int pass, fail;
initial forever #1 clk = !clk ;
property intersct ;
@(posedge clk) $rose(sig) |-> sig[*4:10] intersect 1[*10]; // Working of consequent ??
endproperty
assert property( intersct ) pass=pass+1; else fail=fail+1;
initial begin
$dumpfile("dump.vcd"); $dumpvars;
@(posedge clk) sig <= 1 ;
repeat(3) @(posedge clk) sig<=1;
@(posedge clk) sig<=0;
#50 ; $finish();
end
endmodule
What I meant to ask is : from a reader’s perspective we can see that the left sequence and right sequence are not of the same length although they start at the same time at t:5 .
**(Q1) How do tools interpret the consequent : sig[4] intersect 1[10] ?
Left sequence sig[*4] starts at t:5 and it ends at t:35 .
**(Q2) Is this why the assertion fails at t:35 since left sequence sig[4] has ended whereas right sequence 1[10] hasn’t ended yet ?
I was curious to know why the assertion fails at t:35 specifically when we write the consequent as :
sig[*4] intersect 1[*10]
As you pointed the correct way to write the consequent is :
sig[*4] intersect 1[*4:10]
I wanted to understand the working of the original consequent *with the right sequence as 1[10]
What I meant to ask is : from a reader’s perspective we can see that the left sequence and right sequence are not of the same length although they start at the same time at t:5 .
**(Q1) How do tools interpret the consequent : sig[4] intersect 1[10] ?
sig[*4] intersect 1[*10] is interpreted as:
*sig[*4] intersect 1[*1] or // no possibility, will not match
sig[*4] intersect 1[*2] or // no possibility, will not match
sig[*4] intersect 1[*3] or // no possibility, will not match
sig[*4] intersect 1[*4] or // a possibility, can match
…
sig[*4] intersect 1[10] // // a possibility, can match
Thus if sig ==1 at t1, t2, t3, t4 the RHS thread of the intersect that ends at t4
meets the condition where the LHS and the RHS are start at the same cycle and end at the same cycle.
Left sequence sig[*4] starts at t:5 and it ends at t:35 .
**(Q2) Is this why the assertion fails at t:35 since left sequence sig[4] has ended whereas right sequence 1[10] hasn’t ended yet ?
sig[*4] intersect 1[*10] will always fail since it requires the LHS to be true
for 4 cycles while the RHS, also starts at the same time as the LHS, and be true for
10 cycles.
I was curious to know why the assertion fails at t:35 specifically when we write the consequent as :
sig[*4] intersect 1[*10]
As you pointed the correct way to write the consequent is :
``` verilog
sig[*4] intersect 1[*4:10]
sig[*4] intersect 1[*4:10] interpreted as:
*sig[*4] intersect 1[*4] or
sig[*4] intersect 1[*5] or
sig[*4] intersect 1[*6] or
..
sig[*4] intersect 1[*10]*
Hope this helps
As discussed in thread , the consequent being a degenerate sequence is illegal as per LRM.
Tool seem to interpret the consequent in context of intersect operator and the assertion fails once the LHS sequence ends