Home > Community > Blogs > Industry Insights > incisive 13 2 verification apps use formal methods to boost productivity
Login with a Cadence account.
Not a member yet?
Create a permanent login account to make interactions with Cadence more conveniennt.

Register | Membership benefits
Get email delivery of the Industry Insights blog (individual posts).


* Required Fields

Recipients email * (separate multiple addresses with commas)

Your name *

Your email *

Message *

Contact Us

* Required Fields
First Name *

Last Name *

Email *

Company / Institution *

Comments: *

Incisive 13.2 – Verification Apps Use Formal Methods to Boost Productivity

Comments(0)Filed under: Functional Verification, Incisive, code coverage, reachability, formal apps, verification apps, X propagation, register map validation, Incisive 13.2, verification productivity 

The Cadence Incisive 13.2 announcement, made today (Jan. 13, 2014), brings unparalleled performance to IC functional verification. But the complete message is not about how fast a simulator can run - it's about improving verification productivity from start to finish for complex SoCs. And one new technology that helps boost productivity in the new release is the use of verification "apps" that employ formal and simulation approaches.

Why the push for productivity? Adam Sherer, product marketing director at Cadence, noted that verification teams constantly have to do more work with the same or fewer resources. And as chip complexity grows, verification complexity grows even faster. The verification challenge is not measured by the number of transistors -- it's measured by the number of storage bits. What's critical, then, is the number of registers and the bits that they store.

Each bit can have a 0 or a 1 value. Thus, when a verification engineer looks at a 32-bit register, he or she sees 232 possible states. "It becomes nuts," Sherer said. "Moore's Law is geometric - 2X [in complexity] every 18 months. But for us, it's 2 to the X every 18 months."

To solve this explosive productivity challenge, we need to look beyond how fast a simulator can run. Pure performance is necessary but not sufficient. And that's where verification apps come in. Verification apps are targeted, automated solutions that bring formal verification technology into the simulation environment, without requiring users to bring in formal verification expertise or write properties in an unfamiliar language. For example, an existing Incisive verification app can evaluate the reachability of coverage holes, making simulation code coverage much more effective.

The Incisive 13.2 release includes new verification apps in these categories:

  • X (unknown) state propagation in simulation
  • Register map validation
  • Exclusion mechanism for code coverage reachability

Verification apps can quickly solve problems that would be very difficult to solve with simulation alone. For example, a complex SoC design may have 30,000-100,000 control registers, and the number of tests you would have to write to verify those registers is "almost beyond human comprehension," as Sherer put it. The Incisive 13.2 register map validation app listed above can perform that task within hours.

Incisive 13.2 has a number of other features, including a new formal verification engine that can speed analysis up to 20X, a new constraint engine in Incisive Enterprise Simulator, new SystemVerilog support in the Incisive Debug Analyzer, IEEE 1647 (e language) unit testing without simulation, and more. The rest of this blog post will focus on the verification apps listed above. For a more complete overview of the Incisive 13.2 release, see our feature story here and the "Top Ten" automation feature list here.

The New Incisive X-Propagation Capability

The Incisive 13.2 release offers an X propagation capability using both simulation and formal technology. This combination helps verification teams find X-related bugs and run reset simulations at the register-transfer level (RTL), thus minimizing the need to run time-consuming gate-level simulations.

Quick background: An X value in simulation indicates an "unknown" state, whereas an X in synthesis indicates "don't care." This difference can lead to mismatches between RTL and gate-level simulation. Further, in RTL simulation, the Verilog Language Reference Manual (LRM) semantics create a situation called "X optimism," in which the simulator assigns a 0 or a 1 in a situation where the value is actually unknown.

The diagram below depicts the X optimism problem. When cond=X, the Verilog LRM semantics calls for the condition to be evaluated as "false," and thus the "else" branch is taken in RTL simulation. But the synthesis tool may optimize cond=X to cond=1, and as a result, the "if" branch will be taken in gate-level simulation. The result is a discrepancy that may take a long time to debug.

Gate-level simulation may run 4X-5X slower than RTL simulation. What is clearly needed is a way to find X propagation issues at RTL. To accomplish this, the Incisive Enterprise Simulator provides these simulation modes:

  • In the FOX mode, the output is always driven to an X when there is an X in control. This may be more pessimistic than the actual hardware.
  • In the CAT mode, the output is driven to a non-X value when both paths match. This typically matches hardware behavior well.

As shown in the diagram above, the FOX mode is more pessimistic (has more Xs) than the CAT mode. Both modes have their place, and neither mode requires changes to the existing HDL design. For a detailed report on how Ambarella used these two simulation modes, see the presentation and/or video from the recent Cadence System-to-Silicon Verification Summit.

In addition to these simulation modes, the existing Super Linting verification app adds X propagation checks in the Incisive 13.2 release. Between this formal technology and simulation, the new release provides a very comprehensive X propagation capability. The Super Linting app generates assertions that can be used in both the FOX and CAT simulation modes, allowing a very exhaustive test.

The X state propagation capability is primarily aimed at reset verification, including power-up reset sequences in low-power design. According to a Cadence customer survey I reported last year, reset verification was the #1 reason for running gate-level simulation, and X optimism in RTL was the #2 reason.

"Reset simulation is absolutely critical to make sure you have working silicon," Sherer said. "Now how are you going to do that? You could have someone grind away with gate-level simulation and watch the screen for X values that are not where they should be. A better way is to replace the gate-level engine with an RTL engine. The second thing is to provide apps that look for bad structures and do some automated checking. That's what gives us productivity."

Register Map Validation and Coverage Exclusion

In the Incisive 13.2 release a new formal app promises exhaustive register map verification within hours, saving the weeks that might be required to generate directed tests. To use it, engineers define registers using the IP-XACT XML format. From this input, the app can generate properties that prove whether or not registers are properly programmed. The app can exhaustively check a number of common register use cases such as value after reset, register access policies, and write-read sequences with front door/back door access (see figure below).

The register map validation app is described in more detail in a recently archived Cadence webinar.

As noted, the Incisive Enterprise Simulation had a coverage unreachability app prior to the 13.2 release. While the app can identify coverage holes in RTL code, this "unreachable" code may or may not indicate a problem in the design. The engineer thus needs to decide what to exclude from the coverage report. A new app in the Incisive 13.2 release helps automate this exclusion process.

In summary, while clocks-per-second verification performance is important, it's necessary but not sufficient.  Productivity includes, but goes beyond, simulator performance. And one way to reach that productivity is through "short cuts" made possible by verification apps such as those in the Incisive 13.2 release.

Further information about Incisive verification apps is included in a new datasheet.

Related Blog Posts

Webinar Report: How Formal "Apps" Ease IC Verification

Functional Verification Survey - Why Gate-Level Simulation is Increasing


Leave a Comment

E-mail (will not be published)
 I have read and agree to the Terms of use and Community Guidelines.
Community Guidelines
The Cadence Design Communities support Cadence users and technologists interacting to exchange ideas, news, technical information, and best practices to solve problems and get the most from Cadence technology. The community is open to everyone, and to provide the most value, we require participants to follow our Community Guidelines that facilitate a quality exchange of ideas and information. By accessing, contributing, using or downloading any materials from the site, you agree to be bound by the full Community Guidelines.