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

Hi Neil,

Please, see below.

Thanks,
Dmitry

-----Original Message-----
From: Neil Korpusik [mailto:neil.korpusik@oracle.com]
Sent: Tuesday, November 09, 2010 4:46 AM
To: Korchemny, Dmitry
Cc: Gordon Vreugdenhil; Eduard Cerny; Arturo Salz; sv-ac@eda.org; sv-bc@eda.org
Subject: Re: [sv-ac] RE: [sv-bc] RE: Simulation semantics of deferred assertions (Mantis 3206)

Hi Dmitry,

This whole discussion sounds like a good topic for the upcoming SV-AC
face-to-face meeting in February. This is the sort of topic which is
difficult to resolve via email.

[Korchemny, Dmitry] I agree. If it is decided that this issue is important, we will discuss it in our F2F meeting.

Arturo made some suggestions for potential changes to the semantics of deferred
assertions that might be useful in your environment. One of those suggestions
involved changing deferred assertions so that they mature in the Re-NBA region.

I don't see how this particular change will help much. Value changes driven out
of a program output port will happen in the reactive region set, but the
"design processes sensitive to those cross-region variables and nets are
scheduled for wake up in the active region set." (24.3.2). Because of this, the
new values coming from the program block may not reach the inputs to the
deferred assertions until the event processing has gone around the Outer loop.
That would leave you with the same glitch problem that you are trying to
eliminate.

[Korchemny, Dmitry] This is a serious issue.

There is also the problem of breaking backward compatibility.

[Korchemny, Dmitry] If we come to some acceptable solution, we will have to consider its implications to the backward compatibility. We should strive to introduce as little incompatibility as possible.

Deferred assertions, as they are defined today, are very useful. The cases
that you are trying to resolve seem to be more related to methodology
issues rather than language issues.

[Korchemny, Dmitry] I do my best to filter out pure methodology issues. This one seems to be a real issue of the language.

Neil

On 11/08/10 13:32, Korchemny, Dmitry wrote:
> Hi Gord,
>
>
>
> Please, see below.
>
>
>
> Thanks,
>
> Dmitry
>
>
>
> *From:* Gordon Vreugdenhil [mailto:gordonv@model.com]
> *Sent:* Monday, November 08, 2010 6:34 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 agree with Neil -- don't do things that cause the problems.
>
> Deferred assertions were explicitly designed to deal with
> "in-region" glitching. Trying to extend that to cross-region
> glitching isn't going to work very well. We intentionally
> and explicitly agreed that "big loop" issues causing glitches
> were going to be part of the model.
>
> */ /*
>
> */[Korchemny, Dmitry] We told that mixing in the same assertion design
> and TB variables is not a good methodology. The problem that we
> disregarded is the case when an assertion/assumption combines a primary
> input and an internal signal. Writing such untimed assertions is not a
> good practice for ABV. However, this is done for formal equivalence
> check, and such assertions/assumptions turned out to be essential. /*
>
>
> Having re-active continuous assigns in checkers and
> expecting clean interactions with the design is not really
> reasonable -- the program regions and design regions
> were intentionally designed to provide for TB/DUT
> interaction, not for interwoven interaction and it has
> been intentional in EC and BC to go that route.
>
> */[Korchemny, Dmitry] We can consider defining continuous and blocking
> assignments in checkers in the Active region. This looks strange since
> the nonblocking assignments in checkers are performed in the Re-NBA
> region. We will discuss this and see what the implications are./*
>
>
> So I don't think that there should be a solution to this
> that involves creating specific program/design region
> scheduling requirements. The checkers semantics
> for things like CAs or other problematic features should
> probably be re-examined by the AC to see whether they
> can be fit more cleanly into a single region. I certainly
> don't want to try to twist the original (already complex)
> scheduling model to fit different assumptions and
> interactions for which it was never designed.
>
> */[Korchemny, Dmitry] We will do that and see if it is possible (as I
> mentioned above)./*
>
>
> If AC can make a sufficiently strong case for yet another
> scheduling sub-loop, you could try to go that route,
> but there is going to be a great deal of resistance to that
> as well.
>
> */[Korchemny, Dmitry] This is the last resort./*
>
>
> Gord.
>
> On 11/8/2010 8:12 AM, Korchemny, Dmitry wrote:
>
> Hi Gord,
>
>
>
> I think it is our common goal to make the checker semantics consistent
> with the semantics of the rest of the language, and this is what we are
> trying to do. On the other hand we need to address the problems we have,
> and not to ignore them because they require changes. The reason I sent
> this problem not only to SV-AC but also to SV-BC is to seek help in
> solving the problem we have. I value the SV-BC expertise very high, and
> I am sure you can suggest the most appropriate solution.
>
>
>
> Thanks,
>
> Dmitry
>
>
>
> *From:* Gordon Vreugdenhil [mailto:gordonv@model.com]
> *Sent:* Monday, November 08, 2010 5:59 PM
> *To:* Korchemny, Dmitry
> *Cc:* Eduard Cerny; Arturo Salz; sv-ac@eda.org <mailto:sv-ac@eda.org>;
> sv-bc@eda.org <mailto:sv-bc@eda.org>
> *Subject:* Re: [sv-bc] RE: Simulation semantics of deferred assertions
> (Mantis 3206)
>
>
>
> It is almost certainly too late now to re-examine the decisions; I
> certainly
> don't have a full proposal for more consistent approaches. Such things
> take real time and collaborative effort.
>
> But as you might recall, I originally had serious reservations about
> future needs
> for adding sequential semantics (processes, etc) into checkers. That
> is now
> coming home to roost. I have my doubts that the entire direction has been
> explored nearly enough yet. For example, do you really have solid
> semantics for processes that are "instantiated" via a procedure call? What
> about *all* of the things that can occur in sequential blocks and routines
> called from them? How much global analysis and synthesis like logic
> flattening is now being assumed?
>
> In terms of your list, "common look and feel" is extremely deceptive --
> having a "common look and feel" with dissimilar semantics is worse
> for language design than doing something that is both semantically
> and syntactically differentiated.
>
> Sequence triggered isn't first class in any case -- you cannot pass that to
> a task with a boolean argument and have it retain the persistent
> "triggered" state for "wait". Is having something that is only half-way
> consistent better? I don't think it is.
>
> In any case, I am going to be very concerned about changes to semantics
> for anything in checkers which are not aligned with non-checker semantics.
> Assertions are only one part of that -- sequential process and tf semantics
> are also crucial.
>
> Gord
>
> On 11/8/2010 7:36 AM, Korchemny, Dmitry wrote:
>
> 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 <mailto:sv-ac@eda.org>;
> sv-bc@eda.org <mailto: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
> <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.
>
>
>
>
> --
>
> --------------------------------------------------------------------
>
> 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.
>
>
>
> --
>
> --------------------------------------------------------------------
>
> 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* <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, and is
believed to be clean.