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:

I think you have a race between the two initial procedures.

J.H.

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of ben
cohen
Sent: Friday, July 09, 2010 5: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 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>
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 <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.