After a few decades of watching formal verification techniques being applied to SoC designs, it certainly continues to be a growth market for EDA vendors. In the first decades from 1970-1990 the earliest forms of formal tools emerged at technical conferences, typically written by University students earning their Ph.D.s, and the users had to be at the Ph.D. level to understand how best to use the limited tools and interpret the results for theorem proving. In the next twenty years, 1990-2010 we saw formal property checking emerge, and you still had to manually write the properties and have the domain experience in formal technology. Thankfully, since 2010 to present the formal tool user is a verification engineer that is using a variety of automated formal apps. Now that’s progress.
Siemens/Infineon had their own internally developed formal apps and decided to spin-out a separate company in 2005 called OneSpin, and they’ve been a strong #3 player in the formal market for a number of years now. Just last month Siemens EDA announced the acquisition of OneSpin, adding to what the Questa product family has been offering, so now the combination places Siemens EDA as the #2 vendor in formal apps. It’s kind of rare to find a successful EDA spin-out that was later acquired.
I’ve been following OneSpin ever since I passed by their booth at DAC one year and McKenzie Ross literally pulled me into their booth for an update, maybe it was the DAC badge that said Press or Blogger. Brett Cline is another OneSpin person that I’ve followed ever since his days at Summit Design in 1998. You can follow OneSpin on Twitter, where they are quite active and relevant.
With formal you hear about Assertion Based Verification (ABV) and apps for specific tasks like Sequential Logic Equivalence Checking (SLEC), Clock Domain Crossing (CDC), etc. Mentor acquired formal vendor 0-In back in 2004, and continued to grow the product family over the years. Now Siemens EDA has over a dozen formal apps to choose from, more choice is always better.
Verification engineers have been quick to adopt new tools and methodologies in order to get their job done on increasingly larger designs, with huge state spaces, however the traditional functional simulation techniques are not sufficient to reach verification goals. Adoption of formal methods and apps have enabled verification engineers to complete their tasks more quickly.
Two combined engineering teams instead of competing engineering teams makes sense, to grow the market for formal tools. With a bigger scale comes some benefits of better ideas, and knowing what was already tried before.
The technology combination of OneSpin and Questa Formal will offer users even more ways to automate their verification, and I’ll be interested to learn what the product roadmap looks like.
Customers of both Questa Formal and OneSpin should be happy, knowing that their vendor is investing even more resources in this critical area.
Growing a point tool company into a successful business, then getting acquired by a larger EDA company is a good sign, because it means that the formal product segment is healthy, so expect to see continued news of formal tools being adopted across the hot industries, like: 5G, AI, automotive, IoT, HPC and mission critical fields of aerospace and defense.
There’s always the classic decision of growing your own product line through internal software development, or acquiring a smaller and successful company. I’d say that Siemens EDA made another savvy decision to acquire OneSpin in order to accelerate into the formal market. My favorite list of past acquisitions shows that Siemens EDA has the history of making these deals work out: Berkeley DA, Tanner EDA, 0-In, Model Technology.
- Formal for Post-Silicon Bug Hunting? Makes perfect sense
- Probing UPF Dynamic Objects
- Verification IP proves essential for PCIe GEN5
- “Connecting the Divide” at SEMICON Europa
- Accellera IP Security Standard: A Start
- ESD Alliance CEO Outlook Features Powerhouse Lineup
- Verification 3.0 Holds it First Innovation Summit
- Functional Verification using Formal on Million Gate Designs