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
> 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 MailScanner <http://www.mailscanner.info/>, and is
> believed to be clean. 


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