Accellera SuperVerilog Assertion Activity: Re: [sv-ac] Conditio

Re: [sv-ac] Conditions over sequences

Subject: Re: [sv-ac] Conditions over sequences
From: Bassam Tabbara (bassam@novas.com)
Date: Sun Dec 08 2002 - 10:04:44 PST

What I meant was to prefix that paragraph of "BTW [*in OVA*].... common denominator..." etc.. I did not mean OVA and PSL (but I see it is confusing). I meant that in -OVA- the idea is to have different event: .... / event: .... tied to different clocks, and then pull them together in the same sequence.... ended/matched in that case are the operators, the sequence they live in is the common denominator region ....

Sorry, not OVA and PSL .... Thx again for clarifying.

-Bassam.

Erich Marschner wrote:

Bassam,I agree that the LRM needs much work.I understood what you stated about the use of 'ended' to achieve the result of sequence implication. That's not an issue.I was responding to your statement that "the same argument applies to multiple clocks", and that "an operator [can be] used to get the common denominator" of the semantics of the two languages. The fact is that, w.r.t. interaction between multiple clock domains, there seems to be no common denominator between OVA and PSL, which is why the DWG has agreed to leave out multiple clocking entirely. (And if there are still references to multiple clocking in the LRM, they need to be removed.)Regards,Erich -------------------------------------------
Erich Marschner, Cadence Design Systems
Senior Architect, Advanced Verification
Phone: +1 410 750 6995 Email: erichm@cadence.com
Vmail: +1 410 872 4369 Email: erichm@comcast.net

-----Original Message-----
From: Bassam Tabbara [mailto:bassam@novas.com]
Sent: Sunday, December 08, 2002 12:43 PM
To: Erich Marschner
Cc: Joseph Lu; Stephen Meier; sv-ac@eda.org
Subject: Re: [sv-ac] Conditions over sequences
Erich, I am disheartened you did not get what I stated. It was not my intent to address merging PSL/OVA, of course there are subtlties. I responded to the question in the -context specified- and outlined that in *OVA* legacy (the dominant language it -seems- in LRM0.75):
    - multiple clocking is supported
    - if (bool_expr) .... is not such a major restriction only a syntactic one.
BTW, this is the first I hear that DWG had intended to avoid multiple clocking, if so, then the LRM reflects this poorly ... Also It is important first to see that if each approach -can- do the function ... only then can you consider merging or picking one or the other ....
-Bassam.
P.S. Faisal may I suggest sv-ac/DWG implement an ISSUE list of unresolved item ? We did that in sv-cc and it saves a lot of time by keeping things focused. A lot of questions have been posed, not a great many have been discussed. Adam started a list of comments, can we may be do something like:
ISSUE 1.x: Allow seq_expr in if (....)
    - opinions -> solution -> resolution
And associate such a list (like a "release_notes" or a "todo") with each version of LRM.

Erich Marschner wrote:
Bassam,Your argument about multiple clocks fails to consider the different semantics of PSL and OVA. OVA requires both clocks to tick, whereas PSL does not. >From the PSL perspective, the clock 'synchronization' of OVA - what you refer to as the "delayed latching" concept - looks like an implementation artefact that will get in the way of modeling self-timed logic and other kinds of systems that are not strictly synchronous. It is this mutliple-clock semantic difference between OVA and PSL that has caused the DWG to avoid dealing with multiple clocks at all in the current version of the SVA LRM.So I would say that your 'analogy' does not work, in fact, when you get down to the details of the clocking semantics.Regards,Erich-------------------------------------------
Erich Marschner, Cadence Design Systems
Senior Architect, Advanced Verification
Phone: +1 410 750 6995 Email: erichm@cadence.com
Vmail: +1 410 872 4369 Email: erichm@comcast.net
-----Original Message-----
From: Bassam Tabbara [mailto:bassam@novas.com]
Sent: Sunday, December 08, 2002 11:21 AM
To: Joseph Lu
Cc: Stephen Meier; sv-ac@eda.org
Subject: Re: [sv-ac] Conditions over sequences
Hi Joe,
Thanks for bringing up these issues. About "bool_expr" in condition, also Adam had raised this ... so let me offer my opinion on this.
I feel the language DOES support having "sequence conditions" , it is just a matter of how you compose "sequences" to build others. The language merely restricts the syntax somewhat to make the semantics clear e.g, if (...), means if ("boolean"), so if you have a sequence you have to "convert" it to boolean through ended (a.k.a. matched) to "sample" it as a condition. Am I missing your point and Adam's or do you agree with me that indeed this is there, just adding a minor syntactic layering to make the semantics easy to understand ? Do you see that what you want can be done through:
    if (ended(sequence_here)) then .....
BTW same argument can be made for multiple clocks, instead of "defining" the semantics of what mixing of domains means, an operator is used to get the "common denominator" if my analogy works :-)! and make sense of the expression through the syntax construction ....
This is a design philosophy, we actually have 2 philosophies in the mix:
    a) PSL legacy with sampling @... so you sample from different domains in a single sequence
    b) OVA legacy of "single clocking domain" with the delayed "latching" concept.
