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.Received on Thu May 12 10:54:27 2011
This archive was generated by hypermail 2.1.8 : Thu May 12 2011 - 10:54:33 PDT