Formal verification extended for Sequential Logic & CDC gate-level analysis
Mentor cites a five-fold reduction in debug cycles with an interactive multi-platform user interface (GUI) for the Questa PropCheck and Questa CDC tool suites. Now added is the formal-based Questa Sequential Logic Equivalence Checking (SLEC) app, for RTL-to-RTL equivalence checking. And, the new Questa Clock Domain Crossing (CDC) Gate-level verification app helps minimize re-spins and ensures critical synchronization logic has not been disrupted.
The interactive multi-platform graphical user interface (GUI) for the Questa PropCheck and Questa CDC apps enables users to be productive anywhere. The formal-based RTL-to-RTL equivalence checking flows with the SLEC app can, Mentor says, reduce verification turnaround time by 10x.
Interactive debug capabilities can, Mentor says, shorten every step of the debug cycle—from failure detection to identification of the root cause of failures to development and validation of a fix. Using Mentor’s Visualizer Debug Environment (itself built on the popular “Qt” platform), the Questa PropCheck app for formal verification enables users to more rapidly find root cause issues with their device under test (DUT) that the formal algorithms identify.
Additionally, with web browser and mobile views – claimed as an industry-first – users can check on the progress of running jobs and analyze results when away from their workstations: using a VPN to provide a secure data link, users can access formal or CDC results and decide whether to re-run an analysis with new parameters, alert colleagues in different time zones to necessary corrective actions, or login to their employer-provided laptops to take more extensive corrective actions themselves.
Exhaustive sequential logic equivalency checking
Even the most carefully designed testbench is inherently incomplete, since constrained-random methods cannot hit every corner case. Even after 100% functional coverage is achieved, there can still be critcal bugs hiding in unimagined state spaces. Furthermore, many high-value verification tasks can take weeks of testbench development and simulation. In contrast, a host of verification use cases can be addressed by sequential logical equivalence checking in hours—even minutes—with exhaustive results.
The Questa SLEC app provides an exhaustive comparison between the behaviours of two RTL blocks so users can be assured all possible corner cases have been checked. In particular, this app is optimized to address three popular RTL-to-RTL sequential equivalence checking flows: verification of manual low-power clock gating, bug fix and engineering change order (ECO) validation, and ISO 26262 safety mechanism verification.
This product complements the Calypto SLEC Pro and SLEC System offerings, which are focused on the verification of PowerPro’s automatic power reductions and C-to-RTL equivalence checking respectively. In contrast, Mentor’s FormalPro solution will continue to focus on cases where the DUTs being compared have the exact same number of states (post-synthesis RTL-to-gate, and gate-to-gate logic equivalency checking).
Gate-level analysis detects metastability
CDC bugs from clock signal metastability are impossible, Mentor continues, to detect with simulation. Without CDC analysis, CDC bugs will only be discovered in the lab, when it is too late to take corrective action other than to re-spin the whole chip. Even worse, at the gate-level of logic in advanced node devices (28 nm or lower), RTL CDC tools cannot easily detect glitches introduced by synthesis or other back-end tools on CDC paths that were safe at RTL.
The Questa CDC-GL app is optimized for gate-level analysis. The app leverages the RTL CDC data and the waivers generated at the RTL level by the Questa CDC solution to produce focused “low noise” results that enable rapid identification of catastrophic gate-level CDC errors. The Questa CDC-GL app is suited for designs at the 28nm node and below where a gate-level analysis approach is required to prevent unpleasant surprises when the initial samples come back from the fab.
Mentor; www.mentor.com
If you enjoyed this article, you will like the following ones: don't miss them by subscribing to :
