Re: [sv-ac] Items would like to address at upcoming meetings

Scott,
1) let me think about the 'const.
2) .. a new concept (a local variable that is only assigned once in the
antecedent and can therefore be used more freely throughout the assertions
language) but then the new construct is limited to being read in the
consequent of the of implies or in the antecedent (but not in the same
cycle where the local variable is assigned if in the antecedent).

3) Why, for instance would I not be able to use it in the antecedent of |->
or |=>?
Actually, you could. That's a good idea. In both cases (the implies or the
|-> or |=>) the antecedent is a sequence.

I understand that the restrictions are somewhat bothersome; however, they
are needed. This is why we currently have rules about the flow out of local
variables when used with "and", "or", "intersect" and "implies" (BTW, the
LRM does not directly address the "implies", most likely because it is
equivalent to "not A or B").
Thanks,
Ben

On Thu, May 12, 2011 at 11:46 AM, Little Scott-B11206
<B11206@freescale.com>wrote:

> Hi Ben:
>
>
>
> 1) I understand that. What about another keyword that might make more
> sense? I haven’t thought about it carefully and don’t know SV well enough
> to foresee many potential issues, but what about using ‘const’? To me,
> ‘const’ is closer to how you are defining this construct (see the definition
> of instance constants in 8.18 for a similar capability).
>
>
>
> 2) I wasn’t clear enough on point 2. My concern isn’t with the
> restrictions you enumerate below. In fact, they seem to be needed as you
> illustrate below. My concern is that this proposal introduces a new concept
> (a local variable that is only assigned once and can therefore be used more
> freely throughout the assertions language) but then the new construct is
> limited to being used in the antecedent of implies and nowhere else. I
> would prefer to see more thought put into how this additional freedom with
> local variables can be used across SVA. Why, for instance would I not be
> able to use it in the antecedent of |-> or |=>?
>
>
>
> Thanks,
>
> Scott
>
>
>
> *From:* ben cohen [mailto:hdlcohen@gmail.com]
> *Sent:* Thursday, May 12, 2011 12:53 PM
> *To:* Little Scott-B11206
> *Cc:* Korchemny, Dmitry; sv-ac@eda-stds.org
>
> *Subject:* Re: [sv-ac] Items would like to address at upcoming meetings
>
>
>
> Scott,
>
> 1) On "automatic", I was just trying to avoid another keyword.
>
> 2) On the restrictions, they were derived out of necessity. To explain,
> consider the following case (am using automatic for now:
>
> property P_problematic;
>
> automatic int v1, v2;
>
> (##0 (a, v1=dt)) and // <-- sq1
>
> (##0 (b, v2=ad) and // <-- sq2
>
> (##1 (v1==10, v2=100)) and // <-- sq3
>
> (##1 (v2==20, v1=0) // <-- sq4
>
> implies w;
>
> endproperty : P_problematic
>
> The issue is that the ordering of processing is not guaranteed (i.e., is
> sq2 processed before sq3?) because the sequences being ANDed are concurrent.
> In addition, even if the ordering were known, one of those sequence may use
> variables used by another ANDed sequence. That is demonstrated in sq3 and
> sq4. If the ordering of the processing is defined (e.g., sq3 is processed
> before sq4), then reversing the order of sq3 and sq4 would yield different
> results. That is not acceptable. To avoid these issues, I had to add the
> following restrictions:
>
> a) The local variable can be set once, and only once, in the antecedent of
> the implies operator but it can be read anywhere from within the property
> statement, including across all branching expressions like implies, and, or,
> and intersect.
>
> b) In the antecedent of the implies operator it shall be illegal for an
> automatic local variable to be read and written in the same cycle within the
> branching expressions like implies, and, or, and intersect.
>
> c) Also, in the consequent of the implies operator it shall be illegal for
> an automatic local variable to be written in any cycle within the branching
> expressions like implies, and, or, and intersect.
>
> d) The antecedent of the implies is always computed first before the
> consequent.
>
> e) It shall be illegal to declare an automatic local variable in a
> sequence declaration (because it does not make sense to have them there).
>
>
>
> 3) This style allows the use of timing diagrams using timing information
> (e.g., @ cycle x this, @cycle y that. See http://bit.ly/lJmc9A for
> another example.
>
>
>
> Have you considered other operators where this might be useful (|-> for
> instance)? If the capability is useful, then I would prefer to see a
> proposal that enables the functionality across all SVAs as appropriate.
>
> I open to ideas.
>
> Thanks,
>
> Ben
>
>
>
> On Thu, May 12, 2011 at 5:59 AM, Little Scott-B11206 <B11206@freescale.com>
> wrote:
>
> Hi Ben:
>
>
>
> I took a brief look at 3195 and have some high-level concerns.
>
>
>
> I find the choice to use the keyword automatic for these variables
> confusing. Automatic has meaning in the rest of the LRM and it doesn’t mean
> a variable that can only be assigned once. I understand the desire to not
> add keywords, but I don’t think the choice of automatic works well.
>
>
>
> The restrictions for the use seem quite severe (only w/ implies). It is
> clear that you have a specific use case and coding style in mind. The
> proposal allows for this use case/coding style and nothing more. Have you
> considered other operators where this might be useful (|-> for instance)?
> If the capability is useful, then I would prefer to see a proposal that
> enables the functionality across all SVAs as appropriate.
>
>
>
> I would expect to see some changes to the formal semantics for this, but
> those are missing from the proposal.
>
>
>
> Thanks,
>
> Scott
>
>
>
> *From:* owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] *On Behalf Of *ben
> cohen
> *Sent:* Thursday, May 12, 2011 12:59 AM
> *To:* Korchemny, Dmitry
> *Cc:* sv-ac@eda-stds.org
> *Subject:* Re: [sv-ac] Items would like to address at upcoming meetings
>
>
>
> Dmitry,
>
> Thanks. Can we add 3552 and 3195 to next week's agenda?
>
> On 3478, can you please seek permission, as this issue deals with a very
> important missing feature of SVA to address bi-directional IOs.
>
> Thanks,
>
> Ben
>
>
>
> On Wed, May 11, 2011 at 10:53 PM, Korchemny, Dmitry <
> dmitry.korchemny@intel.com> wrote:
>
> Hi Ben,
>
>
>
> You are welcome to address issues 3552 and 3195. We are not authorized to
> address 3478.
>
>
>
> Thanks,
>
> Dmitry
>
>
>
> *From:* ben cohen [mailto:hdlcohen@gmail.com]
> *Sent:* Thursday, May 12, 2011 02:31
>
>
> *To:* sv-ac@eda-stds.org; Korchemny, Dmitry
> *Subject:* [sv-ac] Items would like to address at upcoming meetings
>
>
>
> Dmitry,
>
> Below is a list of items I would like us to address:
>
> *Make drivers of inout ports accessible*
>
> http://www.eda-stds.org/svdb/view.php?id=3478
>
> Uploaded a new version of the mantis.
>
> I also uploaded a diagram (extdriver.pdf) clarifying the meaning of those
> functions in a DUT instantiated in a testbench.
>
>
>
> *16.14.6 Sequence methods // .triggered need further clarification*
>
> http://www.eda-stds.org/svdb/view.php?id=3552
>
> Made some updates
>
>
>
> *Local Variables Flow Out Issue in and/or/intersect/implies*
>
> http://www.eda-stds.org/svdb/view.php?id=3195
>
> Made some updates
>
>
>
> I also welcome comments on these topics.
>
> Ben Cohen SystemVerilog.sv
>
> ---------------------------------------------------------------------
> 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.