RE: PSL: Attributes for Verilog and SystemVerilog

From: Michael McNamara (mac@verisity.com)
Date: Tue Mar 16 2004 - 09:09:42 PST

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

    Apologies for jumping into the middle of this, but using the 1364
    attribute syntax as a way to introducing PSL code inline to Verilog
    code is, in my opinion, a very bad idea.

    1364 defines the syntax of what can appear in the attribute region,
    and it is rather limited, basically consisting of assignment
    statements.

    Section A.9.1 of P1364-2005 Draft 3

    attribute_instance ::= (* attr_spec { , attr_spec } *)
    attr_spec ::= attr_name [ = constant_expression ]
    attr_name ::= identifier

    I suspect that embedded PSL might like to have richer semantics than
    are allowed (branches, use of non-verilog operators, non-verilog
    expression syntax, et cetera). The example in this email is illegal,
    as the fragment 'property X = always A & b;' does not match the BNF
    above.

    In my mind the right next step is to have representative(s) of the VFV
    attend a 1364 meeting and discuss ideas for syntax facilitating
    embedding of PSL in Verilog which will address the needs of both
    languages.

    The next meeting of the IEEE 1364 Working Group is Monday, March 22nd,
    at 8:30 am pacific time. The right time & forum to introduce this
    topic would be at the Behavorial Task Force Meeting, which begins at
    10:30 on that day.

    In order to join the IEEE 1364 group, go to
    http://www.verilog.com/IEEEVerilog.html, and click on the Join icon;
    fill in the form; and you will get dialin information.

    -- On Mar 15 2004 at 17:09, VhdlCohen@aol.com sent a message:
    > To: cliffc@sunburst-design.com, vfv@eda.org
    > Subject: "PSL: Attributes for Verilog and SystemVerilog "

    > Cliff brought up an interesting comments that the LRM is not
    > addressing: How inline PSL is defined as comments rather than
    > attributes. Tool vendors seem to have universally adopted the
    > "comment" approach to specify PSL statements. Verilog-2001 and
    > SystemVerilog added attributes for the inclusion of information
    > related to the design. Thus, using that approach. PSL should be
    > implemented as something like:
    >
    > (* PSL, psl_assertion *)
    > Example:
    > (* PSL, property X = always a & b; *)
    > (* PSL, assert X; *)
    >
    > The whole reason for adding attributes to Verilog-2001 (and
    > SystemVerilog) was to get tools away from using comments. Now PSL
    > assertion-compliant tools are again in the business of parsing
    > comments - very annoying! and not compliant to goals of the
    > language specifications. One could argue that how PSL is used in
    > the HDL is tool dependent, and should not be specified in the LRM.
    > However, IEEE spec (verilog 2001) and Accellera specs defined the
    > means to add such attributes. Thus, should the PSL LRM add such a
    > requirement? Ben
    > -----------------------------------------------------------------------------
    > Ben Cohen Trainer, Consultant, Publisher (310) 721-4830

    This archive was generated by hypermail 2.1.4 : Tue Mar 16 2004 - 08:53:40 PST and
    sponsored by Boyd Technology, Inc.