How to write Assertions for timing registers

In reply to ben@SystemVerilog.us:

Since NcSim is giving you grief with procedural concurrent assertion, you could, in some circumstances, have procedural code to write flags that can be used by concurrent (non-procedural) assertions. Thus, for the above problem:

bit start;
always @ (posedge clk) begin
  if (!start) start <= 1'b1;
end 
else Assertion9 : assert property(start |-> a9);

However, one would lose a lot of capabilities in not being able to write procedural concurrent assertions.
Ben Cohen http://www.systemverilog.us/

  • SystemVerilog Assertions Handbook, 3rd Edition, 2013
  • A Pragmatic Approach to VMM Adoption
  • Using PSL/SUGAR … 2nd Edition
  • Real Chip Design and Verification
  • Cmpt Design by Example
  • VHDL books