Re: [sv-ac] Discussion: Legal use of .ended in disable iff ?

From: Surrendra Dudani <Surrendra.Dudani@synopsys.com>
Date: Fri Apr 30 2004 - 06:57:04 PDT

Hi Ben,
One of the reasons for the limitation that the expression of "disable iff" may not contain .ended is that this expression is evaluated asynchronously during simulation. Since .ended is not allowed and has no meaning outside of the narrow "observe" region, one cannot evaluate such an expression asynchronously.
However, SV also provides an event for each declared sequence. You can use level-sensitive event sequence.trigger in the "disable iff". Your example can be written as

 sequence Q; (a ##1 b); endsequence
property Y;
    disable iff (Q.trigger) ..... ; endproperty 
assert property Y;

Surrendra
At 11:10 AM 4/29/2004 -0400, VhdlCohen@aol.com wrote:

Surrendra / Adam / Wolfgang,
This is another area where SVA and PSL differ, and I really would like to see the PSL interpretation of an endpoint that can be used as a clocking expression or in the PSL abort when condition.  With that interpretation, one should be able to use the end of a sequence to disable another property. This is very POWERFUL stuff!
Tha only alternative I see is to declare in SV a variable that gets assigned a value based on .ended (Possible?), and then use then in the disable.  For example:
  bit : reset_based_on_endpoint;
  ...
  sequence Q; (a ##1 b); endsequence
  // somewhere in a block
  reset_based_on_endpoint <= Q.ended;
  ...
  property Y;
    disable iff (reset_based_on_endpoint) ..... ; endproperty 
  assert property Y;
 
Is above legal?
Thanks,
Ben Cohen
------
In a message dated 4/29/2004 7:11:14 AM Pacific Standard Time, Surrendra.Dudani@synopsys.com writes:

Hi Wolfgang/Ben,

Below are the answers to your questions:

* does the expression after disable_iff needs an event to be evaluated (both of us guess Yes)?

I presume the "event" here refers to a change in value of one of the operands of the expression associated with the "disable iff" clause. There is no requirement that such an event is needed for the evaluation. However, for efficiency, one would only evaluate the expression whenever there is a change in value.

* can ".ended" produce an event (Wolfgang guesses No, Ben guesses Yes)?

 

.ended does not generate any verilog event as it can only used in the assertion expressions for detecting the end of a sequence in any particular cycle. .ended cannot be used in a clocking expression or a "disable iff" expression.

Surrendra

Hello Wolfgang;


According to the 3.1a draf6 copy, and matching my expectations, use of the methods
".ended" and ".matched" are expressions (actually a primary).

From this approach, one should be able to use the end of a sequence to disable another
property.

Whether or not the tools support such a construction is another question.


      Adam Krolnik
      Verification Mgr.
      LSI Logic Corp.
      Plano TX. 75074
      Co-author "Assertion-Based Design"

 
-----------------------------------------------------------------------------
Ben Cohen Trainer, Consultant, Publisher (310) 721-4830
http://www.vhdlcohen.com/ vhdlcohen@aol.com
Author of following textbooks:
* Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004 isbn 0-9705394-6-0
* Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 0-9705394-2-8
* Component Design by Example ", 2001 isbn 0-9705394-0-1
* VHDL Coding Styles and Methodologies, 2nd Edition, 1999 isbn 0-7923-8474-1
* VHDL Answers to Frequently Asked Questions, 2nd Edition, isbn 0-7923-8115
------------------------------------------------------------------------------

**********************************************
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 
********************************************** Received on Fri Apr 30 06:57:15 2004