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, … Read More
Tag: formal
Formal for Post-Silicon Bug Hunting? Makes perfect sense
You verified your product design against every scenario your team could imagine. Simulated, emulated, with constrained random to push coverage as high as possible. Maybe you even added virtualized testing against realistic external traffic. You tape out, wait with fingers crossed for first silicon to come back. Plug it into… Read More
A New ML Application, in Formal Regressions
Machine learning (ML) is a once-in-a-generation innovation that seems like it should be applicable almost everywhere. It’s certainly revolutionized automotive safety, radiology and many other domains. In our neck of the woods, SoC implementation is advancing through learning to reduce total negative slacks and better optimize… Read More
The Wolper Method
If you read around topics in advanced formal verification you’re likely to run into something called Wolper coloring, or what Vigyan Singhal (Chief Oski at Oski) calls the Wolper method. Many domains have specialized techniques but what’s surprising in this instance is a seeming absence of helpful on-line explanations (though… Read More
When FPGA Design Looks More Like ASIC Design
I am sure there are many FPGA designers who are quite content to rely on hardware vendor tools to define, check, implement and burn their FPGAs, and who prefer to test in-system to validate functionality. But that approach is unlikely to work when you’re building on the big SoC platforms – Zynq, Arria and even the big non-SoC devices.… Read More
Meltdown, Spectre and Formal
Once again Oski delivered in their most recent Decoding Formal session, kicking off with a talk on the infamous Meltdown and Spectre bugs and possible relevance of formal methods in finding these and related problems. So far I haven’t invested much effort in understanding these beyond a hand-waving “cache and speculative execution”… Read More
Formal: Going Deep and Going Early
This year I got a chance to talk with Cadence at DVCon on a whole bunch of topics, so expect a steady stream of blogs over the next couple of months. First up was an update from Pete Hardee (Director of Product Management) on, surprise, surprise, formal verification. I’m always trying to learn more about this space, so I picked a couple… Read More
An Advanced-User View of Applied Formal
Thanks to my growing involvement in formal (at least in writing about it), I was happy to accept an invite to this year’s Oski DVCon dinner / Formal Leadership Summit. In addition to Oski folks and Brian Bailey (an esteemed colleague at another blog site, to steal a Frank Schirrmeister line), a lively group of formal users attended… Read More
Concluding Inconclusives
Formal methods are a vital complement to other tools in the verification arsenal, but they’re not without challenges. One of the more daunting is the “inconclusive” result – that case where the tool seems to be telling you that it simply gave up trying to figure out if a particular assertion is true or false. Compounding the problem,… Read More
Simulation and Formal – Finding the Right Balance
Simulation dominates hardware functional verification today and likely will continue to dominate for the foreseeable future. Meanwhile formal verification, once thought to be a possible challenger for the title, has instead converged on a more effective role as a complement to simulation. Formal excels at finding problems… Read More