RE: [sv-ac] SVA: USING ASSERTIONS WITH VERILOG RTL

Ben,
    Stuart is accurate in his statements. SVA is
architected and designed to work with Verilog RTL
WITHOUT the use of pragmas and "ifdef". Use of these
unrecommended methods will be non-compliant to SVA
standard. As Stuart said, binding is the easiest one
to use without requiring changes in Verilog models or
tools. If in-lining is required, then both models and
tools have to be modified to read SVA BNF. In fact,
when using pragmas, Verilog parsers have to change to
read and parse these unrecommended pragmas. Therefore
tools should be changed to the legal use of SVA as
defined in the LRM.

    One more thought, is that one of SystemVerilog
goals is to get rid of the bad coding practice of
using Pragmas. So if tools and models are to be
compliant with the SVA standard, they need to use SVA
as defined in the LRM.

      Ben, please follow the SVA standard as it is
written. You also should follow the advice of Stuart
and teach the standard way of using SVA and try to
stay away from Pragmas.

Vassilios

--- Stuart Sutherland <stuart@sutherland-hdl.com>
wrote:

> Ben,
>
> The only suggestion on including SVA with legacy
> Verilog code that makes
> sense to me is to use binding. SVA assertions are
> fully backward compatible
> with Verilog, with the exception of new keywords.
> Therefore, if a tool can
> execute SVA, even if nothing else from
> SystemVerilog, then it makes no sense
> to hide SVA in ifdefs or pragmas. If a tool cannot
> execute SVA, then
> perhaps it makes sense to use ifdef to exclude the
> SVA code, though binding
> would be a lot cleaner. The use of pragmas and
> large blocks of comments to
> hide SVA (or PSL or any other code) is a kludge that
> I find ugly and teach
> my students to avoid. If someone likes ugly pragmas
> around blocks of
> comments rather than native code, then they might as
> well just use PSL.
>
> Just my thoughts...
>
> Stu
> ~~~~~~~~~~~~~~~~~~~~~~~~~
> Stuart Sutherland
> stuart@sutherland-hdl.com
> 503-692-0898
>
> > -----Original Message-----
> > From: owner-sv-ac@eda.org
> [mailto:owner-sv-ac@eda.org] On
> > Behalf Of VhdlCohen@aol.com
> > Sent: Thursday, August 19, 2004 2:15 PM
> > To: sv-ac@eda.org
> > Subject: [sv-ac] SVA: USING ASSERTIONS WITH
> VERILOG RTL
> >
> > A question that often comes up is how to use
> assertions with
> > Verilog RTL code. Users understand that the
> addition of
> > assertions means that the tool handling the
> assertions is a
> > SystemVerilog tool. However, some users desire to
> maintain
> > the current Verilog design flow with Verilog
> design tools
> > (such as synthesis), but yet provide the assertion
> capability
> > for use with other tools, such as simulation or
> formal
> > verification. The following provide potential
> solutions:
> > 1. Define the assertions in separate modules, and
> use the
> > "bind" SystemVerilog feature to bind the property
> modules to
> > the RTL modules. Here, we have clear separation
> between the
> > RTL modules and the assertion modules.
> > 2. Use the "ifdef sva" to enable of disable a
> block of
> > property and verification directives within the
> RTL code.
> > 3. Use an SVA pragma to have an SystemVerilog
> accept the
> > assertions, but yet have non SystemVerilog tools
> interpret
> > the pragma lines as comments. This is done in PSL
> with the
> > "psl" pragma. For example:
> > // sva property test;
> > // @ (posedge clk) req |=> ack;
> > // endproperty : test
> > The questions to this audience are:
> > 1. Is there a standard that companies prefer?
> > 2. Is there a preferred method?
> > Of course, the goal here is interoperability.
> > Thanks,
> > Ben Cohen
> >
> >
>
--------------------------------------------------------------
> > ---------------
> > 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
> >
>
--------------------------------------------------------------
> > ----------------
> >
> >
> >
>
>

        
                
__________________________________
Do you Yahoo!?
New and Improved Yahoo! Mail - 100MB free storage!
http://promotions.yahoo.com/new_mail
Received on Fri Aug 20 00:58:18 2004