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

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
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. 

---------------------------------------------------------------------
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.