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

 

 

 

 

 

 


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