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

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
> --------------------------------------------------------------
> ----------------
>
>
>
Received on Thu Aug 19 22:14:26 2004