[sv-ac] RE: ensure vs. verify

But the standard defines (mostly) simulation semantics, not FV semantics.

Shalom

________________________________
From: Korchemny, Dmitry
Sent: Sunday, December 07, 2008 5:27 PM
To: Bresticker, Shalom; sv-ac@server.eda.org; stuart@sutherland-hdl.com; Neil.Korpusik@sun.com
Subject: RE: ensure vs. verify

Hi Shalom,

I don't think that 'verify' or 'validate' is appropriate here. Consider the following example:

module m(logic read, write, ...);
                m1: assume #0 ($onehot0({read, write}));
                ...
                a1: assert property(...);
endmodule

We want to assume here that the signals read and write are mutually exclusive. In simulation we do verify the assumption correctness: if the environment violates this assumption, the assumption violation is reported. But for the formal verification this is not true: all assertions are proved only for cases when read and write are mutually exclusive. When this is not true, the assertions (e.g., a1) are not guaranteed (sorry for using this word here :)) to hld. We do not verify the assumption m1 at all, but just assume it is correct.

Dmitry

From: Bresticker, Shalom
Sent: Sunday, December 07, 2008 5:18 PM
To: Korchemny, Dmitry; sv-ac@server.eda.org; stuart@sutherland-hdl.com; Neil.Korpusik@sun.com
Subject: RE: ensure vs. verify

No, I think that 'verify' or 'validate' is more appropriate here.

The reason that 'ensure' is not appropriate, at least from IEEE point of view, is that if the input stimulus does not conform to assumed requirements, the existence of assertions does not cause them to be so. The assertions only flag that they are not so.

For IEEE, the term 'ensure' involves legal responsibility, which has particular significance in safety-related issues.

Shalom

________________________________
From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On Behalf Of Korchemny, Dmitry
Sent: Sunday, December 07, 2008 5:03 PM
To: sv-ac@server.eda.org; stuart@sutherland-hdl.com; Neil.Korpusik@sun.com
Subject: [sv-ac] ensure vs. verify
Hi all,

Following IEEE requirements the editor has changed "ensure" and "guarantee" with other words. One such example is the beginning of 16.2:

An assertion specifies a behavior of the system. Assertions are primarily used to validate the behavior of a
design. In addition, assertions can be used to provide functional coverage and to ensure verify that input
stimulus that is used for validation conforms to assumed requirements.

IMO "ensure" is much better suited here than "verify", since in formal verification the assumptions normally cannot be verified unless you consider them in a larger context. Therefore I am curious whether better suggestions are available.

Neil, is it compulsory to change the world "ensure" in this case? If not, I would prefer to keep it unchanged.

Thanks,
Dmitry

---------------------------------------------------------------------

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