A group of formal verification specialists is now blogging at InFormal Chat on the Synopsys website.
The team, which includes experts with wide experience in applying formal methods to the verification of digital design, has touched on number of key formal issues in their blogs on the site.
The two most recent blogs focus on what you can learn about formal verification at this week's Design Automation Conference, currently underway in Austin, Texas.
Anders Nordstrom, whose blogs have appeared here on Tech Design Forum, gives an overview of formal activity at DAC, from presentations and poster session through to Thursday's training day opportunities to learn in more depth about specific techniques, such as formal verification using SystemVerilog Assertions.
Sean Safarpour, CAE director of VC Formal at Synopsys, offers his thoughts on the rise of machine learning and artificial intelligence techniques in verification, one of the focuses of this year's DAC. His view? Lots of people are talking about it, but Synopsys has real data to show how using these techniques can improve the performance and convergence of formal properties by automated analysis of regression test logs.
Other blogs cover issues such as deliberately introducing bugs into design code (a so-called 'RTL mutation' strategy) to see whether your current verification suite can detect them – hence giving insights into the depth of your fault coverage. The blog, by Xiaolin Chen, includes an example of the strategy at work.
Iain Singleton, formerly part of the advanced verification methodologies group at graphics processor IP company Imagination Technologies but now at Synopsys, uses his blog to explore the knotty issue of creating the right set of constraints for your design. Set too few constraints and bugs may slip through unnoticed. Set too many constraints and they could disallow some valid behaviours of the design. Singleton reflects on how new tools can help verification engineers get to the Goldilocks solution for their constraints – not too many, not too few, but just right.
Ravindra Aneja's blog discusses the tradeoff between benefits accrued and effort expended in the application of formal verification strategies. There's a useful graphic that maps the work involved in using each of a set of techniques against the verification complexity it addresses, and a discussion of the utility of applying a couple of the techniques.
A second blog by Sean Safarpour explores the development of formal verification techniques over the past ten years, and offers three reasons why the technique is now being more widely applied. What are they? It's all in the blog...