RE: [sv-ac] Recommended Items to Work and Study on the Next P1800 Revision

Hello Ben,

I would like to see one practical example that works well in formal and simulation, one that cannot be done by using existing means. IMHO, complexifying the language is not always good. Even as it stands now, people have enough problems understanding the intricacies of SV (and SVA).

Thanks and Happy New Year!

ed

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of Ben Cohen
Sent: Wednesday, December 31, 2014 1:46 PM
To: Korchemny, Dmitry
Cc: sv-ac@eda.org; Karen Pieper; IEEE P1800 Working Group (ieee1800@eda.org) (ieee1800@eda.org)
Subject: Re: [sv-ac] Recommended Items to Work and Study on the Next P1800 Revision

Added the following note to the mantis:
Solutions 1, 2, 3 all lead to the conclusion the need to have a local variable accessible to all concurrent assertions and siblings, and thus, it must somehow be tagged or qualified as special (e.g., with the $set_freeze, $probe, or a qualifier for the variable) .  This lead to solution 4, which provides the least impact to changes.  We could tag that special local variable with a qualifier "local" or even "global" since it is, in effect, global to the property.
The question arises: what happens if this "globally local" variable is read before it is written?  I believe that it is up to the user to insure this condition.  The value read if not written is the defaulted or initialized value.  Below is a potential solution as to how a user can be sure that the variable is written before it is read; this is a coding style, rather than something the tool must verify.

module m4571_4;
  bit clk, a, b, c, d, e;
  logic[31:0] x, y, z;
  property p1;
    local logic[31:0] v='bX; //  could also be
                         // global logic[31:0] v='bX;
     (a ##[1:$](b, v=x)) or
     (c ##[1:$] !$isunknown(v) ##1 c ##0 y==v);
   endproperty p1;
...

On Mon, Dec 29, 2014 at 10:43 AM, Ben Cohen <hdlcohen@gmail.com<mailto:hdlcohen@gmail.com>> wrote:
Dmitry and all,
I uploaded mantis_4571 that discussed the issues and provides 2 promising solutions.
Please review and comment for the next meeting.
http://www.eda-stds.org/svdb/view.php?id=4571

Thanks,
Ben

On Sun, Dec 28, 2014 at 4:43 AM, Korchemny, Dmitry <dmitry.korchemny@intel.com<mailto:dmitry.korchemny@intel.com>> wrote:
Hi all,

Per Karen request, I will call a meeting next Monday to discuss the feasibility of 4571.

Thanks and Happy Holidays,
Dmitry

From: Karen Pieper [mailto:karen_l_pieper@yahoo.com<mailto:karen_l_pieper@yahoo.com>]
Sent: Saturday, December 27, 2014 00:06
To: Korchemny, Dmitry; IEEE P1800 Working Group (ieee1800@eda.org<mailto:ieee1800@eda.org>) (ieee1800@eda.org<mailto:ieee1800@eda.org>)
Cc: 'sv-ac@eda.org<mailto:sv-ac@eda.org>'
Subject: Re: [sv-ac] Recommended Items to Work and Study on the Next P1800 Revision

Can the SV-AC please start the study on the feasibility of 4571, and advise at the P1800 review meeting what is known, likely schedule requirements, and suggested path forward?

Thanks,

Karen

________________________________
From: "Korchemny, Dmitry" <dmitry.korchemny@intel.com<mailto:dmitry.korchemny@intel.com>>
To: "IEEE P1800 Working Group (ieee1800@eda.org<mailto:ieee1800@eda.org>) (ieee1800@eda.org<mailto:ieee1800@eda.org>)" <ieee1800@eda.org<mailto:ieee1800@eda.org>>
Cc: "'sv-ac@eda.org<mailto:sv-ac@eda.org>'" <sv-ac@eda.org<mailto:sv-ac@eda.org>>
Sent: Thursday, December 25, 2014 6:30 AM
Subject: [sv-ac] Recommended Items to Work and Study on the Next P1800 Revision

SV-AC: Recommended Items to Work and Study on the Next P1800 Revision

Following internal discussions, SV-AC recommends to work on the following mantis items:

•        3057: Make local variables a first class language construct in SVA
•        5063: Allow tools to infer 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

SV-AC recommends to study the feasibility of the proposal:
•        4571: For next 1800: Probing property local variables for sharing across boundaries

SV-AC requests from SV-CC to address the proposal:
•        2182: Ballot comment 56: Elaborate VPI diagrams for checkers

SV-AC recommends to create a cross-P1800 group to study the following proposal and to elaborate recommendations for the future work:
5068: concurrent assertions in classes

Also, SV-AC recommends to work on errata and clarification items.

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



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