[sv-ac] Forwarding note from Jay Lawrence

Subject: [sv-ac] Forwarding note from Jay Lawrence
From: Stephen Meier (Stephen.Meier@synopsys.com)
Date: Thu Apr 24 2003 - 17:29:06 PDT

Hi:  Jay's emails are bounding due to anti-spam enforcement of member emails.

One comment on Jay's reply.  My comment back to Adam was with respect to immediate assertions and not with respect to concurrent assertions.

I will agree that printing variable values in reactive region with concurrent assertions can result in mismatched values due to potential signals which transition after sampling.  This has been discussed in detail and is a known side effect of cycle based semantics.  The whole point of cycle based sampling is that you abstract away from underlying noise of full delay semantics and thus there is a potential difference between the abstraction and the more detailed view, this is always inherent in abstractions and we take care to ensure the differences are ones we don't care about through methodology.

There are several examples for assertion tools using cycle based semantics successfully and there are debug solutions from vendors which display the sampled values correctly.

Steve
---------
Date: Thu, 24 Apr 2003 16:22:38 -0700 (PDT)
From: owner-sv-ac@eda.org
To: owner-sv-ac@eda.org
Subject: BOUNCE sv-ac@eda.org:    Non-member submission from ["Jay Lawrence" <lawrence@.com>]  
X-Spam-Status: No, hits=1.8 required=5.0
        tests=AWL,HTML_10_20,HTML_FONT_COLOR_BLUE,HTML_MESSAGE,
              NO_REAL_NAME
        version=2.52
X-Spam-Level: *
X-Spam-Checker-Version: SpamAssassin 2.52 (1.174.2.8-2003-03-24-exp)
X-Loop: smeier@eda.org


>From owner-sv-ac Thu Apr 24 16:22:14 2003
Received: from mailgate2.Cadence.COM (mailgate2.Cadence.COM [158.140.2.31])
        by server.eda.org (8.12.0.Beta7/8.12.0.Beta7) with ESMTP id h3ONMBpp027797
        for <sv-ac@eda.org>; Thu, 24 Apr 2003 16:22:13 -0700 (PDT)
Received: from exmbx01chel.global.cadence.com (exmbx01chel.Cadence.COM [158.140.105.230])
        by mailgate2.Cadence.COM (8.9.3/8.9.3) with ESMTP id QAA00165
        for <sv-ac@eda.org>; Thu, 24 Apr 2003 16:22:10 -0700 (PDT)
X-MimeOLE: Produced By Microsoft Exchange V6.0.6249.0
content-class: urn:content-classes:message
MIME-Version: 1.0
Content-Type: multipart/alternative;
        boundary="----_=_NextPart_001_01C30AB8.544D6EDB"
Subject: RE: [sv-ac] Issue of action block in reactive region.
Date: Thu, 24 Apr 2003 19:22:10 -0400
Message-ID: <0D3972F302D58440BD35BF14DC48AF56011E6A69@exmbx01chel.cadence.com>
X-MS-Has-Attach:
X-MS-TNEF-Correlator:
Thread-Topic: [sv-ac] Issue of action block in reactive region.
Thread-Index: AcMKt5jk11SbwOQ0TDuokBT2vr4pGwAAF9Fw
From: "Jay Lawrence" <lawrence@.com>
To: "Stephen Meier" <Stephen.Meier@mailgate2.Cadence.COM>,
   "System Verilog Assertion" <sv-ac@server.eda.org>
X-Received: By mailgate2.Cadence.COM as QAA00165 at Thu Apr 24 16:22:10 2003

This is a multi-part message in MIME format.

------_=_NextPart_001_01C30AB8.544D6EDB
Content-Type: text/plain;
        charset="us-ascii"
Content-Transfer-Encoding: quoted-printable


I do not believe this is corrected in Draft 6. It still says that
concurrent assertions use sampled values, and that action blocks run in
the reactive region. Only the wording on immediate assertions was
changed.
=20
If the assertion runs on sampled values it is looking at the value of
the signal in the preponed region. The values in the reactive region
will see the values which have changed during this cycle. There is every
chance that they will be different.
=20
Cadence continues to believe this is a serious issue.
=20
Jay
=20
p.s. Thanks for taking time to read the ballot response=20

=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D
Jay Lawrence
Senior Architect
Functional Verification
Cadence Design Systems, Inc.
(978) 262-6294
lawrence@cadence.com
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=20

-----Original Message-----
From: Stephen Meier [mailto:Stephen.Meier]=20
Sent: Thursday, April 24, 2003 7:16 PM
To: System Verilog Assertion
Subject: Re: [sv-ac] Issue of action block in reactive region.


Adam:

Note that the issue you demonstrate was raised and resolve during last
meeting and is included in Draft 6 of the LRM

In Sec 17.2:=20


That is, the expression does not evaluate to a known, non-zero value.
The else=20

statement can also be omitted. The action block is executed immediately
after the evaluation of the assert=20

expression.





So the message would print out non mutex values of a and b.

Note that action block is in reactive region for concurrent assertions
and this follows the need to have clear separation between sampled
signals and evaluating their results.  We need to wait for the active
region to complete before we can see which clocks have occurred.

Adam I hope this clears this issue and we can have your support as you
have worked very hard within the comittee to get to this point.

