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 Mon Nov 15 09:24:53 2004