RE: [sv-bc] RE: Simulation semantics of deferred assertions (Mantis 3206)

Hi Gord,

Here is the list of the main checker specific features:

* Ability to be instantiated in a procedure

* Context inference

* Passing sequences and properties as arguments

* Common look and feel of ports and parameters

* Free variables

* Ability to handle sequence triggered method as a first class boolean

Do you think that we can extend the notion of a module to incorporate all these features? Isn't the situation similar to that of interfaces and programs? These constructs are also similar to modules, but they are not modules. What are your suggestions?

Thanks,
Dmitry

From: Gordon Vreugdenhil [mailto:gordonv@model.com]
Sent: Monday, November 08, 2010 5:11 PM
To: Korchemny, Dmitry
Cc: Eduard Cerny; Arturo Salz; sv-ac@eda.org; sv-bc@eda.org
Subject: Re: [sv-bc] RE: Simulation semantics of deferred assertions (Mantis 3206)

I really do not like this.

It is going to be yet another change to current semantics and a change that
is being added to support adding module like constructs to checkers -- something
that I don't like to begin with.

The question when checkers were first introduced was why they were needed versus
a few additional constructs to support formal semantics (checkvars or similar).
Checkers are now *syntactically* converging with modules but have tweaks with
special semantics. Is this really where we want to go with the language?

I am quite uncomfortable with the entire trajectory of this work.

Gord.

On 11/8/2010 4:06 AM, Korchemny, Dmitry wrote:
Hi Ed, Arturo,

It looks to me that maturing deferred assertions in the Re-NBA region would answer most practical needs. Of course, if a deferred assertion refers a checker variable which is a target of a nonblocking assignment, the race will be possible. However, such references do not have much sense in deferred assertions, since the targets of nonblocking assignments in checkers upon assignment essentially hold the future value of the variable, and not the current one. Therefore, if such variables are used in deferred assertions, they should be explicitly sampled.

For example, in a checker

always @clk a <= !b; //b defined elsewhere

assert #0 (c == a); // c is a design variable

does not make much sense, whereas

assert #0 (c == $sampled(a));

does.

Thanks,
Dmitry

From: Eduard Cerny [mailto:Eduard.Cerny@synopsys.com]
Sent: Saturday, November 06, 2010 2:50 PM
To: Arturo Salz; Korchemny, Dmitry; sv-ac@eda.org<mailto:sv-ac@eda.org>; sv-bc@eda.org<mailto:sv-bc@eda.org>
Subject: RE: Simulation semantics of deferred assertions (Mantis 3206)

Hi,

execution in RE-NBA may have its own problems because of a possible race with checker variable assignments, no?
What if deferred assertions used sampled values, would it help?

ed

From: owner-sv-ac@eda.org<mailto:owner-sv-ac@eda.org> [mailto:owner-sv-ac@eda.org] On Behalf Of Arturo Salz
Sent: Friday, November 05, 2010 9:25 PM
To: Korchemny, Dmitry; sv-ac@eda.org<mailto:sv-ac@eda.org>; sv-bc@eda.org<mailto:sv-bc@eda.org>
Subject: [sv-ac] RE: Simulation semantics of deferred assertions (Mantis 3206)

Dmitry,

If we allow assertions to drive new values into the design with zero delay then there is no bounded iteration limit that will guarantee that we have the final disposition of the assertions. So another disadvantage of option 2 is that in general it won't work. Another option would be to execute deferred assertions in the NBA-reactive region. Or, disallow driving values in the same time step from within a deferred assertion action blocks.

                Arturo

From: owner-sv-ac@eda.org<mailto:owner-sv-ac@eda.org> [mailto:owner-sv-ac@eda.org] On Behalf Of Korchemny, Dmitry
Sent: Friday, November 05, 2010 5:24 PM
To: sv-ac@eda.org<mailto:sv-ac@eda.org>; sv-bc@eda.org<mailto:sv-bc@eda.org>
Subject: [sv-ac] Simulation semantics of deferred assertions (Mantis 3206)

Hi all,

Deferred assertions were designed to avoid simulation glitches. However simulation glitches are still possible when some of the assertion subexpressions are evaluated in the Active region and the others in the Reactive one. In this case the assertion matures twice: the first time when it reaches the Observed region for the first time, and the second time when it reaches it again upon the evaluation in the Reactive region. One such example is discussed in Mantis 3206 (http://www.eda-stds.org/mantis/file_download.php?file_id=4571&type=bug). This situation is going also to occur in checkers when the continuous assignments in checkers are introduced.

To address these problems the simulation semantics of deferred assertions should be changed. I can think of the following options:
1. Make assertions mature in the Postponed region instead of the Observed one. The advantage of this solution is its simplicity, the obvious disadvantage is the inability to change anything from the assertion action blocks.
2. Require deferred assertions to "make two full iterations through simulation regions", and make them mature only starting at the second visit in the Observed region. The advantages is the ability to change design variables from the assertion action blocks (e.g., to count), its disadvantage is performance penalty and more complicate simulation semantics.

What would you suggest?

Thanks,
Dmitry
---------------------------------------------------------------------
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<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.
---------------------------------------------------------------------
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<http://www.mailscanner.info/>, and is
believed to be clean.
--
--------------------------------------------------------------------
Gordon Vreugdenhil                                503-685-0808
Model Technology (Mentor Graphics)                gordonv@model.com<mailto: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.