Subject: Re: [sv-ac] Conditions over sequences
From: Joseph Lu (Juin-Yeu.Lu@sun.com)
Date: Mon Dec 09 2002 - 16:39:35 PST
Hi Bassam,
Thanks for the comments.
Of course, I understand i may create a bool_exp by sampling matched seq_exps.
My question is how "match" really works with multiple-clock
sequences and where its formal semantics is defined (I don't see it the
DWG doc so far). Also, I am concerned about how operators (temporal and bools)
can be applied upon the matched multi-clock sequences. This is a subtle issue
and I want to see the semantics is defined/posted as early as possible.
Hope DWG will address this issue sooner.
Thanks,
--Joseph
------------- Begin Original Message -------------
>From: Bassam Tabbara <bassam@novas.com>
>X-Accept-Language: en
>MIME-Version: 1.0
>To: Joseph Lu <Juin-Yeu.Lu@sun.com>
>CC: Stephen Meier <Stephen.Meier@synopsys.com>, sv-ac@eda.org
>Subject: Re: [sv-ac] Conditions over sequences
>Content-Transfer-Encoding: 7bit
>X-OriginalArrivalTime: 08 Dec 2002 16:21:09.0793 (UTC) FILETIME=[D162C910:01C29ED5]
>
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&DNovas Software, Inc. bassam@novas.com (408) 467-7893
------------- End Original Message -------------
-------------------------------------------------- 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 --------------------------------------------------
This archive was generated by hypermail 2b28 : Mon Dec 09 2002 - 16:43:44 PST