Re: [sv-ac] Forwarding note from Jay Lawrence


Subject: Re: [sv-ac] Forwarding note from Jay Lawrence
From: Arturo Salz (Arturo.Salz@synopsys.com)
Date: Thu Apr 24 2003 - 18:14:28 PDT


Stephen,

If users want to generate their own assertion messages, they can use a clocking domain to explicitly sample the variables. If we rewrite Adam's example to make use of this feature we can do:

    clocking y @(...) input a, b; endclocking

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

Or, insert the whole thing (assertion included) inside the clocking declaration.

    Arturo

----- Original Message -----
From: Stephen Meier
To: System Verilog Assertion
Sent: Thursday, April 24, 2003 5:29 PM
Subject: [sv-ac] Forwarding note from Jay Lawrence

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 - 18:16:37 PDT