bit clk , a , b ;
property ab ;
@( posedge clk ) a |=> always !b ;
endproperty
initial forever #5 clk = ! clk ;
initial begin
// ' b ' is NEVER True after ' a ' is True at T : 5
//
#4 ; a = 1 ;
#10 ; a = 0 ;
#10 ; a = 0 ;
#50 ;
#5 ;
$finish() ;
end
a_property : assert property ( ab ) else $display(" TIME : %0t AB FAIL " , $time ) ;
c_property : cover property ( ab ) $display(" TIME : %0t AB PASS " , $time ) ;
My expectation was that the assertion would pass as there was No b , however I observe No O/P i.e Incomplete Assertion .
In reply to hisingh:
If the strong or weak operator is omitted, then the evaluation of the sequence_expr (interpreted as a property) depends on the assertion statement in which it is used. If the assertion statement is assert property or assume property, then the sequence_expr is evaluated as weak(sequence_expr). Otherwise, the sequence_expr is evaluated as strong(sequence_expr). Thus,
In reply to hisingh:
Ran the assertion below. Because there no failure, the error count is zero. At the end of simulation the tool reports the Active count. It canot report the pass action block because the assertion is not finished, and is in the active state.
property ab ;
@( posedge clk ) a |=> always !b;
endproperty
ap_always : assert property (@(posedge clk) a |=> s_always[1:10000] !b) else $display(" TIME : %0t AB FAIL " , $time );
ac_always : cover property (ab);
There are a couple of issues in play here. The main issue is that dynamic simulation cannot consistently prove that a safety property like always or a liveness property like eventually will definitively pass or fail, only static formal analysis can do that.
For a bounded strong sequence, a dynamic simulation can trigger a failure if the sequence does not reach its endpoint by the end of simulation. But all you can say for an unbounded sequence is that it has been started and still active, but it can never reach an endpoint.
How this gets reported is tool specific. This Mentor/Siemens EDA sponsored public forum is not for discussing tool specific usage or issues. Please read your tool’s user manual or contact your tool vendor directly for support.