RE: [sv-ac] CheckerUsability

Hi Tom,

I am attaching the updated version of the document following your comments. It also contains modifications in the description of checker output argument reflecting my private discussion with Laurence. See also my comments below.

Thanks,
Dmitry

-----Original Message-----
From: Thomas J Thatcher [mailto:thomas.thatcher@oracle.com]
Sent: Thursday, September 09, 2010 4:29 AM
To: Korchemny, Dmitry
Cc: sv-ac@eda.org
Subject: Re: [sv-ac] CheckerUsability

Hi Dmitry,

Here is some feedback on the checker usability document.

First of all, there needs to be some kind of justification or use case
presented at the beginning. Tell everyone what use cases we are trying
to support. I'm not suggesting that you dive in with code examples. I
would like to see high-level block diagrams of the kinds of things we
want checkers to do. Then all the proposed changes will fit into context.

[Korchemny, Dmitry] I added a brief motivation section. Specific proposals should provide more detailed and elaborated motivation sections. Could you provide an example of a block diagram you are talking about? Are you talking about use cases?

On page 3, where you give the reason for sampling RHS variables of
checker non-blocking assignments:

You don't need a two-clock scenario to show the need for sampling. A
much simpler example will do. If you have a design variable driven by a
non-blocking assignment, which is then passed to a checker, and appears
on the RHS of a checker NBA, you will get the following sequence of events:

        Active Region: clock rises
                        Design always block is triggered
                        Assignment to design variable is scheduled
        NBA Region: design variable assigned
        Reactive Region: Checker always procedure is triggered
                        because of the clock rising:
                        Assignment to checker variable is scheduled
                        If design variable is not sampled, the
                        assignment will use the new value.
        Re-NBA Region: Checker variable NBA occurs

THAT's why we need sampling.

[Korchemny, Dmitry] The explanation I provided is required for checker variables. The need in sampling of checker variables in the RHS of a checker variable NBA is not obvious, and normally both sampled and non-sampled checker variables yield the same result. However, I realized that I did not provide the explanation why non-checker variables should be sampled. I added a small example to clarify this point.

Also, statements like "If checker variables are assigned in the Re-NBA
region, it would be before the Observed region are only going to confuse
people. The Observed region is before the Re-NBA region. Of course,
assignments in the Re-NBA region will cause a trip around the "big
loop", resulting in the simulator visiting the Observed region again in
the time step (which I think is what you meant).

[Korchemny, Dmitry] I slightly modified the language:
"Since checker variables are assigned in the Re-NBA region, when the clock is generated in the Reactive region this assignment will be performed before entering the Observed region for the second time."

Also, do you envision clock signals being created inside checkers? If
so, why? Better discuss this in your use cases. One person I talked to
today, said, "Don't do that, that is only going to cause scheduling
problems."

[Korchemny, Dmitry] I think that generating clock signals inside checkers may be very useful. However, this is not related to the enhancements described in this document, because this is already legal. Here are two examples:

1. For internal checker needs define a clock which is twice as slow as some given clock:

bit sclock = 0;
always @clk sclock <= !sclock;
always @sclock
        // ...

2. We may want to define a non-deterministic clock and reason about assertions with this clock:

rand bit clk;
m1: assume property (@$global_clock $rising_gclk(clk));
a1: assert property (@clk s_eventually some_property);

---
That's all for now.  I'll send more feedback as I think of it.
Tom
---------------------------------------------------------------------
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.