Re: [sv-ac] RE: more on 1900 checkers

Hi Dmitry,

If you are planning to have random simulation behavior for free variables
within checkers I strongly suggest that you do this in a manner that is
consistent with the way it is currently defined for classes. See clause 17 for
details.

There are two types of random variables allowed within classes; rand and randc.
There is a lot of material in clause 17 but make sure you do get a chance to
review sub-clauses 17.13 and 17.14 which discuss the repeatability concerns
that Tom mentioned. The notion of thread/object stability is an important
consideration that should be taken into account by your checker proposal.

Based on what I know about your proposal it sounds like what is already
defined for classes can be reused in the checker construct. Maybe all of
what is in clause 17 won't need to apply to checkers but there does appear
to be overlap in what you want to do in checkers and what is already defined
for classes.

I also don't understand this comment:

> We agreed at the last SV-AC meeting to add a note that it shall be
> illegal to use non-deterministic free variables in simulation.

The LRM is defined in terms of simulation semantics, so this doesn't
seem to make any sense. This boils down to not allowing non-deterministic
free variables at all, yet it is in the checker proposal.


Neil


Korchemny, Dmitry wrote On 10/15/07 01:16 AM,:
> Hi Tom,
> 
>  
> 
> We agreed at the last SV-AC meeting to add a note that it shall be
> illegal to use non-deterministic free variables in simulation. It does
> not prevent vendors, of course, from suggesting custom solutions for
> simulating non-deterministic assumptions. Fixing the simulation
> algorithm in the LRM now will lead to backward compatibility problems if
> wanted to change it in the future.
> 
>  
> 
> Thanks,
> 
> Dmitry
> 
>  
> 
> ------------------------------------------------------------------------
> 
> *From:* Thomas.Thatcher@Sun.COM [mailto:Thomas.Thatcher@Sun.COM]
> *Sent:* Sunday, September 30, 2007 8:00 AM
> *To:* Korchemny, Dmitry
> *Cc:* Lisa Piper; sv-ac@eda-stds.org
> *Subject:* Re: [sv-ac] RE: more on 1900 checkers
> 
>  
> 
> Hi Dmitry,
> 
> With regard to assume property statements and free variables, Lisa is
> correct. We are changing
> the semantics of assume property statements. Up to now assume property
> statements have been
> identical to assert property statements in a simulation environment.
> They simply check the property.
> In this proposal we are extending the function of assume property
> statements to actually guide the
> randomization of values.  This does open up all kinds of questions about
> what happens if a constraint
> solver can't generate a value that satisfies all assumptions.
> One idea:  should we use the same mechanism for randomization that is
> used for class member initialization?
> 
> I think I'm OK with variables being randomized differently on different
> simulators.  But there does need
> to be a way to control repeatability and randomization. 
> 
> Tom
> 
> Korchemny, Dmitry wrote:
> 
> Hi Lisa,
> 
>  
> 
> Please, see my comments below.
> 
>  
> 
> Thanks,
> 
> Dmitry
> 
>  
> 
> ------------------------------------------------------------------------
> 
> *From:* Lisa Piper [mailto:piper@cadence.com]
> *Sent:* Tuesday, September 25, 2007 4:26 AM
> *To:* Korchemny, Dmitry
> *Cc:* sv-ac@eda-stds.org <mailto:sv-ac@eda-stds.org>
> *Subject:* more on 1900 checkers
> 
>  
> 
> Dmitry,
> 
> 1. Doesn’t the following significantly change the requirements of a
> simulator relative to the processing of assume statements, and guarantee
> differences across simulators? 
> 
> checker observer_model(bit valid, reset);
> 
>         default clocking @$global_clock;
> 
> freevar bit flag;
> 
> m1: assume property (reset |=> !flag);
> 
> m2: assume property (!reset && flag |=> flag);
> 
> m3: assume property (!$rising_gclk(flag) |-> valid);
> 
> endchecker : observer_model
> 
> In this example the free variable flag behaves as follows:
> 
>  If it is high it remains high as long as there is no reset.
> 
>  If there is a reset it becomes low.
> 
>  It may become high only when valid is high.
> 
> Note that although the behavior of the free variable flag has been
> restricted by the assumptions m1, m2,
> 
> and m3, it is still non-deterministic because it does not have to become
> high when valid is high. Figure
> 
> 16.17 (Note to editor: please insert a correct figure number) shows two
> possible legal behaviors of this
> 
> variable given the same behaviors of reset and valid.  Note to editor:
> please number consistently with rest of chapter.
> 
> In simulation, a tool implementation-dependent decision may be made to
> use one of the following simulation methods to implement the
> non-deterministic choice:
> 
>  Symbolic simulation, where all possibilities are represented.
> 
>  Random values chosen at simulation time.
> 
>  Default values for their type used at simulation time.
> 
> [Korchemny, Dmitry] Unfortunately, the simulation semantics of the
> assumptions in the LRM has not been sufficiently elaborated. The free
> variables don’t introduce anything new here, the same issue exists with
> the plain inputs as well. The problem we face her is that the SVA
> assumptions play two different roles: they check the behavior of the
> environment or they model the environment. Consider the following example:
> 
> module m (logic a …);
> 
>             …
>             assume property(@clk a || b);
>             …
> 
> endmodule
> 
> In its first role this assumption acts as an assertion in simulation, it
> checks that the environment  ensures that always either a or b have a
> high value. In the second case the assumption acts as a constraint in
> simulation: the simulator should infer that the only legal values of a
> and b are a == 1 or b == 1 and GENERATE these values. Therefore the
> simulator may act either as an observer (“checker”), or as a value
> generator (constraint solver). Unfortunately these roles are not
> distinguished syntactically, and the tool has to infer them using some
> internal algorithm, which is not described in the LRM. Exactly the same
> situation occurs with the free variables, and for the example from the
> proposal you cited the constraint solving is more appropriate than the
> assertion checking. A cleaner way would be to introduce different
> keywords for these two roles, e.g., to keep “assume” for observing, and
> to introduce “model” for constraints:
> 
> model property(@clk a || b);  // Generate appropriate values of a and b
> using this constraint
> 
> Note that there is no distinction between assume and model for formal
> verification.
> 
> Though the issue you raised is closely related to the free variables, I
> would keep it as a separate one. Should we open a new Mantis for it?
> 
> 2. I think that this proposal needs to be split into smaller chunks. 30
> pages is a lot for one proposal, and it may come down to all or nothing.
> The free variables is a major chunk that could be separated.  There is
> also discussion on global clock and scheduling that does not need to be
> here.
> 
> [Korchemny, Dmitry] This is a challenge. If we separate free variables
> then the remaining checker may contain nothing but assertions. In this
> case the added value of checkers becomes unclear, and there is a big
> overhead in splitting this proposal, and then to write two incremental
> proposals instead of it. Global clock in checkers may be moved into a
> separate proposal. As for the scheduling is concerned, I think that
> without it the checker proposal is incomplete.
> 
>  3. This is kind of a silly question. Do you need to explicitely state
> that comments are allowed in checkers?  It is not in the list of things
> allowed, but I’m not  sure if others do either.  Of course we want to
> allow comments.
> 
> [Korchemny, Dmitry] I will ask Shalom whether it needs to be explicitly
> stated. There is no doubt that we want to allow comments in checkers.
> 
> Lisa
> 
> ---------------------------------------------------------------------
> 
> 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 <http://www.mailscanner.info/>*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. *

-- 
---------------------------------------------------------------------
Neil Korpusik                                     Tel: 408-276-6385
Frontend Technologies (FTAP)                      Fax: 408-276-5092
Sun Microsystems                       email: neil.korpusik@sun.com
---------------------------------------------------------------------



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