An interesting issue came up in the VerificationAcademy forum where an assertion leading clocking (LC) is one of those signals modified in the NBA or Reactive regions instead of the traditional posedge clk. For example, what is the difference between (@(sig) b|-> c;) and (@(posedge clk) b|->c;) when sig is a signal modified in the NBA or Observed, or Reactive region of the (posedge clk) time step? Another question related to regions: how is the disable iff handled when the disabling condition is updated in any of the SystemVerilog regions?
This paper goes into detail about how these regions should be handled by a simulator as described in the SystemVerilog LRM; this should give you a better understanding of how assertions work. The paper makes two important points: 1) Clocking events occurring in the same time step in different regions (e.g. Active, NBA, Observed, and Reactive) are indistinguishable due to the sampling of signals. 2) Upon entry or reentry into the Observed region, a scheduled assertion will be disabled with a disable iff(signal) if that signal was true before it entered that evaluation region. Recommendations for handling this type of coding style are also
provided.
Ben Cohen Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
https://docs.google.com/document/d/1W488Af-UiHJ9V6bHsmim4ge607JSfWCYXuSrz_lHNTM/edit?usp=sharing