[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 14:14:56 2004