RE: PSL: Attributes for Verilog and SystemVerilog

From: Erich Marschner (erichm@cadence.com)
Date: Wed Mar 17 2004 - 18:42:19 PST

  • Next message: Michael McNamara: "RE: PSL: Attributes for Verilog and SystemVerilog"

    Mac, Shalom,

    I'm glad to see that the question of how to embed PSL code into Verilog is of such interest.

    I'd like to point out that there are several options for embedding PSL assertions into an HDL description, and there are several languages (Verilog, VHDL, SystemC, SystemVerilog) with which PSL can potentially be used. The approach taken so far - structured comments - has had some advantages:

      - the approach can be used in Verilog, VHDL, SystemC, etc.
      - no changes were required in those languages (works with current versions)
      - embedded PSL is transparent to tools that are not yet PSL-aware

    At the same time, I, and I believe most others, have always expected the structured comment approach to be temporary, and that a more integrated solution would be adopted eventually, as PSL is more widely adopted and integrated with existing standards.

    One possible approach for embedding is the adoption of PSL as a native part of the language. This is the approach being taken in the VHDL 200x effort.

    Another approach would be a 'foreign code' block of the sort that has been discussed here. While this approach is less integrated than the previous approach, it might have other advantages - e.g., allowing C or other HDLs as well as PSL to be embedded in a given HDL design.

    Although this question is clearly of interest to those of us working on PSL, I believe the issues are largely in the Verilog domain - i.e., what works best within the Verilog 1364 standard. I would suggest that the main constraints from the PSL side are the following:

     - Embedded PSL should be allowed to appear 'anywhere' in the design
       (where 'anywhere' means at least before/after any statement).

     - Embedded PSL should follow standard PSL syntax.

     - Embedded PSL should be able to reference any Verilog identifiers visible at
       the place where the PSL is embedded.

    | ... I'd love to have
    | representatives from the PSL group visit us and we talk
    | about them live. This email exchange however is useful to
    | flush out many issues ahead of time as well.

    I should point out here that the Accellera standard does not define an embedding strategy for PSL, and Accellera has not endorsed the current embedding strategy, so it is not at all clear that you need to engage with the 'official' PSL group (the Accellera FVTC). The decision to use structured comments for embedding PSL in designs was taken by a group of PSL implementors in the summer of 2002, and it is an industry convention, not part of the Accellera PSL standard.

    As a representative of one of those PSL implementors, I would be happy to discuss this with the 1364 committee. Representatives of other companies implementing PSL may also want to participate. I would recommend that you schedule a discussion on this to occur a few weeks from now, and invite PSL implementors to attend.

    Regards,

    Erich Marschner
    Cadence

    | -----Original Message-----
    | From: Michael McNamara [mailto:mac@verisity.com]
    | Sent: Wednesday, March 17, 2004 5:57 PM
    | To: Shalom.Bresticker@motorola.com
    | Cc: Alec Stanculescu; mac@verisity.com;
    | cliffc@sunburst-design.com; btf@boyd.com; vfv@eda.org
    | Subject: Re: PSL: Attributes for Verilog and SystemVerilog
    |
    |
    |
    |
    |
    | -- On Mar 17 2004 at 22:03, Shalom.Bresticker@motorola.com
    | sent a message: > To: alec@fintronic.com, mac@verisity.com,
    | > cliffc@sunburst-design.com, btf@boyd.com, vfv@eda.org > >
    | Subject: "Re: PSL: Attributes for Verilog and SystemVerilog"
    | > However, there are disadvantages as well. >
    | > If we compare a psl block to a specify block, then first
    | it adds > two new keywords. Who says that psl is the end and
    | that there won't > be a need for another new block type and
    | then another and another?
    |
    | We could do:
    |
    | foreign (* type = "psl" *)
    |
    | endforeign
    |
    |
    | > Second, the exact grammar of specify blocks is specified
    | in the Verilog
    | > language. Will we have to do that with psl blocks as well?
    |
    | My proposal is that we would not do this.
    |
    | The foreign language could use what ever syntax it wanted.
    | If however, it wanted to reference Verilog variables, it
    | would have to define some hook up method (in my minde the
    | right way is by using attributes. Alternatively, as with
    | SPecify blocks, one could do this by using the same variable
    | naming conventions as verilog and depending on the tool to
    | parse the module to find the variables).
    |
    | module top;
    | joe j1 ();
    | bar bar_one ();
    | endmodule
    |
    | module joe;
    | reg foo;
    |
    | foreign (* type = "psl", a = foo, b = top.bar_one.cpudata *)
    | assume a => b unless hell_freezes_over;
    | endforeign
    |
    | endmodule
    | ...
    |
    | > Third, if we look at SV Assertions as well, due to their
    | close > alignment with PSL, is it logical to have completely
    | separate > mechanisms for SVA and PSL when they have the
    | same core language?
    |
    | The issue here is how do you embed PSL in Verilog.
    |
    | Great effort has gone into making SVA a proper subset of
    | PSL, and even if this could have been achieved (it wasn't)
    | there is still the need to embed code that uses PSL
    | constructs that aren't in the SVA subset. This is the issue
    | before us.
    |
    | > Fourth, an advantage of the pragma/attribute approach is
    | that you write
    | > them adjacent to the place where they are relevant instead
    | of at the end
    | > of the module, far away.
    |
    | There is no restriction on where specify blocks may occur,
    | nor how many you can include in a module. I would presume we
    | do the same here with PSL and/or foreign blocks.
    |
    | It even is the case that while '(*PSL="' and '"*)' uses up
    | 10 characters, 'psl' 'endpsl' uses up only 9, so the
    | psl..endpsl container is arguably less intrusive to the
    | reader than using attributes.
    |
    | > There are probably solutions to all of these, but it is
    | important to
    | > recognize that there are issues that have to be dealt with
    | and not get
    | > into the same complications again that there were and are
    | with config > blocks, for example.
    |
    | I absolutely agree, and this is why I'd love to have
    | representatives from the PSL group visit us and we talk
    | about them live. This email exchange however is useful to
    | flush out many issues ahead of time as well.
    |
    | > Shalom
    | >
    | >
    | > On Wed, 17 Mar 2004, Alec Stanculescu wrote:
    | >
    | > > Mac,
    | > >
    | > > I fully support your idea of how to include PSL into
    | Verilog and I am > > even more adamant about not changing
    | the Attribute construct > > introduced in Verilog 2001. > >
    | > > The advantage of the proposed method over the current
    | one where PSL is > > not embedded is that it will support
    | object oriented description (each > > module will have its
    | PSL description within it) and will reduce the > > need for
    | lengthy external references. > >
    | > > Formal comments used for PSL is the poor and intelligent
    | man's approach > > to the problem. It is not a long term
    | solution, we all agree on that. >
    | > --
    | > Shalom Bresticker
    | Shalom.Bresticker@motorola.com
    | > Design & Reuse Methodology
    | Tel: +972 9 9522268
    | > Motorola Semiconductor Israel, Ltd.
    | Fax: +972 9 9522890
    | > POB 2208, Herzlia 46120, ISRAEL
    | Cell: +972 50 441478
    | >
    | > [x]Motorola General Business Information
    | > [ ]Motorola Internal Use Only
    | > [ ]Motorola Confidential Proprietary
    |

    This archive was generated by hypermail 2.1.4 : Wed Mar 17 2004 - 18:26:10 PST and
    sponsored by Boyd Technology, Inc.