Hinging on a new hybrid formal register-transfer-level (RTL) verification product, a design-for-verification (DFV) methodology from Synopsys leverages SystemVerilog's capabilities to integrate verification throughout the design process. The methodology uses assertion-based verification, constraint random test generation, and formal analysis. This approach reaps some of the verification promise of SystemVerilog as envisioned in its Superlog days.
The methodology comprises at least two major components, according to Dave Kelf, senior director of marketing for Synopsys' Verification Technology Group. The first part is a platform that integrates simulation with other verification technologies. "Verification must begin at the transaction specification level and work its way down through to gate level," says Kelf.
Enter Magellan, a hybrid formal verification tool that allows assertions to drive verification at all levels of abstraction. Magellan's hybrid architecture permits it to search through the design in simulation mode until it reaches a problematic area, where it can apply formal-verification techniques to uncover deeply hidden bugs. The built-in VCS simulation engine and Synopsys' built-from-scratch formal engine leverage each other to save time and iterations. The tool offers very large capacity, enabling it to handle full blocks and sidestepping verification gaps that arise when blocks must be broken up to accommodate tools with lesser capacity.
A second major component of the methodology is a unified language, which is what SystemVerilog brings to the table. "If designers understand the use of transaction specification in the design flow, then they need to use the same language as the verification engineers and other designers downstream," says Kelf.
Use of SystemVerilog and Magellan allows verification engineers to avoid rewriting testbenches over and over for different verification tools, an otherwise time-consuming and error-prone process.
Another benefit of Magellan is its ability to weed out false-negative error reports and to deliver deterministic results. Violations detected by the tool's formal engine are automatically tested out by the VCS simulator before being reported as errors.
Adding Magellan to Synopsys' Discovery Verification Platform enables hierarchical verification. Block-level assumptions and assertions are automatically reused as chip-level monitors by VCS and Vera.
Magellan is being beta-tested now and will be generally available in the fourth quarter. Pricing starts at $73,500 for a one-year license.