RE: [sv-ac] updated proposal for AC 296

Hi Ed,

I was under the impression (from the discussion on the reflector) that
$past
on ended will not work as its sampled value will never be true (As per
LRM:
$past returns the sampled value of the expression that was present
number_of_ticks
prior to the time of evaluation).

Are you suggesting that $past on ended will be defined differently as it
is
used only in assertions ? If that is the case then, $rose, $fell and
$stable will also work for ended.

Thanks.
Manisha

-----Original Message-----
From: Eduard Cerny [mailto:Eduard.Cerny@synopsys.com]
Sent: Thursday, November 18, 2004 8:33 AM
To: Kulshrestha, Manisha
Cc: Sv_Ac
Subject: RE: [sv-ac] updated proposal for AC 296

Hi Manisha,

I like your last version of the proposal, except for oine thing - from
the discussions on the reflector, it seems to me that there is no
problem in using $past on s.ended provided that the sampling clock is
the same as that of s and it is used only in the context of sequences.

Best regards,

ed
 

> -----Original Message-----
> From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of
> Kulshrestha, Manisha
> Sent: Wednesday, November 17, 2004 11:54 AM
> To: sv-ac@eda.org
> Subject: [sv-ac] updated proposal for AC 296
>
> Hi All,
>
> I have uploaded a new proposal for 296.
>
> Thanks.
> Manisha
>
> -----Original Message-----
> From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of
> Kulshrestha, Manisha
> Sent: Monday, November 15, 2004 10:45 AM
> To: Eduard.Cerny@synopsys.com; john.havlicek@freescale.com
> Cc: john.havlicek@motorola.com; sv-ac@eda.org
> Subject: RE: [sv-ac] RE: AC 296
>
> Hi All,
>
> It seems like using .triggered and .ended in sampled value functions
> will not work as per current LRM definition. And since sampled value
> functions can be applied to expressions (which can include these
> methods and other signals in a more complex expression), it is not
> easy to modify definition of sampled value functions for these
> methods. I think this topic needs more discussion.
>
> I can create a separate errata for later discussion to deal with this
> issue. I'll mention it in my proposal that the usage of these methods
> in sampled value functions is not supported as their values are not
> available in preponed region.
>
> Does that sound reasonable ?
>
> Thanks.
> Manisha
>
> -----Original Message-----
> From: Eduard Cerny [mailto:Eduard.Cerny@synopsys.com]
> Sent: Monday, November 15, 2004 10:04 AM
> To: Kulshrestha, Manisha; john.havlicek@freescale.com;
> Eduard.Cerny@synopsys.COM
> Cc: john.havlicek@motorola.com; sv-ac@eda.org
> Subject: RE: [sv-ac] RE: AC 296
>
> Hi Manisha,
>
> Regarding these system functions, the 3.1a LRM says "This section
> describes the system functions available for accessing sampled values
> of an expression. These functions include the capability to access
> current sampled value, access sampled value in the past, or detect
> changes in sampled value of an expression. Sampling of an expression
> is explained in Section 17.3. The following functions are provided."
>
> It refers to sampled values which in the case of ended does not make
> sense.
> We have two choices, it seems to me, not allow past etc. on ended or
> modify the definition of these functions to accept current values of
> ended. The reference to past would mean the value of ended at the
> preceding clock.
> Using $sampled would be invalid on ended. rose, fell, stabel would be
> OK.
>
> The question remains what about s.triggered in these functions when
> they are used outside assertions. I suppose this should be the same as

> applying the functions to any event e.triggered (if it has been
> defined
> - it does not seem so) However, given again that these functions
> operate on sampled values from the preponed region, using past etc. on

