In reply to bhajanpreetsinght:
ap_go_data_vld: assert property( @(posedge clk)
$rose(go) |-> go && $changed(vld)[->1] or go && $changed(data)[->1] within
($rose(go) ##1 $fell(go) [->1]))
pass=pass+1; else fail=fail+1; // for debug
Question: Why does the property (seq1 within seq2) not fail when seq1 is not a match?
In Evaluation. My previous response is incorrect
(seq1 within seq2) is equivalent to: ((1[*0:] ##1 seq1 ##1 1[*0:]) intersect seq2 )
For example, let seq2=1[*3]; let seq=0; then
((1[*0:$] ##1 seq1 ##1 1[*0:$]) intersect seq2 ) // get reduced to
((1[*0:$] ##1 0 ##1 1[*0:$]) intersect 1[*3] )
// the intesect occurs on the 3rd cycle with
((1[*3] ##1 0 ##1 1[*0:$]) intersect 1[*3] ) // true, and never false
(1[*2] ##1 0 intersect 1[*3] // final reduction., yielding a NO MARCH
Question: How can we write an assertion that detects seq1 is a no match (a failure)?
Actually, there is an issue with he ORing, and I am currently talking to my colleague on this.
FOr educational purposes, I am providing a solution with support logic.
Again, this should NOT be needed here.
The concept is to set a variable when seq1 occurs within seq2, and then check for that variable. The following fails to work because of SVA limitation, but it demonstrates the concepts.
(4) - EDA Playground // code
EPWave Waveform Viewer //wave
property p_changed_ILLEGAL;
bit v;
@(posedge clk) $rose(go) |-> ((go && $changed(vld)[->1], v=1) within
($rose(go) ##1 $fell(go) [->1]))
and $fell(go)[->1] ##0 v==1;
Local variable v referenced in an expression where it does not flow.
To overcome this SVA issue, you can use a function call to set a module variable (or a static function variable) when seq1 is a match (or true if an expression). You can then check if that variable was set. You need to make sure that another attempt does not clobber taht variable. In this case, since you cannot have 2 consecutive rose(go) without a fall(g) that terminates the assertion, there is no issue here.
(4) - EDA Playground // code
EPWave Waveform Viewer //wave
bit clk, go, vld, data, dbg;
int pass1, fail1, pass2, fail2, covered;
function static bit achange(bit set, value);
bit happened; // support logic
if (set) happened=value;
dbg=happened; // debug
return happened;
endfunction
property p_changed;
bit v; // v is used for syntax conformity, not by the assertion
@(posedge clk) ($rose(go), v=achange(1, 0)) |->
(go && $changed(vld)[->1] ##0 (1, v=achange(1, 1)) or
go && $changed(data)[->1] ##0 (1, v=achange(1, 1)) within
($rose(go) ##1 $fell(go)[->1])) and
$fell(go)[->1] ##0 dbg; // achange(0,0);
endproperty
ap_go_data_vld2: assert property(p_changed)
begin pass2=pass2+1; end else
begin fail2=fail2+1; end // for debug
Note: If I made that function void with no return, then
there is no need for the property local variable
(5) - EDA Playground // code
EPWave Waveform Viewer // wave
function void achange(bit set, value);
bit happened; // support logic
if (set) happened=value;
dbg=happened; // debug
//return happened;
endfunction
property p_changed;
//bit v; // v is used for syntax conformity, not by the assertion
@(posedge clk) ($rose(go), achange(1, 0)) |->
(go && $changed(vld)[->1] ##0 (1, achange(1, 1)) or
go && $changed(data)[->1] ##0 (1, achange(1, 1)) within
($rose(go) ##1 $fell(go)[->1])) and
$fell(go)[->1] ##0 dbg; //
endproperty
ap_go_data_vld2: assert property(p_changed)
begin pass2=pass2+1; end else
begin fail2=fail2+1; end // for debug
A 3rd option is to use a task with fork-join_any called upon a rose(go) as
described in my paper on Understand SVA.
Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
or Links_to_papers_books - Google Docs
Getting started with verification with SystemVerilog
