Hi Lisa, Please, see my comments below. Thanks, Dmitry ________________________________ From: Lisa Piper [mailto:piper@cadence.com] Sent: Friday, September 28, 2007 3:45 AM To: Korchemny, Dmitry Cc: sv-ac@eda-stds.org Subject: RE: more on 1900 checkers Hi Dmitry, Thanks for the response and sorry for the long silence from me. I wanted to think about it and bounce it off my peers. ________________________________ From: Korchemny, Dmitry [mailto:dmitry.korchemny@intel.com] Sent: Tuesday, September 25, 2007 8:14 AM To: Lisa Piper Cc: sv-ac@eda-stds.org Subject: RE: more on 1900 checkers 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? [Lisa Piper >>>] While it is possible for a simulator to do this, the current baseline (LRM) semantics for both assume and assert is that they are treated as checkers in simulation. In 16.14.2 it states: “For simulation, the environment must be constrained so that the properties that are assumed shall hold. Like an assert property, an assumed property must be checked and reported if it fails to hold” [Korchemny, Dmitry] If assumptions are interpreted as assertions, they will just fail in the simulation in these cases. One solution to this problem is to state that simulation tools are not required to support assertions/assumptions containing non-deterministic variables, and that they may ignore these assertions. However non-deterministic free variables are important for formal verification. .If a given tool is able to interpret an assume about primary inputs as a constraint that will be satisfied by a constraint solver, then it may do so - but there should not be any requirement that all simulators be able to do this. And I don’t think another keyword would solve the problem because the simulator will either have the capability or not. [Korchemny, Dmitry] Another keyword would not solve the problem of the constraint-based simulation for the tools that don’t have this capability, but it will solve the problem for the tools that do have it. Also, how do you plan to handle assumes about internal signals? [Korchemny, Dmitry] This question is not quite clear to me. Will immediate assumes be treated differently than concurrent assumes? If I remember correctly you don’t have immediate assumes in a checker, so does this rule only apply to assertions in the checker (you may have answered that already – I don’t remember)? [Korchemny, Dmitry] Currently there immediate assertions are not allowed in the checker. Another issue I see is that you will likely apply a checker to an interface where in one case a signal is an output of the interface and in another case interface it is an input (a master-slave interface for example). It would be more powerful if the checker can determine whether it needs to drive the signals independent of whether the verification directive is an assert or an assume. [Korchemny, Dmitry] I think this problem is not related directly to checkers. When the signals are sometimes inputs and sometimes outputs in the interface, even writing a plain assertion/ assumption will have the same problem. One option is to let the tool to decide. Other options will require language extensions. 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. --------------------------------------------------------------------- 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.Received on Sun Sep 30 19:56:11 2007
This archive was generated by hypermail 2.1.8 : Sun Sep 30 2007 - 19:56:47 PDT