Subject: Re: [sv-ac] Assume proposals.
From: Joseph Lu (Juin-Yeu.Lu@sun.com)
Date: Wed Sep 17 2003 - 13:45:42 PDT
Hi Adam,
>I can understand a need for part of proposal #1 - constraining a stimulus generator.
>But it would seem that if one wants assumptions, they would want both assume and
>assume_guarantee types.
>The assume statement would be used outside of the design code being verified to
>restrict the stimulus/search space to a subset of the legal space.
>The assume_guarantee statement would be used inside the design code to define
>how the block is intended to be used.
>
>I don't quite see how an immediate assume fits in. I understand how immediate assertion
>statements can be used - something instead of "if (!expr) $error()". Joseph, maybe
>an example or two to show how you see the immediate assumption being used.
In PSL LRM, i edited the verification layer session where the two directives, assume and
assume_guarantee, have similar semantics to DUT that they can be used to constrain
certain behaviors (or operating conditions) for the DUT. The only difference between
the two is that the assume_guarantee directive directs the verification tool/environment
to have the proof obligation on the assumption, while the assume directive doesn't.
Much the use of immed_assume is for creating local constraints (i.e. "force") which are from
inputs or not easy to be configured from inputs. Of course, we can add immed_assume_guarantee
directive to guide the verification tool/environment to be obligated to prove the assumption
attached to the directive.
For example of a simple dual-port memory assertion,
always @(posedge ck) begin
if (write && port1_en) begin
immed_assume (!port2_en) ;
assert (dqs) ; else $display("%m data strobe not asserted when data is ready");
end
end
Thanks and best regards,
--Joseph
--------------------------------------------------
Joseph Lu
Processor Product and Network Group
Sun Microsystems
M/S USUN 03-202, 430 N. Mary Ave.,
Sunnyvale, CA 94086
408-616-5887
joseph@eng.sun.com
--------------------------------------------------
>Date: Wed, 17 Sep 2003 09:33:05 -0500
>From: Adam Krolnik <krolnik@lsil.com>
>Subject: Re: [sv-ac] Assume proposals.
>To: Joseph Lu <Juin-Yeu.Lu@Sun.COM>
>Cc: sv-ac@eda.org
>MIME-version: 1.0
>Content-transfer-encoding: 7bit
>X-Accept-Language: en-us, en
>User-Agent: Mozilla/5.0 (X11; U; SunOS sun4u; en-US; rv:1.2.1) Gecko/20030711
>
>
>
>Hi Joseph;
>
>Proposal #1 is for an assume statement for environmental constraints and for
> constrained stimulus generation.
>Proposal #2 is for an immediate (boolean) assume statement, for use in design code.
>
>PSL has 4 verification directives for functionality such as this:
> assume, assume_guarantee, restrict, restrict_guarantee (these last two, only
> for sequences, not properties.)
>
>
>I can understand a need for part of proposal #1 - constraining a stimulus generator.
>But it would seem that if one wants assumptions, they would want both assume and
>assume_guarantee types.
>The assume statement would be used outside of the design code being verified to
>restrict the stimulus/search space to a subset of the legal space.
>The assume_guarantee statement would be used inside the design code to define
>how the block is intended to be used.
>
>I don't quite see how an immediate assume fits in. I understand how immediate assertion
>statements can be used - something instead of "if (!expr) $error()". Joseph, maybe
>an example or two to show how you see the immediate assumption being used.
>
>I would like to see assume and assume_guarantee functionality through a combination of
>these proposals. This would provide the ability to specify intent of properties
>in design code as well as constrain stimulus generation specifically.
>
>Surrendra -
>
>BTW, it seems that the biasing and extra constructs for stimulus generation do not
>address temporal constraints. A very simple example is constraining an interface
>to 3 transactions in N clocks, or not starting another stimulus source until a
>previous one completes.
>
>
> Thanks for the proposals guys.
>
> Adam Krolnik
> Verification Mgr.
> LSI Logic Corp.
> Plano TX. 75074
> Co-author "Assertion Based Design"
>
>
>
>
>
This archive was generated by hypermail 2b28 : Wed Sep 17 2003 - 13:46:26 PDT