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

 

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 ?

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

- is it good idea to allow simulators decide whether to ignore the
assumptions or not, without any explicit directive in source code ?

 

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.

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

 

Regards,

Mirek

 

 

 

 

 

 


-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.