SystemVerilog reference verification methodology: RTL

The VMM for SystemVerilog goes beyond simulation-based techniques to encompass the comprehensive verification of formal analysis as well. The wide range of SystemVerilog assertion constructs allows specification of assertions targeted for simulation, formal analysis, or both. The VMM for SystemVerilog provides guidelines for writing assertions that work well with both verification approaches.

A formal tool can analyze each assertion and try to prove that it is safe and can never be violated under any scenario. This step does not require any simulation tests to be written. Assertions so proven do not generally need to run in simulation although they should not be deleted since later RTL design changes could introduce bugs and invalidate the proof.

If an assertion fails, the formal tool generates a counterexample that shows how the assertion can fail. The counterexample either reveals a bug in the assertion or the design, or demonstrates that there are insufficient constraints on the inputs to limit the analysis to legal stimulus sequences.

Some formal analysis tools can also be used to target temporal coverage points that were not hit in simulation by directed or constrained-random testing. Such a formal tool first tries to determine whether the coverage goal can ever be reached. If not, this indicates redundant or unreachable logic in the design, and the coverage database can be updated.

If it can be reached, then an input test may be generated. If the test corresponds to legal stimulus (because the input constraints are sufficient) then the test can be executed with assertions to verify the design behavior and the coverage database can be updated.

Creating reusable verification IP

The layered testbench architecture and other features of the VMM for SystemVerilog is a natural fit for creators of reusable verification intellectual property (VIP). VIP such as transaction-level models, generators, transactors, checkers, assertions, and the other objects in the layered testbench must be easy to use in a wide range of different projects. The guidelines of the VMM for SystemVerilog enable developers to produce compliant VIP, whether for internal reuse across projects or as commercial products.

Any SoC development team that has a VMM for SystemVerilog-compliant verification environment can easily and quickly adopt the internal or external VIP, saving both time and resources on the project. Figure 3 shows how a VIP component is used within the layered testbench. If the verification components associated with a particular interface are packed up properly, then any future chip using this same interface can reuse the VIP.

Conclusions

When coupled with an appropriate methodology, SystemVerilog provides all the constructs and features necessary to build a productive verification environment encompassing constrained-random stimulus generation, coverage-driven verification, and assertions. The book VMM for SystemVerilog documents the reference verification methodology that enables best use of the language capabilities and greatly increases the chance of first-silicon success for advanced chip designs.

The next article in this series will move beyond RTL to cover system-level verification, including the interaction between SystemVerilog and SystemC. The fourth and final article will discuss strategies for adoption, including use of the standard building-block and assertion libraries defined in the VMM for SystemVerilog. Together, this series of articles will provide a broad overview of using SystemVerilog for the verification of complex SoCs. More information on the book can be found at www.vmm-sv.com.

Editor's note: Future articles in this series will appear over the next few months.

Thomas Anderson is Director of Technical Marketing at Synopsys, Inc. His responsibilities include assertions, coverage, formal analysis and RTL checking. He holds an MS in Electrical Engineering and Computer Science from MIT and a BS in Computer Systems Engineering from the University of Massachusetts at Amherst.

Janick Bergeron is a Scientist at Synopsys, Inc. He is the author of the recently published book Writing Testbenches using SystemVerilog, which builds on the success of its best-selling predecessors, and the moderator of the Verification Guild. He holds an MBA degree from the University of Oregon, a Masters degree in Electrical Engineering from the University of Waterloo, and a Bachelor of Engineering from the Université du Québec Chicoutimi.

Eduard Cerny, Ph.D. (McGill University) is a Principal Engineer, R&D, in the Verification Group at Synopsys, Inc. He joined Synopsys in 2001 after 25 years in academia, as Professor of Computer Science at the Université de Montréal. His interests have been in design, verification and test of hardware, and he is author of many articles in these areas.

Alan Hunter, BEng(Hons), MSc, is the Design Verification Methodology Programme manager at ARM Ltd and leads the design verification methodology work for ARM worldwide. This work covers all areas from CPU design verification through systems and system component design verification. His main areas of interest include optimizing design verification efficiency and quality, formal methods, and determinism in the design verification flow.

Andrew Nightingale, BEng(Hons), MBCS CITP, is a consultant engineer at ARM Ltd. and has led the SoC Verification group in ARM's Cambridge and Sheffield design centers for several years. The group covers ARM PrimeXsys platforms and Prime-Cell development, including advanced AXI- and AHB-based system backplane components such as bus interconnects and high-performance memory controllers.