Re: [sv-ac] FW: [sv-ec] 1900 mantis (checkers): checker variable semantics: interoperability and portability issues.

Hello everyone,

This text was the result of a compromise.

In the 1800-2005 standard, the assume property construct was defined as 
follows (clause 17.13.2):

> "The purpose of the assume statement is to allow properties to be considered as assumptions for formal
> analysis as well as for dynamic simulation tools. When a property is assumed, the tools constrain the environment
> so that the property holds.
 >
> For formal analysis, there is no obligation to verify that the assumed properties hold. An assumed property
> can be considered as a hypothesis to prove the asserted properties.
 >
> 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. There is no requirement
> on the tools to report successes of the assumed properties."

Essentially, formal verification tools may use the assume propery 
construct to determine what the legal input values are on a signal. A 
simulator, however simply treats the assume property the same way as an 
assert property.

The initial proposal for Mantis 1900 said that any tool (formal or 
simulation) would use assume property constructs to determine valid 
values for free variables.  However, I felt that this was changing the 
semantics of assume property.  If the assume property construct was used 
to set the values of free variables in simulation, shouldn't they also 
be used to set the values of unconnected inputs of a module, for 
example, rather than setting those inputs to X?

I proposed text that mirrored the existing text in 17.13.2.  However, it 
was argued that certain specialized simulators do have constraint 
solvers that can solve temporal properties, and there are several 
techniques like model checking on the fly which use this capability. 
These types of simulators should set the values of free variables based 
on the assume property statements.  The result is the text you see in 
the Mantis 1900 proposal.

Tom


Bresticker, Shalom wrote:
>  
> 
> ------------------------------------------------------------------------
> *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.
> 
>  
> 
> 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* <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* <http://www.mailscanner.info/>, and is
> believed to be clean.

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