Subject: Re: [sv-ac] Conditions over sequences
From: Joseph Lu (Juin-Yeu.Lu@sun.com)
Date: Sat Dec 07 2002 - 19:05:01 PST
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
>
This archive was generated by hypermail 2b28 : Sat Dec 07 2002 - 19:09:53 PST