Hi Dmitry, I've listen this discussion very carefully. The most important conclusion IMHO was: the SV LRM no longer refer to the single (simulation) semantic only, rather than it refer to the at least three different (in nature) semantics now: the (event-based) simulation, formal checking and symbolic simulation were mentioned. The simulation semantics seems to keep dominate position in LRM text, but certain paragraphs start to refer other semantics now ... But the basic problem is: only the simulation semantic's foundation is well defined in LRM - this is chapter 9 "Scheduling semantics". This is where any "semantics" shall start at all in the SV LRM ... I think this chapter shall be extended with foundation definitions for the other two semantics (formal checking and symbolic simulation), the today contant of the chapter shall become sub-paragraph. It does not imply whole LRM text shall tripled immediately - initally we can assume the today content apply to the all semantics unless it is specified otherwise for particular construct. Than only specific constructs can be supplemented with definitions for a new semantics. With such document organization, dealing with things like "free checkvar" will be much more easy: The LRM text can contain full definition of some construct (i.e.: the "free checkvar") semantics for one domain (i.e: formal checking), without need to provide full mapping of that content into the other semantics domain (i.e.: simulation) if it (obviously) do not fit at all. For another domain a completely different semantics definition could be made - in particular: an empty one - the construct shall be ignored by a tools that implement such semantics. (this is not exactly the case for "free checkvar" probably - "free checkvar" is expected to act like random-constrained variable in simulation, but still this demonstrates that different domains may require different semantins explained for a construct - on a basis of different fundametals of the domain.) All this is not possible without having good foundation chapter for multiple semantics ... Regards, Mirek _____ From: Korchemny, Dmitry [mailto:dmitry.korchemny@intel.com] Sent: 9 kwietnia 2008 15:39 To: Mirek Forczek; sv-ec@server.eda.org Cc: sv-ac@eda.org Subject: RE: [sv-ec] 1900 mantis (checkers): checker variable semantics: interoperability and portability issues. Hi Mirek, We started discussing this issue at our yesterday meeting, See some more comments below. Thanks, Dmitry _____ From: owner-sv-ec@server.eda.org [mailto:owner-sv-ec@server.eda.org] On Behalf Of Mirek Forczek Sent: Monday, April 07, 2008 2:37 PM To: sv-ec@server.eda.org Subject: [sv-ec] 1900 mantis (checkers): checker variable semantics: interoperability and portability issues. In "16.18.6 Checker variables" section of the proposal there is: "Simulators shall assign arbitrary values to the free checker variables provided that these values are consistent with the free checker variable assignments; they also may use the assumptions to constrain these values if they have the capability to do so. If the values assigned by a simulator contradict some of the assumptions, the simulator shall report a violation of the corresponding assumptions. The simulator shall report a violation of an assertion containing free checker variables if the assertion is violated for the values of the free checker variables assigned by the simulator. Optionally the simulator may choose to check the assertions for all possible values of the free checker variables imposed by the assumptions and assignments if it supports relevant formal verification techniques, e.g., if it supports model checking on the fly." The style of some sentences: may(/may-not ?), if they have capability, optionally - make a potential threat to interoperability and portability, IMHO. With the same input (source code) simulators are allowed to work in a different manner. [DK] Yes. the interoperability is important, but let's ask a different question: given two different formal tools checking the same assertion, would you expect that both tools would generate the same counterexample? To achieve it you have to standardize the verification strategy, the model checking algorithms and its parameters, search heuristics, SAT solvers, etc. The situation in our case is very similar. The sentence: "If the values assigned by a simulator contradict some of the assumptions, the simulator shall report a violation of the corresponding assumptions." rise a questions: - once the assumptions were specified in a source code, what is the point to assign by a simulator the values that obviusly will contradict with the assumptions, to check the assumptions after that and report violation ? [DK] There are several reasons for doing that. One is that the assumptions may be contradictory or contradict the RTL. The other reason is not to require from a simulator to have an embedded formal verification engine. Without such an engine you cannot guarantee to satisfy all the assumptions (and even with it you can have a blow-up). Wouldn't it be better to obligate simulator to check the new values against assumptions before an assignment and not to assign them if they violate assumptions, just to select another one .. ? [DK] See my previous comment. - is it good idea to allow simulators decide whether to ignore the assumptions or not, without any explicit directive in source code ? [DK] Same. It is good idea to classify and organize checker variable semantics accordingly to the assumed simulator capabilites, but it would be better to have strictly defined behaviour for particular syntax. [DK] ? More advanced semantics could be denoted with additional directives or additional options to the existing directives/declarations. An advanced semantics - once denoted in a source code - shall obligate simulator to follow them. Users shall be aware of their simulator limits and to achieve code portabiity an advanced directives could be explicitly placed under conditional compilation (which is a popular coding style to achieve code portability). [DK] See my previous comment. Regards, Mirek --------------------------------------------------------------------- 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, and is believed to be clean. -- This message has been scanned for viruses and dangerous content by MailScanner, and is believed to be clean.Received on Wed Apr 9 08:19:30 2008
This archive was generated by hypermail 2.1.8 : Wed Apr 09 2008 - 08:19:45 PDT