Either one is fine, and I believe what I am stating is that both approaches can support this requirement. In fact, the two approaches have almost the same overhead in terms of semantic analysis, (a) is more concise at the expense of being less reusable in composition terms (i.e. less "common sub-sequence expressions identified by user).
Right now in the LRM, the (b) flavor seems dominant: more explicit ("interface" between clocking domains), more precise, more readable for designer, more typing :-), but it's a trade-off and conceivably we can have both approaches live together, they are compatible in this regard: (b) approach offers a good simple foundation in terms of having different "interface" mechanisms in the future between these clocking islands (e.g. semantics of event consumption, queuing etc....).. (a) can be a "shortcut" once the interfaces are defined (e.g. through "default" and the like).
So again a sound mixing is in order :-)! I hope the readers now see that there is no sematic restriction, only a syntax one ... Adam/Joe, please comment if I somehow missed your questions.
-Bassam.

Joseph Lu wrote:
Hi Steve,
Thanks for your comments.
As you mentioned about the use of properties as assumption, the
current definition of conditional sequence dose not allow the
condition expression to be a sequence (it only allows boolean exps).
We may have to change it to allow sequence expressions. In such case,
I would also like to bring up the attention of how we resolve the
semantics of handling sequences which might be associated with different
clocks. For the example you have shown as follows.
>I think the requirement that you are striving for is to use properties as
>assumptions.
>
> assert @(posedge clk1) if ( sequence1) sequence2;
Is such case, we need to consider to extend if (seq1) seq2 as
the sequential implication "seq1 ==> seq2" (also Bassam mentioned
the same need for that in his previous email) and seq1 and seq2 are
associated with different clocks. Such properties are very commonly seen.
For example, on a self-timing network, we may see different data/address
packages flowing around the network and each package has its own timing
information. As we are verifying system properties, sometimes we only care
about the package ordering rather than the exact cycle information between
packages. What we may end up with verifying properties is like:
    {s1; s2; s3} ==> {s4; s5; s6; s7}
where s1 .. s7 may be associated with different clocks.
I think we need to address this issue.
Thanks,
--Joseph
--------------------------------------------------
Joseph Lu, Ph.D.
Processor Product Group
Sun Microsystems
M/S USUN 03-202, 430 N. Mary Ave.,
Sunnyvale, CA 94086
408-616-5887
joseph@eng.sun.com
--------------------------------------------------
> Hi Joseph:
>
> Yes I think you are missing the intent of the restrictions on sequences.
>
> These operations (istrue, occurs) are to put additional restrictions on
> behaviors which must occur in addition to the sequence occuring. It is a
> way of creating a more complex sequence.
>
> As an example for occurs
>
>          occurs sequence1 within sequence2
>
> When asserted, then not only does sequence2 need to hold but the sequence1
> must hold somewhere within the time window of sequence2.
>
>
> I think the requirement that you are striving for is to use properties as
> assumptions.
>
> This can be achieve by having a tool directive to assume a property.
>
> asssert @(posedge clk1) if ( sequence1) sequence2;
>
> If this property was asssumed then then the verification tool would
> constraint things such that if sequence1 did occur then it would need to
> generate sequence2. Whenever sequence1 does not occur then sequence2 is
> ignored.
>
> I hope this clarifies and corrects the topic.
> Steve
> ----------
> At 11:31 AM 12/6/2002 -0800, Joseph Lu wrote:
>
> >Hi,
> >
> >The DWG Rev0.75 documents states that constraints can be specified as
> >conditions over
> >sequences. The semantics states that the condition must hold true while
> >processing a transaction. Further, it explains that if the condition
> >becomes false while the sequence is being evaluated, the sequence does
> >not match and a property stated over this sequence would declare a failure
> >as shown in the 11.7.7 example.
> >
> >My question is if we are using constrains to filter out some
> >unexpected/uninterested
> >inputs combinations to DUT, why should we check if the sequence
> >matches when the constraints are not met? If the constraints are
> >not met, we are not interested in the sequence specified.
> >Making the property stated over this sequence to declare a
> >failure when the constraints are not met seems a little bit
> >counter-intuitive to me. Even more so for formal verification,
> >we use constraints to trim/scope down the interested design space.
> >Am i missing something?
> >
> >Thanks,
> >
> >
> >
> >--Joseph
> >
> >--------------------------------------------------
> >Joseph Lu
> >Processor Product Group
> >Sun Microsystems
> >M/S USUN 03-202, 430 N. Mary Ave.,
> >Sunnyvale, CA 94086
> >408-616-5887
> >joseph@eng.sun.com
> >--------------------------------------------------
>
> Steve Meier (stephen.meier@synopsys.com) W: 650-584-4476, Cell: 408-393-8246
>
-- 
Dr. Bassam Tabbara
Technical Manager, R&D

Novas Software, Inc.
bassam@novas.com
(408) 467-7893
-- 
Dr. Bassam Tabbara
Technical Manager, R&D

Novas Software, Inc.
bassam@novas.com
(408) 467-7893

-- Dr. Bassam Tabbara Technical Manager, R&D Novas Software, Inc. bassam@novas.com (408) 467-7893

This archive was generated by hypermail 2b28 : Sun Dec 08 2002 - 10:06:27 PST