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

Hi Gord,

I missed several your emails, hope it is not too late.

Checker assertions are regular concurrent assertions if they are
considered in the checker context. The following examples illustrate
this statement:

Example 1.

checker mycheck1 (logic a, event clk = $inferred_clock);
	p: assert property (@clk a);
endchecker

module m;

logic x, clock;

...

always @(posedge clock) begin
	...
	mycheck1 c(x);
end

In this example the assertion p has an explicitly specified clock - clk;
assertion usage in checkers is consistent with their usage in modules.
The value of clk is inferred as (posedge clock), but it is related to
the argument passing mechanism, and not to the inference rules for the
assertion itself.

Example 2.

checker mycheck2 (logic a, event clk = $inferred_clock);
	always_check @clk
		p: assert property (a);
endchecker

module m;

logic x, clock;

...

always @(posedge clock) begin
	...
	mycheck2 c(x);
end

In this case the clock for assertion p is inferred from always_check as
clk since p does not have an explicit clock (of course, modules don't
have always_check, but this is immaterial for our discussion). Since clk
gets value of (posedge clock), the result is identical to mycheck1.

Example 3.

checker mycheck3 (logic a, event clk = $inferred_clock);
	p: assert property (a);
endchecker

module m;

logic x, clock;

...

always @(posedge clock) begin
	...
	mycheck3 c(x);
end

In this example the assertion p does not have any clock to infer, and
therefore a compilation error will be issued. The fact that clk gets
value of (posedge clock) does not change anything.

To summarize, the inference rules for assertions in checkers are not
different from the inference rules in modules.

Thanks,
Dmitry

-----Original Message-----
From: Gordon Vreugdenhil [mailto:gordonv@model.com] 
Sent: Monday, March 10, 2008 6:11 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 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

---------------------------------------------------------------------
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.