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, and is
believed to be clean.