It’s common knowledge that formal verification tools combined with well-crafted SVA or PSL properties leave no stone unturned, yielding an exhaustive solution to a given verification challenge. Despite this tremendous benefit, many engineers—especially designers—do not want to learn about assertion languages. “What does my property mean again?” “How long will it take me to become productive with this new approach?” “Do I have to write properties at all?” Sound familiar?
Aside from formal experts, most engineers do not want to learn about formal techniques given the difficulty in calculating the ROI. Formal analysis has a unique workflow, and the semantics of the results it reports are unfamiliar. In particular, verification leads have trouble showing the value of formal techniques in the context of the full project.
The “Apps” Approach
To bring formal and assertion-based verification (ABV) tools and techniques into mainstream use, a whole new approach is needed—one that puts the focus on “problems vs. EDA technologies.” As such, Cadence has created the “verification apps” approach, which is defined by the following principles:
- A verification app is a well-documented tool capability or methodology focused on a specific, high-value problem
- The given problem is more efficiently solved using formal-based methods and/or a combination of formal, simulation, and metric-driven techniques than simulation-based methods alone
- The barrier to creating the necessary properties and/or the need for ABV expertise is significantly reduced through either automated property generation built-in to the tool(s) or pre-packaged properties (provided)
- Apps quickly solve painful, high-value problems
- Apps are designed for formal/ABV novices to quickly set-up and run
- Many apps tie into metric-driven verification (MDV) flows, making formal/ABV relevant to simulation-centric managers
- Starting from scratch, results from real application can typically be seen in a matter of hours, sometimes even minutes
- Once integrated into a verification team’s workflow, apps tend to proliferate among engineers on their own, freeing up valuable CAD team support resources
Today, Cadence ships a variety of apps that span the entire project life cycle:
As shown in the diagram’s Y-axis, certain classes of users gravitate toward apps that address high-value problems in their particular domain. But since running the apps don’t require any knowledge of formal or ABV, users of all types get results quickly. These results are automatically translated and fed into the metric-driven planning, management, and verification flow in Incisive Metrics Center and Incisive Enterprise Manager
, which are familiar to simulation-centric colleagues and managers.
This app builds on the automatic formal analysis capability, in which Incisive Formal Verifier and Enterprise Verifier automatically generate properties from implied behavior of the DUT’s RTL. With these properties, the tool runs a variety of automatic checks including deadcode, FSM, X-propagation, and more.
The Super Linting GUI overlays the results of the free Incisive HDL analysis and linting tool (“HAL”) with the data from automatic formal analysis to provide a complete picture of the static analysis of your DUT mapped directly to the RTL source code browser.
Protocol Compliance Assertion-Based Verification IP (ABVIP)
Part of the Cadence Verification IP Catalog
, a library of interface properties is available to validate interface protocols like AMBA® APB™, AHB™, AXI™ 3, AXI 4, ACE™, and OCP. These properties are written in IEEE-standard SVA to support either simulation or formal flows.
Among the benefits of these pre-packaged property libraries are fast bring-up (just instantiate and configure), minimal debug of missing constraints, protocol-aware debug in SimVision, and quick sanity checks and coverage points. Indeed, when used with Incisive formal and multi-engine tools, this IP enables users to quickly “bring-up” designs and/or exhaustively verify protocol compliance without a testbench.
Code Coverage Unreachability
Holes in code coverage can take weeks to analyze manually. With this app, a previously tedious, time-consuming process is completely automated such that properties are generated automatically from holes remaining in the simulation regression coverage database. Users can tell at a glance whether code coverage “holes” are reachable or literally impossible to hit. (Of course, this app supports manual designation of “legitimate” areas known to be unreachable in advance.)
Correct register map access and absence of corruption is not checked sufficiently in simulation. By using this app to generate properties automatically for your SPIRIT/IPXACT specification, you can exhaustively check a multitude of common register use cases like value after reset, register access policies (RW, RO, WO), and write-read sequences with frontdoor/backdoor access.
Modern SoCs can have more than 1,000 unique IP components. Even the once-simple pad ring block can have dozens of multiplexed channels that each support out-of-band use cases like BIST and low-power control. Creating testbenches for all of this interconnect is time-consuming and error-prone.
This app leverages your interconnection spec (in an open, human, and machine-readable Excel spreadsheet) to automatically generate and verify properties from the interconnect spec. Users of this app commonly achieve interconnect verification within a single-digit number of hours instead of weeks or months.
Need a Custom App?
Cadence also regularly coaches D&V engineers in creating apps that address their company’s unique verification needs and workflows. Please contact us
with your questions and ideas!