Hi Forum, what is difference bwt below two properties, I see the results are same.
module test;
bit a, b, en, clk;
initial begin
forever #5 clk = ~clk;
end
assert property ( @(posedge clk) en |-> a within (b [->1])); //line 10
//assert property ( @(posedge clk) en |-> (a [->1]) within (b [->1])); //line 11
initial begin
#5;
en = '1;
#1;
b = '1;
#12;
a = '1;
#10;
a = '0;
#5;
a = '1;
#5;
a = '0;
#10;
b = '0;
end
initial begin
#100; $finish(2);
end
endmodule
// result are same for 2 property
//“test.sv”, 7: test.unnamed$$_1: started at 15ns failed at 15ns
// Offending ‘b’
//“test.sv”, 7: test.unnamed$$_1: started at 45ns failed at 45ns
// Offending ‘b’
In reply to VE:
From my SVA Book
2.4.5 Sequence containment (within)
The sequence containment within specifies a sequence occurring within another sequence. A
visualization of a sequence containment composition is shown in Figure 2.4.5 wherein seq1 is
contained within seq2.
|-------<squence1>-------------|
|<---------sequence2---------->|
Note: (seq1 within seq2) is equivalent to: ((1[*0:$] ##1 seq1 ##1 1[*0:$]) intersect seq2 )
Thanks Ben.
I think I am still not sure why the property
XYZ: assert property ( @(posedge clk) en |-> (a [->1]) within (b [->1]));
failed at 45ns.
Based on your comments and the message from the simulator, I guess the evaluation started at 45ns, and at 45ns, en is true, b is true but a is not, so the assertion failed. If that is case, does it mean below are same ?
XYZ: assert property ( @(posedge clk) en |-> (a [->1]) within (b [->1]));
ABC: assert property ( @(posedge clk) en |-> a within (b [->1]));
or maybe the assertion XYZ does not really make sense?
initial begin
repeat(200) begin
@(posedge clk);
if (!randomize(a, b) with
{ a dist {1'b1:=1, 1'b0:=1};
b dist {1'b1:=1, 1'b0:=2};
}) `uvm_error("MYERR", "This is a randomize error");
end
$finish;
end