Assertion attempt getting incomplete

SystemVerilog
1 
//stimulus
initial begin
            b=0 ;
            c=1;
           g=0;
           clk=0;
        #5  b=1 ;
        #10  c=0;
        #10 g=1;

#200 $finish;
end
//clock_generator
  always #1 clk=!clk;

assert property (@(posedge clk)
$rose(b) |-> ##[1:$] !c |-> ##[1:$] $rose(g)) ;

In the above code I was expecting the assertion attempt starting from time 7 to be successful at 27 , but instead its showing an incomplete attempt at the end of the simulation. Can someone point out the issue?

2

In reply to svishnu:
From my SVA book:
"Multi-thread sequences in both antecedent and consequent
 Rule: If an assertion of a property has a multi-threaded sequence used as an antecedent, then all threads must be exercised in search of a matched antecedent with a first match of the consequent, unless the assertion fails. In that case, the search is short-circuited (i.e., stopped). The assertion is considered failed if there is a matched antecedent with a non-matched corresponding thread of the consequent. For the assertion to be successful, two requirements must be met:

  1. There must be no failure in the search of a matched antecedent with a first match of the consequent.
  2. All threads of the antecedent and consequent must be successful (i.e., vacuous success or true pass).
    Consider the following assertion:
ap_consequent_any_match: assert property(
$rose(a) ##[1:4] b |-> ##[1:3] c);

For the assertion to succeed, all threads of the antecedent must be exercised, the antecedent must match at least once, and upon that match the consequent must thereafter match once within the range of 1 to 3 clocking events (i.e., cycles). If the consequent fails to match within that range for any thread, the assertion fails. As per previous guidelines, it is recommended to rewrite the assertion property as follows:

first_match($rose(a) ##[1:4] b) |-> ##[1:3] c);

For your specific assertion, I have a few comments on style:

assert property (@(posedge clk)
$rose(b) |-> ##[1:$] !c |-> ##[1:$] $rose(g));
// From above, youll need to add the first_match() in the 2nd antecedent 
ap_OK: assert property (@(posedge clk)
$rose(b) |-> first_match(##[1:$] !c) |-> ##[1:$] $rose(g));
// A beeter assertion would be 
ap_better: assert property (@(posedge clk)
first_match($rose(b) ##[1:$] !c) |-> ##[1:$] $rose(g));
// ANOTHER OPTION: 
ap_better2: assert property (@(posedge clk)
   $rose(b) ##1 !c[->1] |-> ##[1:$] $rose(g));
// Note: 
a ##1 b[->1] |-> c; // is equivalent
a ##1 !b[*0:$] ##1 b ] |-> c;

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us