Concurrent Assertion :: After ' a ' is True . ' b ' Should Never be True till end of Simulation

SystemVerilog
,
1

Hi all ,

I coded the following ::


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 .

Any suggestions ?

2

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,

a  |=>  always strong(!b)
3

In reply to ben@SystemVerilog.us:

Ben , I tried using

a  |=>  always strong(!b)

However I still don’t see the assertion Pass display .

4

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);
5

In reply to ben@SystemVerilog.us:

Got it . So I would have to use an appropriate unbounded delay

6

In reply to hisingh:

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.