Subject: Re: [sv-ec] Fwd: [sv-ac] SVAC 0.79 template example
From: dudani@us04.synopsys.com
Date: Mon Feb 03 2003 - 10:22:19 PST
Hi Adam,
Please see the comments below.
Surrendra
At 11:48 AM 2/3/2003 -0600, you wrote:
>Hi Surrendra;
>
>
>Okay, I read your template and have a few comments.
>
>
>1. Now we need this clocking domain in a template.
>
> How does this compare to a set of assertions written in a module?
> Why would one not allow an always block (like modules) to contain
> this satelite FSM state code?
>
> int req_cnt = 0; // initialized to 0 prior to any clock tick
> int ack_cnt = 0; // initialized to 0 prior to any clock tick
>
> always @(posedge clk)
> begin
> if (req) req_cnt <= req_cnt + 1'b1;
> if (ack ) ack_cnt <= ack_cnt + 1'b1;
> end
This is equivalent description to assignments inside a clocking domain.
>2. This is not a good restriction that you have written as a comment.
>
> "// you cannot use assert or cover inside a clocking domain"
>
> While good methodology may include the statement,
> "Define named properties and assert or cover these names.
> This allows for reuse of the properties independent of the
> existing assertion or coverage directives."
The reason for not allowing assert or cover is because they can have
action_block. An action block may contain arbitrary code, which is not
allowed in clocking domain.
> I think the syntax should still allow the shorter form as I originally
> wrote:
>
> expect_req_then_ack: assert @(posedge clk)
> (req => first_match ( (int cnt = req_cnt) // Note req_cnt to match
> with ack_cnt.
> ([1: latency] ack && ack_cnt == cnt))) //
> matches with req.
>
> [The clock specification is an independent thing.]
>
> I think this is also an acceptable way of specifying assertions as
> you don't
> have to search back up for what the property is, or search down to
> see how a
> property is used (assert/cover, etc.) or if it is.
>
I agree, and it is allowed, except in clock domains.
>3. The property to ensure ack's match req's is interesting:
>
> property match_req_p = (req_cnt - ack_cnt >= 0); // you never have
> an extra ack
>
> This only works due to the assumption that the counters will never
> exceed their
> maximum value. If these counters were defined to be smaller than 32
> bits, then
> this assumption may be violated.
>
> Would this be an issue (32 bit state variables)
You are right, that is the assumption.
> Thanks.
>
> Adam Krolnik
> Verification Mgr.
> LSI Logic Corp.
> Plano TX. 75074
**********************************************
Surrendra A. Dudani
Synopsys, Inc.
377 Simarano Drive
Suite 300
Marlboro, MA 01752
Tel: 508-263-8072
Fax: 508-263-8123
email: dudani@synopsys.com
**********************************************
This archive was generated by hypermail 2b28 : Mon Feb 03 2003 - 10:23:11 PST