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

Hi Neil,

I agree with you that the random simulation of the non-deterministic free variables is useful, and the repeatability issue for it is important. And of course, the definition must be consistent with the rest of the language.

However, the random simulation is not the only possible way to simulate the non-deterministic free variables. Consider the following example (this example may be rewritten in a more efficient/intuitive manner, but it is immaterial for our discussion):

// write_data and read_data are 32-bit long
freevar bit [31:0] data;

// Always stable at the sampling points
assume property((@posedge clk) ##1 $stable(data));

// Data read is identical to the data previously written
assert property((@posedge clk) write && write_data == data ##1 read[->1] |-> read_data == data);

If we use a random simulation here, we will check only one randomly selected case, say when the data is 32'h9AC01752. It is most likely that this value will never be written during the simulation, and the assertion will almost always pass vacuously. What the user expects in this case is to check the assertion for every possible value of data during the simulation. This may be done either integrating a simulator with a formal verification engine, or using some rewriting techniques.

Therefore, the definition of the behavior of non-deterministic free variables in simulation is not straightforward, and I think it is too early to fix it in the standard, since any change in the future will be not backward compatible. Maybe additional syntax has to be developed to address different implementations of non-deterministic free variables in simulation. It seems unrealistic to develop a sound definition in the remaining time frame. In order to avoid the backward compatibility issues it was suggested in SV-AC to state in the current proposal that the simulation of the non-deterministic free variables should be illegal.

Nevertheless, the non-deterministic free variables are important for formal verification, and many formal specification languages have them. E.g., PSL has its own modeling layer and has nondet(), nondet_vector() functions and union expression to address the same issue. The only alternative to the non-deterministic free variables for formal verification is dummy free primary inputs, which is extremely clumsy. Using free inputs in the simulation makes the things worse, since most of the assertions and assumptions using these inputs will likely fail. I don't think that the professional FV activity is possible without having non-deterministic free variables in the language. One of our goals is to make SVA suitable for FV people, and not to make them use PSL or other formal specification languages with SV designs.

I believe that we will be able to elaborate simulation semantics for non-deterministic free variables in the future.

Thanks,
Dmitry

-----Original Message-----
From: Neil.Korpusik@Sun.COM [mailto:Neil.Korpusik@Sun.COM] 
Sent: Tuesday, October 16, 2007 3:04 AM
To: Korchemny, Dmitry
Cc: sv-ac@eda-stds.org
Subject: 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
---------------------------------------------------------------------
---------------------------------------------------------------------Intel Israel (74) Limited
This e-mail and any attachments may contain confidential material forthe sole use of the intended recipient(s). Any review or distributionby others is strictly prohibited. If you are not the intendedrecipient, please contact the sender and delete all copies.
-- This message has been scanned for viruses anddangerous content by MailScanner, and isbelieved to be clean.