Hi.
I want to check the stable ‘idle’ signal after $fell(reset) |-> ##[0:1] idle
##[0:$] $stable(idle) does not work in my assertion checker.
property reset_chk0_p;
@(posedge clk)
$fell(reset) |-> ##[0:1] idle ##[0:$] $stable(idle) ##[0:$] $rose(reset);
endproperty
How do I check the idle stable after “$fell(reset) |-> ##[0:1] idle” ?
In reply to UVM_LOVE:
$fell(reset) |-> ##[0:1] idle[*1:$] intersect $rose(reset)[->1];
Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
or Cohen_Links_to_papers_books - Google Docs
Getting started with verification with SystemVerilog
In reply to UVM_LOVE:
the following assertion will check idle is high as long as reset is low. what will be the value of idle when reset transition to high.
property reset_chk0_p;
@(posedge clk)
$fell(reset) |-> ##[0:1] idle ##0 idle[*0:$] intersect !reset[*0:$] ##1 $rose(reset);
endproperty
In reply to ben@SystemVerilog.us:
Thanks you Ben,
Intersect is that sequence must start and finish in the same cycle whether they are matched or not.
Can I inquire about the reason behind your usage of “[->1]”?
In reply to kddholak:
In reply to UVM_LOVE:
$rose(reset)[->1] is equivalent to !reset[*0:$] ##1 $rose(reset)
What is the difference between
fell(reset) |-> ##[0:1] idle ##0 idle[*0:] intersect !reset[*0:$] ##1 $rose(reset);
and
fell(reset) |-> ##[0:1] idle idle ##[0:] intersect !reset[*0:$] ##1 $rose(reset); ?
I’m confused between “idle[*0:]" and "idle ##[0:]”.
idle[*0:$] can be interpreted as (idle ##1) (idle ##1 idle ##1) (idle ##1 idle ##1 idle ##1)…
idle ##[0:$] can be interpreted as (idle ##0) (idle ##1 idle ##1) (idle ##1 idle ##1 idle ##1)…
In reply to UVM_LOVE:
idle[*0:$](repetition with unbounded range) is equivalent to
!idle or idel ##1 idel or idel ##1 idel ##1 idel or .. so on.
##[0:$] idel (its unbounded range) is equivalent to
idel or !idel ##1 idel or !idel ##1 !idel ##1 idel or .. so on.
In reply to UVM_LOVE:
That’s why we test our assertions; we may have the right concept but miss a small detail.
Apologies
$fell(reset) |-> (##[0:1] idle[*1:$] ##1 1) intersect $rose(reset)[->1];
In reply to ben@SystemVerilog.us:
In reply to UVM_LOVE:
That’s why we test our assertions; we may have the right concept but miss a small detail.
Apologies
$fell(reset) |-> (##[0:1] idle[*1:$] ##1 1) intersect $rose(reset)[->1];
Thanks this also work.
property reset_chk0_p;
@(posedge clk)
$fell(reset) |-> ##[0:1] idle[*1:$] ##1 $rose(reset);
endproperty
In reply to UVM_LOVE:
Using $stable :
sequence stable_seq ;
$stable(idle) throughout $rose(reset)[->1] ;
endsequence
property reset_chk0_p;
@(posedge clk) $fell(reset) |-> ##[0:1] idle ##1 stable_seq ;
endproperty
// We use ##1 stable_seq instead of ##0 stable_seq as idle could have changed at same clock as $fell(reset) is True OR 1 clock after $fell(reset) is True.
// Hence $stable(idle) would be False in these 2 cases had we used ##0 stable_seq
In reply to Have_A_Doubt:
In reply to UVM_LOVE:
Using $stable :
sequence stable_seq ;
$stable(idle) throughout $rose(reset)[->1] ;
endsequence
property reset_chk0_p;
@(posedge clk) $fell(reset) |-> ##[0:1] idle ##1 stable_seq ;
endproperty
// We use ##1 stable_seq instead of ##0 stable_seq as idle could have changed at same clock as $fell(reset) is True OR 1 clock after $fell(reset) is True.
// Hence $stable(idle) would be False in these 2 cases had we used ##0 stable_seq
Can’t implement like this instead of using the sequence?
property CHK03;
@(posedge clk)
//$fell(reset) |-> ##[1:2] idle[*0:$] ##1 $rose(reset);
$fell(reset) |-> ##[1:2] idle ##1 $stable(idle) throughout $rose(reset);
endproperty
CHK03_P : assert property (CHK03);