Few individuals have been as visible and influential in the EDA industry as Kathryn Kranen, CEO of formal verification pioneer Jasper Design Automation until its acquisition by Cadence in June 2014. Kranen was also CEO of Verisity Design in the late 1990s, and she served as chairman of the EDA Consortium for two years until the Cadence acquisition. Today she is corporate vice president and general manager for formal and automated verification at Cadence.
In this interview, Kranen talks about her 25+ year history with EDA, how functional verification has changed, how formal technology fits into the IC verification flow, why Jasper developed formal "apps," and the advantages of the Cadence acquisition.
Q: Kathryn, you've been part of the EDA industry for a long time. Can you comment on how you got started with EDA and note a few milestones?
A: In 1987, I joined Daisy Systems as an applications engineer. I joined Daisy because I had been a user of their tools. As an engineer for Rockwell International in Richardson, Texas, I was designing ASICs using Daisy schematic capture and gate-level simulation tools.
I started at Quickturn in the early 1990s as a first-time salesperson, and I left as vice president of North American sales. I left in 1996 to go to Verisity. I was CEO of Verisity Design Inc., the US subsidiary of Verisity Ltd. in Israel. In the three years I was there, the company went from six people in Israel to 80 people worldwide, and became profitable.
At the end of 2002, I became involved with a small startup providing mostly verification services, named Tempus Fugit. I joined as CEO, raised the next round of funding, and launched the company as Jasper Design Automation in March of 2003.
Q: Why did you stay in EDA for all these years? And why functional verification?
A: I love EDA, and being part of enabling engineers to build all the great electronics systems that improve our daily lives. As an engineer myself, I like the technical variety I experience as an EDA provider. It is really fascinating to compare and contrast different customers' engineering cultures, management styles, and product architectures.
Design is constrained by what you can verify. The more we can make things verifiable, the more we free up design possibilities. Other people in EDA focus on implementation and do a great job of it. To me, the action and the fun are in the concept-to-functionality phase.
Q: How has functional verification changed since you first got involved with it?
A: 28 years ago I was at Rockwell using schematic capture and gate-level simulation to design a 50K gate ASIC. To create simulation stimulus, I used a text editor to write ones and zeros in rows for each half clock cycle. I asked Daisy software developers if they could give me a simulation pie chart so I would know how much of the verification had been completed.
Today we can verify billions of gates. So many things are automated now. RTL raised the level of abstraction, constrained-random took away the burden of manually creating stimulus, and coverage and metric-driven verification provide feedback on how effective the stimulus is.
Q: How does formal verification fit into the overall functional verification process?
A: We used to think formal was only about getting a full proof, and proving the absence of bugs. That's where Jasper started with formal 11 years ago. What we've learned since then is that the greatest value of formal is offloading as many bugs as possible from simulation, with less engineering effort and much earlier in the design cycle. By cleaning out those bugs, you have fewer iterations of simulation, and things are easier to debug.
One customer told us that 40% of the total bugs in a huge graphics chip were found by formal verification solutions, and 84% of those were found using a completely automated approach.
Q: Verisity (acquired by Cadence in 2005) helped change the verification landscape with technologies such as constrained-random verification, verification planning, and coverage-driven verification. In your view, what did Verisity bring to verification?
A: Verisity allowed the engineer to think less about the stimulus and more about the checks, and to achieve much higher productivity. That's also true in formal. So in some ways, Verisity was a stepping stone.
In the early days of constrained-random simulation, the Verisity tool became a de facto industry standard. Previously companies were writing C models and scripts and trying to automate their own stimulus creation. But once the Verisity Specman tool became so widespread, it gave the whole industry the opportunity to collaborate more on methodology. Ultimately, UVM became a methodology based on the concepts of constrained-random, coverage-based, metric-driven verification.
Q: How did you get involved with Jasper?
A: Verisity brought in Moshe Gavrielov as CEO when I was 8 months pregnant. I had my baby, came back and did some strategic planning, and continued to run sales and marketing. I stayed for about a year working for Moshe and then left, and I was blissfully "retired" (though consulting pretty actively).
I got a call from a former co-worker asking me to meet the founder of a company named Tempus Fugit and share some advice. I did that over lunch, and then later was approached by Mike Schuh of Foundation Capital, one of the few venture capitalists who invested in EDA. He was considering making an investment in the company but said he would only invest in a CEO that he knew, and asked if I was interested. I said I was retired, but I couldn't get the opportunity out of my head.
I called him back a few months later and took the bait. I performed the remaining due diligence for both Foundation Capital and myself.
While developing the business plan, we made a decision that to grow the company we needed to focus on being a tool provider. I was able to secure the funding from Foundation and joined as CEO.
Q: How did things turn out at Jasper?
A: We had a "near-death" experience in the 2005-2006 timeframe when the formal market seemed to stall. The founders left the company and sold all their shares. Many employees left. Those of us who stuck it out kept chipping away at market obstacles. We built up a new engineering team and re-architected the product.
In 2008, we created a new business model, and revenue started taking off pretty steeply. By 2010, we were profitable, and we have been profitable every quarter since mid-2010. We had 145 people at the time of the [Cadence] acquisition, and with a few exceptions, the entire AE team and the entire R&D team joined Cadence.
Q: What do you see as Jasper's biggest contribution to the EDA industry?
A: I think the biggest contribution was bringing formal property verification to the mainstream. Earlier it was viewed as an expert tool that was never going to proliferate. Jasper made formal not only more usable, but so sticky that, last time we did a survey, 40% of our users were designers of RTL themselves. Case studies show that engineers are two to two and a half times more efficient in finding bugs with formal than with simulation. We've come a long way from the time when people assumed you needed a PhD in formal verification.
Q: Speaking of usability, Jasper's recent focus seems to be on formal "apps." How do you define a formal "app" and why did Jasper take this approach?
A: I define an app as a product that is licensed and sold separately. We have a lot of JasperGold Apps for specific verification tasks, like SoC connectivity, X-propagation detection, configuration and status register verification, and sequential equivalence checking, to name a few.
We started with JG-Apps about two and a half years ago. Previously we had one single product called JasperGold that could be used for a wide range of problems, from simple things like block-level connectivity up to complex problems like system-level deadlock detection. The support burden would be very low for simple problems and very high for sophisticated ones.
Because it was so versatile, JasperGold was very hard to price. By re-architecting the software and separating the product into apps, we made everything licensable, so we could sell the lower end solutions very inexpensively and get customers on board sooner.
Q: From your point of view, what are the advantages of the Cadence acquisition?
A: Now Jasper's formal technologies can be leveraged across the broad verification platform. As Jasper CEO, I could see that Cadence's formal-assisted simulation capabilities, like coverage unreachability, were very popular in the market. Only Jasper didn't have a simulator! So now, instead of trying to compete against the vision of formal-assisted simulation, we can enable it and drive it as fast as we can. Another benefit of being part of Cadence is that it is so much easier for a verification manager or project director to bring in a new solution from their existing supplier than it is to bring in a brand new supplier.
Cadence was definitely our toughest competitor. Jasper had the highest market share [in formal] and Cadence had the second-highest market share. Combined, we have more than half the market. I'm happy we're all together now, instead of battling it out in the field. We combined the R&D resources from both sides and now have the largest formal R&D team on the planet.
Related Blog Post
- Why Cadence Bought Jasper—a New Era in Formal Analysis