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

Korchemny, Dmitry wrote:
> Yes, they have, but are they required having them? 

Certainly they are, unless you don't want to implement the random
constraint portions of the LRM.

I do however mostly agree that it would be a very bad idea to
(even implicitly) require formal provers in a simulator.

Gord

 >  Also, it is not
> always straightforward to use constraint-solving technology to solve the 
> temporal constraints,
> 
>  
> 
> Dmitry
> 
>  
> 
> ------------------------------------------------------------------------
> 
> *From:* Bresticker, Shalom
> *Sent:* Wednesday, April 09, 2008 4:49 PM
> *To:* Korchemny, Dmitry; Mirek Forczek; sv-ec@server.eda.org
> *Cc:* sv-ac@server.eda.org
> *Subject:* RE: [sv-ac] RE: [sv-ec] 1900 mantis (checkers): checker 
> variable semantics: interoperability and portability issues.
> 
>  
> 
> But simulators already have to have constraint solvers?
> 
>  
> 
> Shalom
> 
>      
> 
>     [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).
> 
>      
> 
> ---------------------------------------------------------------------
> 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.

-- 
--------------------------------------------------------------------
Gordon Vreugdenhil                                503-685-0808
Model Technology (Mentor Graphics)                gordonv@model.com


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