Re: [sv-ac] RE: AC 296

Hi John,
According to 3.1a,
If s is a sequence, then @(s) is allowed. This statement is useful for
waiting on an end of a sequence in the reactive region. The end of a
sequence schedules a "sequence event" of the same name in the reactive region.
The behavior of @(s.ended) and @(s.triggered) is not defined. Unlike other
boolean variables, the rising or falling values of s.ended and s.triggered
cannot be detected in SV code. Therefore, @(s.ended) and @(s.triggered)
are not meaningful. Only events (or events caused by changes in values) are
allowed with the @ operator.
Surrendra
At 11:24 AM 11/15/2004 -0600, you wrote:
>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."
> > > >
> > > >
> > > >
> > > >
> > > >
> > >

**********************************************
Surrendra A. Dudani
Synopsys, Inc.
377 Simarano Drive, Suite 300
Marlboro, MA 01752

Tel: 508-263-8072
Fax: 508-263-8123
email: Surrendra.Dudani@synopsys.com
**********************************************
Received on Mon Nov 15 12:56:31 2004