Re: [sv-bc] RE: [sv-ac] RE: [sv-ec] Checkers & Formal

Korchemny, Dmitry wrote:
> Hi Gord,
> 
> I am not sure I understand your question: the description of immediate
> and concurrent assertions exists already in LRM 2005, deferred
> assertions were introduced by Mantis 2005 in a close cooperation with
> SV-BC, and assertions in checkers are regular concurrent assertions.

Now I'm getting confused.  I thought that checker assertions were
NOT always the same as a substitution in the instantiation point.
In particular, that enable, etc inference is not done unless the
special $.. forms were used.

Is that not the case?

Gord.

> To summarize, immediate assertions act as an if statement, deferred
> assertions are roughly speaking immediate assertions reported once at
> the end of the simulation to avoid glitches (the subtlety here is that
> the assertions in different loop iterations and in different function
> invocations are treated as different assertions - see 2005 for more
> detailed description), and concurrent assertions are temporal assertions
> using sampled values of the variables. Concurrent assertions may be
> syntactically written in procedural code, but they are not executed
> together with the simulation flow, and use the procedural context to
> infer their clock and enabling condition, e.g.,
> 
> always @(posedge clk) begin : b1
> 	if (en) begin : b2
> 		...
> 		assert property(a);
> 	end
> end
> 
> is roughly equivalent to
> 
> always @(posedge clk) begin
> 	if (en) begin
> 		...
> //		assert property(a);
> 	end
> end
> 
> assert property(@(posedge clk) en |-> a);
> 
> "Roughly" means modulo scope: the original assertion is defined in the
> scope of b2, while the rewritten assertion is defined in the scope of
> the module.
> 
> Regards,
> 
> Dmitry
> 
> -----Original Message-----
> From: owner-sv-ec@server.eda.org [mailto:owner-sv-ec@server.eda.org] On
> Behalf Of Gordon Vreugdenhil
> Sent: Thursday, March 06, 2008 7:35 AM
> To: Korchemny, Dmitry
> Cc: sv-bc@server.eda.org; sv-ec@server.eda.org; sv-ac@server.eda.org
> Subject: Re: [sv-bc] RE: [sv-ac] RE: [sv-ec] Checkers & Formal
> 
> [Korchemny, Dmitry] ...
> 
> I'd like to have a fairly concise description of the differences
> in rules for immediate assertions, deferred assertions, concurrent
> assertions, and assertions in checkers.  All in the context of
> procedural code since that is the main area where things get
> really messy.  If that cannot be summarized concisely and
> completely, it would make me wonder about the complexity of
> the resulting language and whether we aren't opening the door
> to very difficult language compositionality issues in the future.
> 
> [Korchemny, Dmitry] ...
> 
> Gord
> 

-- 
--------------------------------------------------------------------
Gordon Vreugdenhil                                503-685-0808
Model Technology (Mentor Graphics)                gordonv@model.com


-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.