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

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.

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.

---------------------------------------------------------------------
Intel Israel (74) Limited

This e-mail and any attachments may contain confidential material for
the sole use of the intended recipient(s). Any review or distribution
by others is strictly prohibited. If you are not the intended
recipient, please contact the sender and delete all copies.


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