-Steve
----------
At 05:57 PM 4/24/2003 -0500, you wrote:





Hello all;

Based on the issue below, my vote is:

__ yes  _X_ no    Approve sending the LRM (the work performed by SV-AC)
to the board for their approval.


Reading cadence's issue paper, I wrote this simple (similar) example:


assert property ( ! a & b)
   else begin
     $display("A and B not mutex, see a %b and b %b.", a, b);
    end


Cadence writes the action_block is executed in the reactive region. This
causes
the code in the action block to potentially see different values than
the
assertion code. This will make error messages of assertions unuseable
when
trying to write out values in the message. E.g.


assert property ( ! a & b)
   else $error("A and B not mutex, see a %b and b %b.", a, b);


It would be terrible to see a message

Error ........

  A and B not mutex, see a 1 and b 0.


And leave the user scratching their head, wondering why the assertion
fired
when the values it is showing are legal.


Is this an issue to be addressed as an erratta or a post 3.1 issue? I
would
hope that this is not deferred to a 3.2 issue as it will allow
implementations
to be produced that clearly have a deficiency.

One could also consider addressing the availability of dynamic variable
values
for displaying in an error message. Currently the variable does not
exist
out of the property scope.

   THanks.

   Adam Krolnik
   Verification Mgr.
   LSI Logic Corp.
   Plano TX. 75074





Steve Meier (stephen.meier@synopsys.com) W: 650-584-4476, Cell:
408-393-8246



------_=_NextPart_001_01C30AB8.544D6EDB
Content-Type: text/html;
        charset="us-ascii"
Content-Transfer-Encoding: quoted-printable

<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
Message

I = do not believe=20 this is corrected in Draft 6. It still says that concurrent assertions = use=20 sampled values, and that action blocks run in the reactive region. Only = the=20 wording on immediate assertions was changed.
 
If the = assertion=20 runs on sampled values it is looking at the value of the signal in the = preponed=20 region. The values in the reactive region will see the values which have = changed=20 during this cycle. There is every chance that they will be=20 different.
 
Cadence continues to=20 believe this is a serious issue.
 
Jay
 
p.s. = Thanks for=20 taking time to read the ballot response

=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D
Jay Lawrence
Senior=20 Architect
Functional Verification
Cadence Design Systems, = Inc.
(978)=20 262-6294
lawrence@cadence.com
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =20
-----Original Message-----
From: = Stephen Meier=20 [mailto:Stephen.Meier]
Sent: Thursday, April 24, 2003 7:16=20 PM
To: System Verilog Assertion
Subject: Re: = [sv-ac] Issue=20 of action block in reactive = region.

Adam:

Note that=20 the issue you demonstrate was raised and resolve during last meeting = and is=20 included in Draft 6 of the LRM

In Sec 17.2:=20
That is, the expression does not evaluate to a known, non-zero = value.=20 The else=20
statement can also be omitted. The action block is = executed=20 immediately after the evaluation of the assert=20
expression.



So the message would = print out=20 non mutex values of a and b.

Note that action block is in = reactive=20 region for concurrent assertions and this follows the need to have = clear=20 separation between sampled signals and evaluating their results.  = We need=20 to wait for the active region to complete before we can see which = clocks have=20 occurred.

Adam I hope this clears this issue and we can have = your=20 support as you have worked very hard within the comittee to get to = this=20 point.

-Steve
----------
At 05:57 PM 4/24/2003 -0500, you = wrote:


Hello = all;

Based on the=20 issue below, my vote is:

__ yes  _X_ = no   =20 Approve sending the LRM (the work performed by SV-AC) to the board = for their=20 approval.



Reading cadence's issue paper, I wrote this = simple=20 (similar) example:



assert property ( ! a & = b)
  =20 else begin
     $display("A and B not mutex, = see a %b=20 and b %b.", a, b);
    end



Cadence = writes the=20 action_block is executed in the reactive region. This causes
the = code in=20 the action block to potentially see different values than = the
assertion=20 code. This will make error messages of assertions unuseable = when
trying=20 to write out values in the message. E.g.



assert property = ( ! a=20 & b)
   else $error("A and B not mutex, see a %b = and b=20 %b.", a, b);



It would be terrible to see a = message

Error=20 ........

  A and B not mutex, see a 1 and b = 0.



And=20 leave the user scratching their head, wondering why the assertion=20 fired
when the values it is showing are legal.



Is this = an=20 issue to be addressed as an erratta or a post 3.1 issue? I = would
hope=20 that this is not deferred to a 3.2 issue as it will allow=20 implementations
to be produced that clearly have a = deficiency.

One=20 could also consider addressing the availability of dynamic variable=20 values
for displaying in an error message. Currently the variable = does=20 not exist
out of the property scope.

  =20 THanks.

   Adam Krolnik
   = Verification=20 Mgr.
   LSI Logic Corp.
   Plano TX.=20 75074





Steve Meier (stephen.meier@synopsys.com) W: = 650-584-4476, Cell:=20 408-393-8246


------_=_NextPart_001_01C30AB8.544D6EDB--

Steve Meier (stephen.meier@synopsys.com) W: 650-584-4476, Cell: 408-393-8246

This archive was generated by hypermail 2b28 : Thu Apr 24 2003 - 17:31:45 PDT