Subject: Re: [sv-ac] Draft of SVAC ballot for 2/24
From: Stephen Meier (Stephen.Meier@synopsys.com)
Date: Sat Feb 22 2003 - 20:53:00 PST
Hi Adam: Please see embedded comments.
At 02:48 PM 2/21/2003 -0600, you wrote:
>Hi Steve;
>
>
>A few comments about the ballot:
>
>Item 3 & 4.
>
>#3 says you can't do "initial never s1".
>#4 says I can do "initial never" and I can do "always never" and "always"
>and "initial"
>
>Is there a case where I would want to write a property in the simulation
>that only simulates once? What does this statement mean?
It means that it is only checked for the first evaluation after it is
enabled. This is critically important as you may trigger assertions
through API and in many cases you may only want to have it checked for
initial sequence of evaluation.
initial - means evaluate for only initial evaluation, so a ; b will only
launch the first sample clock cycle. If initial directive is not used then
the assertion is checked at every clock edge.
>initial assert @(posedge clk) (s0 ^ s1);
>
>Do we really need to have an extra 'initial' keyword associated with
>properties?
It is the dual of whether we need the 'always' keyword to be required. If
'always' is implicit then you need initial to override the default behavior
in case you do not want 'always'.
>Is voting against #3 also voting against replacement of 'never' with 'not' ?
No. 'never' has always really meant 'not' and I'm happy to see the
semantics group correct this incorrect name.
> >A yes vote is allowed on only one of items 9a or 9b
> >9a Syn4 Add an non-overlapping implication operator (Cindy's[]
> Yes[]No
> >9b Syn4 Change implication to non-overlapping form (Adam's) []
> Yes []No
>
>I recommend that one be allowed to vote for both, if desired. Since each
>proposal is
>on its own, there should not be any tying to each other. Consider the fact
>that
>9a fails and 9b passes - one could not vote for both wanting one or the
>other...
No, I see them as independent topics. If 9a succeeds then 9b is not
appropriate as it only changes the syntax interpretation of the
operators. Any syntax is up to DWG. So this choice is fairly basic, 1 or
2 operators.
9a) have two forms
9b) have one form and make it non overlapping case
As co-chair I reccomend a vote against 9b. It removes key functionality of
being able to learn one operator and be able to easily express both behaviors
1) Overlapping: a => c;d
2) Nonoverlapping: a => [1];c;d
without the overlapping form, lets call it (=>) then it is not possible to
easily express the
behavior a => c;d.
>Also as justification of 9b:
>
>A combination of 10a and 9b (not 9a) would produce these forms:
>
> Going with your and Cindy's recommendation of two implication
> operators, the forms
> from my previous mail:
>
> 1. (A; [2] b) ok
> 2. (A; [1:2] b) ok
> 3. sequence seqC = ([1:10] c);
> (A; [0] seq) ok.
> 4. (A => B); ok
> 5. (A => 1; B) ok but *1.
> 6. (A => 1; [1:10] B) ok but *1
> 7. (A => [1:11] B) ok *2
>
>
> Written with the nonoverlapping operator would match more closely with
> the forms that define sequences with a nonoverlapping concatenation
> operation.
>
> Note: read these as if => is non-overlapping (though currently its not.)
>
> 4. (A => [0] B); ok - like #3 where want A && c as
> matching.
> 5. (A => B) ok - just like A; B
> 6. (A => [1:10] B) ok - numbering matches "1 to 10 cycles
> later."
> 7. (A => [0:10] B) ok - like #6, but allowing overlap of
> A & B.
>
>
> Thus (nonoverlapping versions)
> cover (A; [1:4] B)
> assert (A => [1:4] B)
>
>
>
>For issues 10a/10b,
>
>These proposals are ill formed for comparison. Cindy's proposals discusses
>semantics
>and meanings, while Surrendra's proposal gives a BNF with no semantic
>discussion.
>I can intepret what the BNF means, but I may be wrong or different from
>another on
>what the sematic meaning is. We should reform these proposals to explain
>semantics
>and BNF.
The semantic meanings are self apparent as it follows all of the semantics
currently explained in Draft 3 of the LRM. The only difference is
syntax. Please refer to v0.8 of working document. The vote will proceed
on this basis.
> Thanks.
>
> Adam Krolnik
> Verification Mgr.
> LSI Logic Corp.
> Plano TX. 75074
>
>
Steve Meier (stephen.meier@synopsys.com) W: 650-584-4476, Cell: 408-393-8246
This archive was generated by hypermail 2b28 : Sat Feb 22 2003 - 20:53:55 PST