RE: [sv-ec] 1900 mantis (checkers): checker variable semantics: interoperability and portability issues, an optional embedded formal verification engine

From: Mirek Forczek <mirekf_at_.....>
Date: Wed Apr 09 2008 - 08:54:55 PDT
Hi Dmitry,
 
About checking the assumptions of checkvars:
 
1)
- 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. [...]


In such case the tool shall report: it is not able to find satifiable value
for checkvar to meet the assumptions -> probably the assumptions are
contradictory or contradict the RTL.

 

2)

[...] 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).

That's true, and following later discussion:

    simulators are required to have the embedded formal verification engine
in order to be SV-compliant, but for number of reasons (i.e.: price) they
may be delivered to the users without this option,
    they will become non 100% SV-compliant than of course, but still they
may be usable for users,
 
now - depending on how the optional semantics (such as checking the
assumptions of checkvars) is expressed with language syntax - the use of non
100% SV-compliant tools can cause more or less interoperability and
portability issues.

In my opinion:

- a freedom level such as: may(/may-not ?), if they have capability,
optionally shall be avoided in LRM,

- a clear rules shall be defined when optional semantcis apply, and ones it
apply it shall be obligatory for a tool

- the syntax for enabling an optional semantics shall be constructed in way
it is possible to ommit it, while still preserving the basic syntax and
semantics of the construct.

i.e.:

    it would be better to define something like:

a)

(a declaration property/extension style):

        free checkvar a; // assumptions are not checked

        free validate checkvar b; // assumptions have to be validated while
assignment

(a separate directive style):

        validate c; // explicit command to obligate assumptions checking for
'c'        

(of course and new keyword is another pain - this is just an idea example)

 

    than to define:

b)

        free checkvar d; // assumptions may(/may-not ?) be checked ... :(


 

In b) the model behaviour become not portable, only the syntax is portable
...,

in a) the model behaviour will be portable, and the syntax will help detect
use of non 100% compliant tool: 

    such tool will be allowed to simulate a basic syntax version, but shall
rise an error/warning ("not supported constuct") in case of extended syntax.

    Also additional level of code portability can be achieved with
conditional preprocessor directives than.

 

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:57:46 2008

This archive was generated by hypermail 2.1.8 : Wed Apr 09 2008 - 08:58:00 PDT