> triggered would not make sense
> - the sampled value (by the same clock as s) wouls always be false.
>
> ed
>
>
>
> > -----Original Message-----
> > From: Kulshrestha, Manisha [mailto:Manisha_Kulshrestha@mentorg.com]
> > Sent: Monday, November 15, 2004 12:48 PM
> > To: john.havlicek@freescale.com; Eduard.Cerny@synopsys.COM
> > Cc: john.havlicek@motorola.com; sv-ac@eda.org
> > Subject: RE: [sv-ac] RE: AC 296
> >
> > Hi All,
> >
> > Thanks John, Ed, Ben for discussing this issue and
> clarifying all the
> > different points.
> >
> > So, seems like it is OK to not allow .triggered in sequence
> > expressions as it might open up other issues which need better
> > clarification.
> >
> > Now, one question remaining is that is it valid to use .ended in
> > sampled value functions like $sampled, $past etc.
> > Since .ended is only valid in observe region, how it can be used in
> > these functions ?
> >
> > Thanks.
> > Manisha
> >
> > -----Original Message-----
> > From: John Havlicek [mailto:john.havlicek@freescale.com]
> > Sent: Monday, November 15, 2004 9:25 AM
> > To: Eduard.Cerny@synopsys.com
> > Cc: john.havlicek@motorola.com; Kulshrestha, Manisha; sv-ac@eda.org
> > Subject: Re: [sv-ac] RE: AC 296
> >
> > Hi Ed:
> >
> > I agree with your point about opening up too many issues by
> allowing
> > "triggered" in sequences. We don't have time for this, and I
> > certainly cannot take on responsibility for such a proposal.
> >
> > The main point of my message was not supposed to be "let's allow
> > triggered in sequences". Rather, I was trying to express
> differences
> > between "ended", "matched", and "triggered" that, to me,
> suggest that
> > we should keep the three distinct.
> >
> > Regarding events built from sequences, I don't know whether
> >
> > @(s.ended)
> >
> > should be legal. If
> >
> > @(s)
> >
> > is legal, then does it differ from
> >
> > @(s.triggered)
> >
> > ?
> >
> > Best regards,
> >
> > John H.
> >
> >
> > > Reply-To: <Eduard.Cerny@synopsys.com>
> > > From: "Eduard Cerny"<Eduard.Cerny@synopsys.com>
> > > Cc: <sv-ac@eda.org>
> > > Date: Mon, 15 Nov 2004 09:32:40 -0500
> > > Organization: Synopsys, Inc.
> > > Thread-Index: AcTKLLGWt7EOk/J8S7O29XMrc5vlOgA8YSkg
> > > X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2800.1441
> > >
> > > Hello John,
> > >
> > > I think that your proposal of handling ended vs. troggered in
> > > assertions is interesting. But if we do allow triggered in
> > sequences,
> > > such that it is true throughout the time step and allows
> > sync between
> > > inequivalent events, what is the validity of
> > $past(s.triggered)? Is it
> >
> > > now synced to the clock like
> > > $past(s.ended) and thus synthesizable? For any event e,
> is it then
> > > possible to use e.triggered within a sequence? Since the
> assertions
> > > are evaluated in the observed region and e could be
> emitted in the
> > > reactive region, how would that behave?
> > >
> > > It seems to me that allowing .triggered inside sequences
> > may open up a
> >
> > > lot of other issues that we may not have the time to resolve.
> > >
> > > ended as an event - I think this is hidden under @(s),
> > i.e., we do not
> >
> > > need
> > > @(s.ended) even though its meaning would be equivalent.
> Disallowing
> > > this would be a limitation, it is potentially quite useful
> > to trigger
> > > sampling of covergroups using @(s) (do not need a cover
> poperty to
> > > instantiate the
> > > sequence.)
> > >
> > > Allowing actual arguments in s(...).triggered is OK, for
> > reasons that
> > > you give. The system can do the instantiation under the hood.
> > >
> > > Best regards,
> > >
> > > ed
> > >
> > >
> > >
> > > > -----Original Message-----
> > > > From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On
> > Behalf Of
> > > > John Havlicek
> > > > Sent: Sunday, November 14, 2004 4:30 AM
> > > > To: Manisha_Kulshrestha@mentorg.com
> > > > Cc: sv-ac@eda.org
> > > > Subject: Re: [sv-ac] RE: AC 296
> > > >
> > > > Manisha and All:
> > > >
> > > > After thinking more about these questions I have a few comments.
> > > >
> > > > First, from the point of view of the assertions, there
> > has been from
> >
> > > > a long time ago a desire to ensure synthesizability of
> > the checkers.
> > > > Therefore, synchronizing constructs that could detect
> > simultaneity
> > > > of "inequivalent" events were disallowed. This
> > consideration led to
> >
> > > > the distinction between "ended" and "matched" in the
> assertions,
> > > > where "ended" is used to mean that the synchronization is
> > known to
> > > > be between equivalent clock events, while "matched" is
> > used when it
> > > > is not so known. When "matched" is used, simultaneity of
> > distinct
> > > > clock events is not detected.
> > > >
> > > > If "triggered" is allowed within the assertion code, then
> > it seems
> > > > to lie between the above partitioning of the synchronization
> > > > methods.
> > > > The semantics of "triggered" seems closest to "ended".
> > "triggered"
> > > > carries no latching mechanism like "matched" to guarantee
> > > > synchronization between inequivalent clock events. However,
> > > > "triggered" can opportunistically synchronize between
> > inequivalent
> > > > events that happen to be simultaneous. This could be
> useful, and
> > > > preserving the syntactic distinction between "triggered"
> > and "ended"
> > > > would be needed because of their distinct semantics.
> > > > Assertions using "triggered" would not be synthesizable unless
> > > > substitution of "ended"
> > > > for "triggered" were legal.
> > > >
> > > > I can see an argument for disallowing "ended" in event
> > expressions
> > > > because "ended" implies an extra guarantee that the
> > synchronization
> > > > is between equivalent events, while the formation of an event
> > > > expression must, of essence, allow the creation of an
> > inequivalent
> > > > event.
> > > >
> > > > I believe that at module level (or analogous levels),
> "triggered"
> > > > should be allowed with arguments. The user can always define a
> > > > wrapper sequence at module level that instantiates a
> > sequence with
> > > > arguments, and so disallowing this is just an
> > inconvenience. I am
> > > > not sure if there are difficulties that arise from allowing
> > > > "triggered" on instances of sequences in other
> contexts. Perhaps
> > > > the rules that govern the definition of a concurrent in a
> > procedural
> >
> > > > context might be helpful.
> > > >
> > > > Best regards,
> > > >
> > > > John H.
> > > >
> > > > >
> > > > > Hi All,
> > > > >
> > > > > As we discussed in the meeting. I think we need to
> discuss the
> > > > > following things before I can update my proposal:
> > > > >
> > > > > 1. Is .ended allowed in event expressions (i.e. in wait
> > > > statement) in
> > > > > the procedural code. My impression is it is allowed
> > based on the
> > > > > discussion few weeks ago. If it is allowed then why
> not make it
> > > > > available till the time the event wakes up to get executed.
> > > > >
> > > > > 2. Is .triggered allowed to be used to form sequence
> > expressions ?
> > > > > Here we need to consider .triggered property of any
> > event not just
> >
> > > > > sequence events. Current syntax allows it and LRM does not
> > > > prohibit it.
> > > > >
> > > > > 3. Joseph raised this question: can .triggered be invoked
> > > > on sequences
> > > > > which have formal arguments ?
> > > > >
> > > > > 4. In what region .triggered goes high ? Currently LRM
> > says that
> > > > > it goes high in Observe region. My understanding is
> > that it should
> >
> > > > > go high at the same time .ended goes high. Here is a statement
> > > > from LRM
> > > > > section 8.11:
> > > > >
> > > > > The triggered status of a sequence is set during the Observe
> > > > > region and persists through the remainder of the
> > time-step (i.e.,
> > > > > until simulation time advances).
> > > > >
> > > > > From this, it looks like the only difference in .ended and
> > > > .triggered
> > > > > is that .triggered defines when it goes down but .ended
> > > > does not define it.
> > > > > I think it will be good idea if we clearly define in
> > the LRM when
> > > > > .ended
> > > > >
> > > > > goes down even if we restrict its usage to sequence
> > > > expressions only.
> > > > >
> > > > >
> > > > > Thanks.
> > > > > Manisha
> > > > >
> > > > >
> > > > >
> > > > > -----Original Message-----
> > > > > From: Eduard Cerny [mailto:Eduard.Cerny@synopsys.com]
> > > > > Sent: Wednesday, November 10, 2004 1:27 PM
> > > > > To: sv-ac@eda.org; Kulshrestha, Manisha
> > > > > Cc: Ed Cerny
> > > > > Subject: AC 296
> > > > >
> > > > > Hello Manisha,
> > > > >
> > > > > I agree with you and think that it is a good idea to
> > summarize the
> >
> > > > > sequence methods in a se[arate section. However I
> would like to
> > > > > suggest a some changes to your proposal. In particular,
> > ended and
> > > > > matched should not be allowed outside expressions in
> > > > sequences. They
> > > > > are more like boolean events valid only at the clock tick.
> > > > We should
> > > > > discuss it tomorrow at the meeting.
> > > > >
> > > > > Best regards,
> > > > >
> > > > > ed
> > > > >
> > > > >
> > > > > ---
> > > > > In the paragraph on ended you say:
> > > > >
> > > > > "The ended status of the sequence is set in the Observe
> > region and
> >
> > > > > persists through the remainder of the time step (i.e. until
> > > > simulation
> > > > > time advances). This method can be used to detect the
> > endpoint of
> > > > > a sequence used in another sequence."
> > > > >
> > > > > I think that extending the duration of the ended in not
> > > > necessary as
> > > > > it cannot be used anywhere but in another sequence
> > which does also
> >
> > > > > evaluate in the Observed region. (Clearly, when evaluating
> > > > sequences
> > > > > the evaluation must be ordered by mutual dependency and the
> > > > dependency
> > > > > graph must not have
> > > > > cycles.) Perhaps you would agree if the text is changed as
> > follows:
> > > > >
> > > > > "The ended status of the sequence is set in the Observed
> > > > region. This
> > > > > method can only be used to detect the endpoint of a
> sequence in
> > > > > another sequence.
> > > > > There must be no circular dependency between sequences
> > > > induced by the
> > > > > use of ended."
> > > > >
> > > > > ---
> > > > > In the paragraph on triggered :
> > > > >
> > > > > "The value of method triggered evaluates to true if the
> > > > given sequence
> > > > > has reached its endpoint at that particular point in time and
> > > > > false otherwise.
> > > > > The triggered status of the sequence is set in the Observe
> > > > region and
> > > > > persists through the remainder of the time-step. This
> > > > method can be
> > > > > used anywhere that the triggered property of events
> can be used
> > > > > (section 13.5.4).
> > > > > It is an error to pass a local variable as an actual
> > argument to a
> >
> > > > > sequence instance on which method triggered is applied.
> > > > This prevents
> > > > > local variables from flowing out of method triggered. (See
> > > > > section 17.8)"
> > > > >
> > > > > I propose that you add:
> > > > >
> > > > > "... This method can be used anywhere that the triggered
> > > > property of
> > > > > events can be used (section 13.5.4), including the boolean
> > > > expressions
> > > > > in disable iff statements of properties. There should be no
> > > > circular
> > > > > dependency between properties and sequences induced by
> > the use of
> > > > > sequence triggered in disable if clauses. It is an error ... "
> > > > >
> > > > > ---
> > > > > The paragraph starting with: "The methods ended and triggered
> > ..."
> > > > >
> > > > > Change as
> > > > >
> > > > > "The method triggered can be used in wait statements
> > or boolean
> > > > > expressions outside of property context. However, it is
> > an error
> > > > > to invoke those methods on sequences which treat their formal
> > > > arguments
> > > > > as local variables. A sequence treats its formal argument
> > > > as a local
> > > > > variable if the formal argument is used as an lvalue in
> > > > > operator_assignment or inc_or_dec_expression in
> > > > sequence_match_item."
> > > > >
> > > > > ---
> > > > > The paragraph starting with: "Unlike ended and triggered,
> > > > matched uses
> > > > > ..."
> > > > >
> > > > > Change to:
> > > > >
> > > > > "Unlike ended and triggered, matched provides means for
> > > > > synchronization between two clocks by making available the
> > > > result of
> > > > > the source sequence match to the evaluation of the
> destination
> > > > > sequence at the first clock tick of the destination
> > > > sequence after the
> > > > > source sequence match. This method is used to detect the
> > > > endpoint of a
> > > > > sequence in a multi-clocked sequence. If the source and
> > > > > destination clocks are the same, again the result is
> > transferred
> > > > > to the first subsequent clock tick. Like ended, matched
> > can only
> > > > > be used
> > > > in boolean expressions in sequences."
> > > > >
> > > > >
> > > > >
> > > > >
> > > > >
> > > >
> >
>
>
>
>
Received on Thu Nov 18 08:50:39 2004