I had the good fortune last month to join an eclectic gathering of formal verification enthusiasts in Bangalore, India at the second Special Interest Group event hosted by the Synopsys VC Formal India team. I have attended similar events over the last two decades but seldom one as well organized, drawing attendees from NXP, Intel, Qualcomm, Samsung, NVIDIA, Marvell, Western Digital, Micron, Microchip and other semiconductor companies alongside technical experts from Synopsys.
Yogesh Mittal, Director Verification and Emulation at NXP, kicked things off with a brilliant keynote on leveraging formal for the verification of automotive designs. He described megatrends transforming the automotive industry and the increasing the emphasis falling on functional safety and security. With over 200 million lines of code in today’s cars, the cost of recalls is very high. AlixPartners recently estimated that their total cost in 2016 reached $22B. In response, NXP’s has an overarching strategy: ‘Vision Zero’ aims for zero collisions, zero emissions, and zero congestion.
Mittal described how his company deploys formal to find bugs that would be difficult to detect in simulation. NXP’s view is that there is no safety without security and both are equally important to address. With increased hacking of connected cars being reported online, security verification is a ‘must-have’ where formal plays a crucial role. Mittal further noted that for functional safety, there is a rising focus on fault injection, with the latest ISO26262-1:2018 specification recommending the use of formal methods.
The next talk was a Synopsys keynote that looked at breaking new frontiers in formal verification. It was delivered by Kiran Vittal, Senior Product Marketing Director, and Pratik Mahajan, Director, R&D.
VC Formal grows through differentiation
Vittal said that deployment of the company’s VC Formal suite has grown three times over in the last 20 months. Today, significant number of users look to the differentiated features within it. These include formal regression mode acceleration (RMA) with machine learning, formal testbench analyzer (FTA) apps for fault injection (Synopsys offers this using the native Certitude technology), adaptive orchestration for more proof convergence, and several deep bug-hunting features.
Mahajan presented Synopsys’ new datapath verification (DPV) app. It integrates the HECTOR proof technology within VC Formal in a distinctive approach to tackling both control and datapath verification. With new technology enabling automatic invariant computation and Verdi integration, HECTOR can be used without much user intervention. Other significant advancements in VC Formal include a dashboard visualizer that displays overall results from multiple formal projects, and NLP based Smart Search that allows users to conduct native language search across documentation within the tool.
My own presentation offered a taster of our Axiomise formal verification training based around a tutorial on how to make formal verification predictable and scalable. It covered methodologies for RISC-V processors and networking designs and showed how the recently designed ISA formal proof kit from Axiomise found over 70 bugs in zeroriscy and ibex RISC-V cores including deadlocks, X-checks, lockstep failures and security vulnerabilities. It also described simple yet powerful techniques for finding bugs and building proofs of bug absence for networking designs.
NXP adds metrics for formal signoff
I was followed by Gaurav Jain, Principal Staff Design Engineer with NXP. He talked about how the company uses a metric-driven methodology for SoC verification. Where connectivity checking and code coverage are used in standard SoC level verification, specific steps are taken by NXP engineers to obtain signoff addressing issues of over-constraints, quantifying property density, deploying the FTA App for fault injection, and computing formal cores – with each stage finding holes in verification.
The formal testbenches are reused in regressions to make sure formal constraints are validated in-situ, and coverage is re-analyzed. Jain said that the best part of running regressions is the speed-up obtained by the machine learning-based formal RMA app within VC Formal.
The next tutorial was by Nitin Ahuja and Anders Nordstorm from Synopsys. They described the use of safety and security solutions from Synopsys for mission-critical applications.
Ahuja focussed on functional safety solutions. He described how the formal apps from Synopsys uncover bugs for systematic faults, and also provide the last slice of coverage closure for random faults. One of the biggest challenges with random faults is understanding fault propagation. Ahuja explained how formal solutions augment results from a Z01X fault simulator to offer a complete analysis for fault propagation.
Nordstrom discussed how new security solutions from Synopsys help customers find security vulnerabilities at the RTL level, before the design reaches silicon. Using a combination of assertions and proprietary solutions from Synopsys, Anders reported obtaining tremendous success with its customers.
The last tutorial was by Siddartha Papineni from Synopsys. He discussed strategies for solving datapath verification problems.
Papineni explained why datapath verification is one of the hardest verification problems and how the VC Formal DPV app addresses this problem. He shared information on fundamental concepts, convergence techniques and the methodology, as well as the results from recent case studies to lay out what it takes to verify datapath centric blocks.
The last technical event of the day was a vibrant panel discussion chaired by Ravindra Aneja, Director, Application Engineering at Synopsys. I joined Ashok Natrajan from Intel, Ipshita Tripathi from Qualcomm, and Pratik Mahajan to discuss the current challenges in adopting formal. We talked about what makes formal standard in organizations and how training, accompanied by active management buy-in, can change the game for formal in different teams.
Aneja asked the panel whether we need more specialists or generalists in teams, and the panel broadly agreed that while a couple of specialists (experts) can drive wider adoption, a more hands-on approach is needed to enable more designers and verification engineers to get an early start in taking advantage of formal techniques.