Jul
Innovations in formal verification
Last week, I received another press release from Jasper Design Automation that talked about advances they have made in a number of areas, including performance (a 2X increase in speed/memory footprint), packaging (common backend for several front ends) and technical (introduction of quiet trace and more parallel operations). This is not the first major product announcement that they have had in the last year. Towards the end of the year, there was the announcement of ActiveDesign – a product that really excites me. For full disclosure, I am on the technical advisory board of Jasper.
This got me to thinking about the other companies that have formal tools. Mentor and Cadence have been active in this area in the past, as has Synopsys. Real Intent seems to have gained some stability in CDC, a product category also being fought by many of the other formal companies. But I do not remember seeing any announcements from any of these about significant advances for quite some time. I went back and checked – nothing that I could find on the Mentor site for the past year, nothing substantial for Real Intent, nothing for Cadence. Calypto is still a relatively new entrant, but attacking a different market (sequential equivalence checking), for which they still have the market to themselves.
At the same time, Bill Murray in a recent article on SCDsource showed that usage of formal technologies had doubled over the past 3 years, which means that there is a real need and growing adoption of these tools. Jasper CEO Kathryn Kranen talks about 100% bookings growth for Jasper in 2008 compared to 2007 on Deepchip. So are the other companies just not talking about their technical advancements, or are they just trying to get what they have working properly? Are they giving up and leaving the market to the only one who appears to be innovating? Is Jasper becoming the formal gorilla?
Brian,
I think the other big EDA companies are only issuing press releases for a few things: multi-million dollar new deals or renewals, brand new tools.
So something like an update to a formal tool isn’t big enough to warrant a press release.
Let’s see if this latest release from Jasper is countered by Cadence, Mentor or Synopsys.
July 13th, 2009 at 6:59 pmJust a couple of days after posting this entry, Real Intent put out a press release (July 16th). Here is a clip from it.
Explicit and implicit X sources (X assignments in RTL and non-resettable flops, respectively) in the designs can lead to many challenging issues for design verification, such as masking real design errors and causing RTL-to-netlist simulation mismatches. Depending on coding styles, simulation results can be X-pessimistic which lead to unnecessary unknown values; or X-optimistic which results in known values when they should have been unknown. Design and verification teams write properties to trap Xs or instrument 2-value simulation with random initialization to avoid X ambiguity in order to detect design errors. However, these approaches take considerable amount of manual and computational resources without offering the complete confidence of X robustness.
Ascent PBV offers a multi-faceted solution that addresses the problem through structural and formal analysis, as well as by augmenting simulation using Ascent SimPortal. Explicit and implicit X sources are automatically detected. Innovative formal techniques are used to prove X-optimism safe designs. Ascent SimPortal can augment simulation to detect X-excitation, control X-pessimism, as well as eliminate X-optimism without loss of efficiency. It is the first automatic and comprehensive solution to detect and debug design errors and RTL/netlist simulation mismatches.
I have to admit that I do not know if the other formal companies have anything similar in their products, but the technique is not new. Randy Bryant published a paper entitled “Formal Verification of Digital Circuits Using Symbolic Ternary System Models” at CAV back in 1990.
*********************************************
July 15th, 2009 at 6:04 pmBrian Bailey
The “Mixing Formal and Dynamic Verification” article by Murray was an interesting one, documenting continuing gains in adoption of formal. It’s not clear from his survey what tools were used by the 19 engineers at 16 companies (which strikes me as too small sample size to draw too large a set of conclusion from, but it’s certainly interesting) so it’s hard to tell which vendor’s tools are being adopted, Gary Smith might have more data. Synopsys, Mentor, and Cadence have a number of areas they compete in, Jasper really has just one: all of their press releases will be about formal.
The other thing to bear in mind is that press releases are primarily useful for communicating with non-customer prospects. Cadence, Mentor, and Synopsys can use their sales force and newsletters to message customers directly, and these will be the easiest to convert for them. So it’s not necessarily the case that they are not continuing to invest and roll out upgrades to their formal tools.
Thanks for the pointer to the Murray article, it was well researched and insightful.
July 16th, 2009 at 3:14 am