Subject: Re: [sv-ac] written proposal: issue 15
From: Cindy Eisner (EISNER@il.ibm.com)
Date: Thu Feb 27 2003 - 02:27:27 PST
prakash, adam, john,
i agree with all of you, and i very much like the idea of coding
> always @(posedge clk) a1: assert (a; b; c);
instead of
> a1: assert initial @(posedge clk) (a; b; c);
this agrees with the intuitions i was trying to get at in my proposal.
however, if a clocked sequence cannot be declared, how can the language be
extended to allow multiple clocks? while we haven't yet discussed
restrictions of a multiply-clocked property embedded in procedural code, it
seems to me that this shouldn't be allowed.
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
Prakash Narain <prakash@realintent.com> on 27/02/2003 04:12:37
To: Adam Krolnik <krolnik@lsil.com>
cc: john.havlicek@motorola.com, Cindy Eisner/Haifa/IBM@IBMIL,
sv-ac@eda.org
Subject: Re: [sv-ac] written proposal: issue 15
May I put forth a vote for Adam's and John's proposals.
With always and initial in verilog, do we need a different way
to specify declarative assertions?
Best Regards,
Prakash
Adam Krolnik wrote:
>
>
> Hi John, Cindy;
>
> Currently your proposal allows:
>
> module test;
>
> a1: assert initial @(posedge clk) (a; b; c);
> a2: assert always @(posedge clk) (a; b; c);
> a3: cover initial @(posedge clk) (a; b; c);
> a4: cover always @(posedge clk) (a; b; c);
>
> endmodule
>
> These are declarative versions.
>
> How much different is this:
>
> module test;
>
> always @(posedge clk) a1: assert (a; b; c);
> initial @(posedge clk) a2: assert (a; b; c);
> always @(posedge clk) a3: cover (a; b; c);
> initial @(posedge clk) a4: cover (a; b; c);
>
> endmodule
>
> Maybe we should simplify the property sequence/expr grammar. Through
> the use of
> the initial/always blocks we would not need to define always/initial
> as keywords,
> but instead through the extraction rules we would obtain the necessary
> once or always
> status.
>
> Does this miss something with named properties and such?
>
> Adam Krolnik
> Verification Mgr.
> LSI Logic Corp.
> Plano TX. 75074
>
>
>
>
This archive was generated by hypermail 2b28 : Thu Feb 27 2003 - 02:29:56 PST