Subject: Re: [sv-ac] Draft of SVAC ballot for 2/24
From: Adam Krolnik (krolnik@lsil.com)
Date: Fri Feb 21 2003 - 12:48:12 PST
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?
initial assert @(posedge clk) (s0 ^ s1);
Do we really need to have an extra 'initial' keyword associated with properties?
Is voting against #3 also voting against replacement of 'never' with 'not' ?
>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...
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.
Thanks.
Adam Krolnik
Verification Mgr.
LSI Logic Corp.
Plano TX. 75074
This archive was generated by hypermail 2b28 : Fri Feb 21 2003 - 12:49:37 PST