The formal verification market is still untapped
The formal verification market is still untapped
Dr. Olivier Coudert
Getting actual figures about the size of the functional verification market proves to be elusive because of the way the products are tied to synthesis license deals, and because of the lack of independent analysts in EDA. Still, the simulation and emulation market of digital systems can be estimated to be at least five times larger than today’s formal verification market. But simulation can only take you so far, so one wonders why formal verification does not have a larger share. Is it because the technology is limited, or because the market is not ready?
Model checking and property verification
Because writing properties can be so complicated, specialized branches grew to address specific needs, as shown below.
• Timing verification. Incorrect timing constraints can lead to missing a target clock cycle, or worse, to a chip failure. Verifying timing exceptions (false paths and multi-cycle paths), as well as CDC (Clock-Domain Crossing), has become a center of attention. It is still unclear how big the market is. However several discussions with IC design companies led me to believe that verifying a set of timing exceptions (usually in the order of 10,000 SDC constraints) save one month work of an engineer. Automation and speed are keys here. . Atrenta, Real Intent, and 0-in propose interesting solutions in that space.
• Sequential clock gating verification. Traditional (combinatorial) clock gating is well supported by EC tools. Sequential clock gating exploits sequential dependencies to derive additional gating conditions, which can be used to save more dynamic power. It has been made popular by Calypto –Envis is also proposing a similar technique at the netlist level. Sequential clock gating correctness cannot be expressed easily with SVA or OVL without making the verification task extremely complex, which explained why specialized verification techniques have been developed.
Formal verification is no longer limited to ASICs: complex systems –SoC, FPGA, and HW/SW co-design— will benefit dramatically from better formal verification techniques if they are deployed adequately.
With the ever-growing size of FPGAs (Altera’s Stratix IV packs 820k logic elements, and Xilinx’ Virtex-6 has up to 750k logic cells), it is clear that simulation will no longer be sufficient to validate the correctness of programmable logic devices. The need for FPGA EC is real, and this requires complete automation and full support for retiming –OneSpin’s 360 EC FPGA has shown some competitive solution in that space. Also note that IP verification and timing verification apply to the FPGA designs too. The real question is whether FPGA designers are willing to pay for formal verification tools.
IP verification, and verifying the correctness of a SoC using IPs, is certainly a very strong driver for more sophisticated formal verification solutions. Power verification will become part of the ASIC design flow, as EC is part of the synthesis flow. Timing verification is still looking for its footing in the design flow –one question is the debug environment, which is still relatively limited, e.g., to showing waveforms.
Looking forward, formal verification techniques can be used (and have been used) in other fields than circuit design. Any critical digital system can benefit from formal verification techniques –transportation, medical equipments, security and privacy applications. The automotive industry is one of the most obvious targets. Cars are ubiquitous, they contains more and more electronics (representing about 30% of the end price today), and a functional bug can have very costly consequences. Cars rely on digital systems for anything from optimizing their engine’s efficiency to navigation systems, entertainment, and on-board diagnosis. Soon the intra-vehicle, vehicle-to-vehicle, and vehicle-to-roadside networking will fuel innovative products, driving the needs for fast development and the highest possible level of correctness. The EDA industry is taking notice, and Mentor has certainly taken the lead there. Whether they provide the adequate functional verification framework is another matter.
Formal verification will extend its reach by addressing the hard problems of EC (datapath verification, and retiming for FPGA), by being seamlessly integrated in the synthesis flow (power and timing exception verification), and by providing practical solutions to IP and hybrid HW/SW design verification.
Dr. Olivier Coudert has 20 years experience in software architecture and EDA product development, including 10 years in research. He received his PhD in Computer Sciences from Ecole nationale supérieure des Télécommunications, Paris , France , in 1991. He has published 50+ papers and book chapters, and he holds several patents on combinatorial optimization and physical synthesis. He is a recognized expert in the fields of formal verification, logic synthesis, low power, and physical synthesis. He led the development of several EDA products, including 3 from scratch in a startup environment. You can follow Olivier on Twitter, meet him on LinkedIn, or read his blog.