SVA: condition met between two disabled sections not showing pass/finish

In reply to Adarsh Santhosh:

In reply to ben@SystemVerilog.us:
Lets say during the “end/done” section, signal “a” is “0” and i wanted to check if it says low for rest of the sim.

Looks OK


// Assertion states that in the cyce following done, and thereafter the done, a==0 until end of sim
// CORRECTION ********
initial ap_preferred: assert property(@(posedge clk)
  done[->1] |=> strong(!a[*1:$]));  // THIS IS INCORRECT because
      // after the 1st !a the consequent completes. 
// What you need 
initial ap_preferred: assert property(@(posedge clk)
  done[->1] |=> s_always (!a) );