RE: [sv-ac] Mantis 1756: The LRM does not indicate how the control tasks $asserton/off/kill affect verification statements in initial blocks

Hi Ben,
if I understand correctly, you are trying to stop ap_initi assertion. But this is an immediate assertion which executes at time 0, no clock involved. The two initial statements are in a race, the order of evaluation can be any. In this case the initial block with the assertion executed first. To avoid that you must either delay the execution of ap_initi by #0 or put them in the same initial block in the right order.

best regards,
ed

From: ben cohen [mailto:hdlcohen@gmail.com]
Sent: Friday, July 09, 2010 6:15 PM
To: Eduard Cerny
Cc: sv-ac@eda.org
Subject: Re: [sv-ac] Mantis 1756: The LRM does not indicate how the control tasks $asserton/off/kill affect verification statements in initial blocks

Ed,
I simulated the following code:
    module m;
  logic enb=0, a=0, b=0, clk=1;
  initial ap_initi: assert(a && b);
  initial $assertoff;
  initial forever #10 clk=!clk;

  always @ (posedge clk) begin
    ap_proc: assert property(@ (posedge clk) $rose(a) |=> b);
    a<=!a;
    b <= !b;
  end

  ap_conc: assert property(@ (posedge clk) $rose(a) |=> b);

endmodule
// simulation results
# ** Error: Assertion error.
# Time: 0 ps Scope: m.ap_initi File: kill.sv<http://kill.sv> Line: 3

If the goal of the $assertoff at the initial statement was to prevent any assertion during initialization, this simulator did not do that.
But it meets the LRM $assertoff shall stop the checking of all specified assertions until a subsequent $asserton. An assertion that is already executing, including execution of the pass or fail statement, is not affected.

<I think that it covers both assertions in always and in initial procedures.>
Agree with you
Ben

On Fri, Jul 9, 2010 at 1:26 PM, Eduard Cerny <Eduard.Cerny@synopsys.com<mailto:Eduard.Cerny@synopsys.com>> wrote:
Hello,

the mantis item was created early in 2007, before the new semantics of procedural assertions were defined in which case the specification of how the control tasks affect assertions in initial blocks was necessary. However, with the semantics as defined in the LRM, I do not believe that any further explanation is required.

In Clause 20.11, it states:
SystemVerilog provides the following three system tasks to control the evaluation of assertion statements:
- $assertoff shall stop the checking of all specified assertions until a subsequent $asserton. An
assertion that is already executing, including execution of the pass or fail statement, is not affected.
In the case of a deferred assertion (see 16.4), currently queued reports are not flushed and may still
mature, though further checking is prevented until the $asserton. In the case of a pending procedural
assertion instance (see 16.15.6), currently queued instances are not flushed and may still
mature, though no new instances may be queued until the $asserton.
- $assertkill shall abort execution of any currently executing specified assertions and then stop
the checking of all specified assertions until a subsequent $asserton. This also flushes any queued
pending reports of deferred assertions (see 16.4) or pending procedural assertion instances (see
16.15.6) that have not yet matured.
- $asserton shall reenable the execution of all specified assertions.

I think that it covers both assertions in always and in initial procedures.

Let me know if you agree, if yes, I will close the mantis item.

best regards,
ed

--
This message has been scanned for viruses and
dangerous content by MailScanner<http://www.mailscanner.info/>, and is
believed to be clean.
-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.