RE: [sv-ac] Feedback request

Hi all,

I would like to comment regarding the importance of assertion inference:

The LRM states the following (16.2 Overview):

An assertion appears as an assertion statement that states the verification function to be performed. The statement shall be of one of the following kinds:
— assert, to specify the property as an obligation for the design that is to be checked to verify that the property holds.
— assume, to specify the property as an assumption for the environment. Simulators check that the property holds, while formal tools use the information to generate input stimulus.

This definition contradicts using assertions as assumptions in formal verification. The fact that most FV tools know how to handle this situation just means that their behavior contradicts the standard. Because nobody wants to make their behavior compliant to the standard, the standard must be changed to make such behavior legal, and define the desired degree of freedom of assertion inference.

There may be an entire spectrum of solutions, starting from adding a clarification that the formal tools may infer the meaning of assert statement freely to introducing a special syntax for assertion inference and defying strict rules how to infer assertion meaning in each case. I think that the right approach is somewhere in the middle. But in any case the problem has to be handle.

One more thing. I think that the explanation of assume statement should be modified: assume does not serve to generate input stimuli by formal tools by to restrict the legal traces. Assumptions may be used to generate input stimuli for test generation tools.

Thanks,
Dmitry

From: Ben Cohen [mailto:hdlcohen@gmail.com]
Sent: Monday, November 24, 2014 20:01
To: Korchemny, Dmitry
Cc: sv-ac@eda.org
Subject: Re: [sv-ac] Feedback request

On
​
5063: Automatic inference of assertion statement type
I am changing my feedback to "nice to have", but I have concerns about usage, as this will add complications to SVA and possible misunderstandings.  Also, isn't this a tool issue rather than a language issue? This topic needs discussion at our next meeting.
Thanks,
Ben

On Fri, Nov 21, 2014 at 3:47 AM, Korchemny, Dmitry <dmitry.korchemny@intel.com<mailto:dmitry.korchemny@intel.com>> wrote:
Hi,

You are requested to send your feedback on working on the following Mantis items in the next P1800 PAR by 1-Dec-2014, UTC:


•        3478: Make drivers of inout ports accessible

•
​​
​​
5063: Automatic inference of assertion statement type

•        5064: Create standard package to define constants used in assertion-related stuff

•        5065: Create standard package to define implementation for commonly used properties

•        5067: Allow variables in delays and repeat operators

•        5068: concurrent assertions in classes

Your feedback should include one of the following marks for each item:

•        Important

•        Nice to have

•        Not important

•        No opinion
along with any free text comments.

You may also suggest additional enhancements not listed above, but they need to be filed as Mantis items first.
There is no need to discuss any errata or clarification items.

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.