Industry Insights Blogs

In mid-2014, Cadence completed its purchase of Jasper Design Automation, and became the overnight leader in the formal verification market. Many Jasper formal verification experts came to work for Cadence, among them Oz Levia, who, as vice president of R&D, leads the new Formal and Automated Verification (FAV) business unit at Cadence.

In this interview Levia talks about how formal technologies complement simulation, how automated formal “Apps” directly solve specific problems, what Jasper contributed to the success of formal verification, who uses formal technology and how, and where Cadence is taking formal verification in the future.

Q: Oz, what were you doing at Jasper, and what are your responsibilities at Cadence today?

A: I had three different roles at Jasper. When I first joined about 4½ years ago, I was vice president of marketing. Then I was in charge of business development, which involved relationships with potential suitors. In addition, I was corporate counsel for Jasper.

At Cadence, I’m in charge of the Formal and Automated Verification business unit. I’m responsible for product development, the product roadmap, the R&D schedule, and customer support.

Q: Commercial formal verification goes back to the early 1990s. At that time, there was a notion that formal verification would compete with, and perhaps even replace, simulation. Today, however, formal verification and simulation are viewed as complementary. What has changed since those early days?

A: I think there was some misplaced marketing very early in the life of formal verification. 15 or 20 years ago, there was an assumption that formal could replace simulation completely, but this ran headlong into limitations in accuracy, capacity, and performance.

At Cadence, we have been able to co-operate not just with simulation, but with other verification methodologies. We look at the strong points of each of the technologies. Formal is very useful for design bring-up, bug hunting, debugging, IP verification, and connectivity, control, and status register verification. It’s also useful for doing equivalence checking with ECOs or low power. It does not replace the need to do full gate-level simulation with timing, or other kinds of functional verification tasks, like emulation and prototyping.

Q: Can you provide examples of how formal verification can work with simulation?

A: Unreachability is one example. We all know that at some point, after the testbench has had a chance to run for a very long time, coverage starts to level off. It gets very frustrating for engineers who are trying to understand why they’re not reaching the coverage they want.

Unreachability analysis helps by finding areas of the design that are not reachable, no matter how many test vectors you throw at them. Once you discover these points, you can modify your testbench, try to create dedicated tests, or debug the functional cause that prevents certain parts of the design from being reached. If it’s okay that the part of the design in question is unreachable, it can be waived and removed from the coverage metrics, saving time and effort needed to achieve coverage closure.

Another way that formal and simulation are co-operating is with coverage. On the simulation side, people start with such approaches as code coverage, line coverage, expression coverage, and functional coverage. In formal, the coverage concepts are slightly different, but the integration of both the formal and simulation coverage results in one database that provides the user with much faster closure. It also tells the user what ROI they are getting for different investments in technologies such as formal, simulation, and emulation.

Q: Formal verification used to require a lot of expertise on the part of the user—PhD-level expertise, some would say. Is this still the case or is it changing?

A: It is changing. We have democratized access to the power of the technology. We are focusing on the problems the design and verification user has. We don’t promote formal for formal’s sake, we promote solutions.

If they do low power and change the design, we have sequential equivalence checking. If they have a design that has a lot of reset and initialization, we promote X-propagation verification. If they have a design with secure registers or storage, we provide a solution that verifies secure register access. We have over a dozen different solutions in which the user does not need to have expertise in formal. They just have to be knowledgeable about their problem.

Another way we help the user is with automation. In many cases the user doesn’t have to write properties. Many of our applications do this automatically today.

Q: You’re apparently talking about the focused programs that Jasper and Cadence, prior to the acquisition, offered as formal verification “Apps.” How did this concept get started at Jasper?

A: Several years ago, Jasper had only one product. It was called JasperGold. You could apply that product to many things, but the application was left to the user. We decided to create solutions that solved particular problems.

Each of these solutions required its own use model. If you are working on connectivity verification, for example, you can use hundreds of licenses simultaneously. But if you’re working on architectural verification, you’re probably using one license per user. From a business perspective, these are not compatible. It was very logical to split our technology into “Apps” and price according to value.

Q: The “Apps” concept was one contribution that Jasper made to the field of formal verification. What other contributions did Jasper make?

A: From a technology standpoint, if you look at the Jasper patent portfolio, many of the fundamental improvements in formal technology during the last 15 years originated with Jasper. One such technology is Visualize. It’s not a product we sell by itself—it’s an interactive console for all the apps and it’s a very advanced formal debugger. And it’s a lot more than a debugger, it’s a complete design comprehension system.

Jasper also made it possible to handle far greater capacity for much larger designs, and to be able to do proofs with much greater speed and depth. Another important contribution that Jasper made was in getting formal verification accepted, not only as a legitimate verification technology but also as an indispensible one.

Q: The Cadence acquisition is about a year old. What were the original goals and what has been accomplished?

A: We first surveyed the technology we have from both Cadence and Jasper, and created a roadmap for the future. It’s not only a plan for product delivery, it’s a roadmap for new technology. Early on we decided that JasperGold was going to be the platform going forward. About 45 days after the acquisition, we already had an integration plan in place. Today the integration is progressing according to schedule.

Q: Who uses formal verification today—designers, verification engineers, or both?

A: The answer is both. We have many customers in which design teams use formal verification as part of the development process of their RTL. Because Visualize is based on formal technology, designers can debug, hunt for bugs, and comprehend their designs.

Verification engineers are using technologies like connectivity, X-propagation, and control and status register verification. Today we’re seeing that formal technology is making its way into regression testing. A few companies are even using formal checking as a signoff methodology.

Q: What goals does the Cadence FAV business unit have for formal verification going forward?

A: First, we want to increase the capacity and the performance. I don’t just mean run time—I mean depth of proof and the ability to handle larger and larger designs. A second focus is extending the solution space that formal can address. There will be more apps, more products, and more value. A third direction is forging links with other Cadence products, not just simulation but also emulation, verification IP, Conformal products, and more. There are many places in the Cadence ecosystem that can benefit from formal technology.

Richard Goering

Related Blog Posts

- JUG Keynote—How Jasper Formal Verification Technology Fits into the Cadence Flow

- JUG 2014: Cadence Unveils Ambitious Roadmap for Formal Verification

- Why Cadence Bought Jasper—A New Era in Formal Analysis