Subject: Re: [sv-ac] written proposal: issue 15
From: John Havlicek (john.havlicek@motorola.com)
Date: Wed Feb 26 2003 - 08:11:34 PST
All:
In my opinion, this syntax
property always p1 = @clk (a;b);
property initial p2 = @clk (a1;b1);
always @(clk) begin
d <= in1;
r1: assert p1;
r2: assert p2;
end
is awful. We should be writing
property p1 = always @clk (a;b);
property p2 = initial @clk (a1;b1);
Then
always @(clk) begin
d <= in1;
r1: assert p1;
r2: assert p2;
end
should mean the same thing as
always @(clk) begin
d <= in1;
r1: assert always @clk (a;b);
r2: assert initial @clk (a1;b1);
end
If this last doesn't make sense, then the preceding shouldn't make
sense either.
In my opinion, it seems that in a procedural context, we want the
top-level temporal modality to be inferred, while in a declarative
context we want it to be explicit. Therefore, the problem is not with
Cindy's proposal. The problem is with what we are allowed to define
and name. If we can only define and name property fragments that
include explicit top-level temporal modalities, then obviously there
is a problem instantiating them in a procedural context where we don't
want to see the temporal modality.
In my opinion we should allow named property fragments that have
no modality. For example, we might let
formula f1 = (a;b);
formula f2 = (a1;b1);
always @(clk) begin
d <= in1;
r1: assert f1;
end
initial begin
in2 = 0;
r4: assert @clk f2;
end
and for use in declarative contexts, we could define
property p1 = always @clk f1;
property p2 = initial @clk f2;
...
Best regards,
John Havlicek
>
> Hi Cindy,
> What happens when a property is defined declaratively, and used in a
> procedural block such as,
>
> property always p1 = @clk (a;b);
> property initial p2 = @clk (a1;b1);
>
> always @(clk) begin
> d <= in1;
> r1: assert p1;
> r2: assert p2;
> end
>
> initial begin
> in2 = 0;
> r3: assert p1;
> r4: assert p2;
> end
> Surrendra
> At 02:29 PM 2/26/2003 +0200, you wrote:
>
> >all,
> >
> >as per yesterday's meeting, here is my written proposal for issue 15:
> >
> >----------------------------------------------------------------------------------------------------------------
> >proposal:
> >
> >when a property is at the declarative level (not embedded in procedural
> >code), require one of either "initial" or "always"
> >when a property is embedded in procedural code, prohibit the use of both
> >"initial" and "always"
> >
> >the bnf for a property would then read something like this:
> >
> >prop_spec ::=
> > ['initial' | 'always'] ['accept' '(' expression ')' ] ['not']
> >clocked_expr
> > | identifier ['(' expression_list ')']
> >
> >while the above proposed restrictions would be semantic restrictions.
> >----------------------------------------------------------------------------------------------------------------
> >
> >i have two concerns that prompt me to make this proposal:
> >
> >1. readability
> >
> >as steven mentioned in the minutes, i think that
> >
> >always @(posedge clk)
> >(0)
> > if (abc)
> > assert always (x;y;z);
> >
> >might be read as
> >
> >assert @(posedge clk) always (abc => always (x;y;z));
> >(1)
> >
> >whereas the extraction rules presented by steve give
> >
> >assert @(posedge clk) always (abc => (x;y;z));
> >(2)
> >
> >although (1) is not a legal assertion in sva, it does have an intuitive
> >meaning to users of other formal languages (like psl). coding as follows:
> >
> >always @(posedge clk)
> >(3)
> > if (abc)
> > assert (x;y;z);
> >
> >eliminates this problem. just as the single @(posedge clk) in (2) is
> >intuitively derived from the single @(posedge clk) in (3), the single
> >"always" in (2) can be understood as coming from the single "always" in
> >(3).
> >
> >2. future expansion of sv assertions
> >
> >if the sv assertions are to be expanded in the future in such a way as to
> >support more flexible kinds of properties (i.e., nesting of clocks,
> >negations, accept, always, etc.), then both (1) and (2) might be allowed in
> >the language. in this case, the extraction rules would need to be more
> >flexible as well, and would probably interpret (0) as (1). thus, in order
> >to get (2), we would have to allow (3).
> >
> >regards,
> >
> >cindy.
> >
> >Cindy Eisner
> >Formal Methods Group Tel: +972-4-8296-266
> >IBM Haifa Research Laboratory Fax: +972-4-8296-114
> >Haifa 31905, Israel e-mail:
> >eisner@il.ibm.com
>
>
>
> **********************************************
> Surrendra A. Dudani
> Synopsys, Inc.
> 377 Simarano Drive, Suite 300
> Marlboro, MA 01752
>
> Tel: 508-263-8072
> Fax: 508-263-8123
> email: Surrendra.Dudani@synopsys.com
> **********************************************
This archive was generated by hypermail 2b28 : Wed Feb 26 2003 - 08:16:41 PST