Cadence today (June 16, 2014) announced the completion of its acquisition of Jasper Design Automation, a leading provider and pioneer of formal analysis and verification tools for IP and system-on-chip (SoC) development. The acquisition allows Cadence to expand an already broad functional verification offering with the Cadence® System Development Suite, and it expands Cadence's formal portfolio just as that technology is coming into mainstream adoption.
While simulation generates directed and random stimulus to devices under test, formal analysis—generally done at the block level, and increasingly at the SoC level for specific tasks—provides a mathematical proof that determines whether a given behavior will always or never occur. Formal analysis is fast and exhaustive, but it needs to be guided to focus on issues related to how the design will be used. Recently, Cadence and other providers have offered "semi-formal" tools that combine both simulation and formal analysis, and both Jasper and Cadence have been delivering formal "apps" for specific verification issues.
Formal verification is a broader term that also includes formal equivalency checking, which compares two netlists (such as before and after synthesis) to ensure that netlists are functionally equivalent. Although Jasper is best known for formal analysis, the company recently developed a sequential formal equivalence checking capability. In contrast to logical equivalence checking, sequential checking can verify that low-power and performance optimizations don't impact functionality, even when those optimizations cause logic to move across clock cycle boundaries.
What Jasper brings to the table
Jasper was launched as Tempus Fugit in 1999 and became Jasper Design Automation in 2003. The company focused on formal analysis from the very beginning, and its core technology is called JasperGold®. This platform delivers a formal proof capability ranging from assertion-based verification (ABV) to exhaustive end-to-end proofs of micro-architectural-level properties. JasperGold has multiple formal engines, a Formal Scoreboard, and Proof Accelerators.
Jasper offers a selection of JasperGold apps, which offer targeted solutions that address specific design and verification challenges. For example, the X-Propagation Verification App helps verification engineers avoid "X state optimism" (assigning a 1 or a 0 when the value is truly unknown) and "X state pessimism" (assigning an X when the value actually is known). This situation arises because of a semantic mismatch—an X is an "unknown state" in simulation but is a "don't care" in synthesis.
Jasper formal apps are shown in the following chart:
Another Jasper offering consists of Intelligent Proof Kits and Verification IP. These allow engineers to accelerate verification by quickly and exhaustively certifying standard interface protocols such as ARM® AMBA® (AXI 3/4, ACE, API, APH, APB), DDR 1/2/3, LPDDR 1/2/3,SDRAM, DFI, Ethernet, OCP, and others. The kits, optimized for formal analysis, eliminate the need to write properties manually, and also plug seamlessly into the simulation environment.
How Cadence completes the picture
Cadence has some strong formal analysis technology as well. The Incisive® Formal Verifier provides assertion-based verification and debug of RTL block-level designs. The Incisive Enterprise Verifier uses integrated formal analysis and simulation engines to uncover bugs deep within a design. Cadence has also developed formal apps in such areas as register map verification, memory map verification, X propagation, coverage unreachability, and connectivity checking.
So what's the difference? According to Michał Siwiński, vice president of product management and marketing for the System and Verification Group at Cadence, formal technologies from Jasper and Cadence are highly complementary. Cadence, for example, has put a lot of attention on the Assertion-Based Verification (ABV) flow and on connecting formal analysis with simulation, and most of the Cadence formal apps do this to some extent. Jasper, in contrast, has mainly developed advanced formal tools with exceptional formal debug and analysis capabilities. Moreover, Jasper brings innovative sequential equivalence checking technology to Cadence.
Siwiński noted that over 70% of the customer hardware "spend" continues to go into verification, and over 80% of development spend for an SoC is split across software, verification, and validation. For this reason, Cadence has been increasing its investment in system design and verification both through acquisitions and internal efforts for a number of years. Previous acquisitions have included Verplex (formal equivalency checking and property checking), Verisity (coverage-driven verification), Denali (verification IP), and Forte (high-level synthesis).
With a wealth of system and verification technology, Cadence has focused on developing integrated end-to-end solutions. "We are the leader with the broadest and most complete platform," Siwiński said. The System Development Suite, first announced in 2011, combines formal, simulation, acceleration and emulation, and virtual and FPGA-based prototyping. It also offers verification IP, planning and management, integrated debug, and focused solutions for low-power, mixed-signal, and ARM-based SoCs. Since the Jasper tools will bring more formal capabilities to the System Development Suite, customers will be able to deploy more cohesive flows for developing high-quality products amid growing schedule pressures.
Go with the flow
Many customers are already using Jasper formal apps along with Cadence verification flows. Other Jasper customers are using Synopsys or Mentor Graphics flows. The Jasper tools are very modular and can run in any environment, Siwiński added. "We'll make sure to complement and augment the overall Cadence solution to provide the best user experience, but if somebody is using that [Jasper] technology with a Synopsys or Mentor flow, we'll support that just as we do with Verification IP," he said.
Another win for Cadence is Jasper's strong R&D and field team. As the premier provider of formal analysis tools, Jasper has some of the world's foremost experts in formal technology. "Jasper has an amazing team, full of deep expertise and passion for customer success, and we are happy for them to be part of Cadence," Siwiński said. He noted that "the team will be a substantial addition to further expand our system and verification division, and our ability to effectively help customers improve their development process."
Even before the Jasper acquisition, Cadence had the industry's broadest system and verification portfolio, Siwiński said. The Jasper purchase "provides another area where Cadence is by far the thought leader with market-leading technology. We already do that around metric-driven verification, UVM multi-language simulation, acceleration, and emulation with Palladium® XP II, Verification IP, high-level synthesis, mixed-signal verification, low-power verification, and ARM-based system verification. There are a number of areas where we are really strong, and we are extending that even further. In turn, this enables us to be the partner of choice for market-leading customers."
Related blog posts
- New Incisive vManager Keeps Functional Verification Costs in Check
- Videos, DVCon 2014 Papers—Formal Verification "Apps" Move to SoC Level
- New Incisive Verification App and Papers at DVCon by Marvell and TI
- Incisive 13.2—Verification Apps Use Formal Methods to Boost Productivity