feature article
Subscribe Now

Formal: It’s Still Hard

Oski Discusses End-to-End Block Verification

Formal verification has had a rough go over the years. It came onto the scene with tons of promise, and that promise remains, to some extent, promise. It’s hard to argue against the possibility of taking a spec and a circuit, pushing a button, and watching while some tool provides proof that the circuit is correct.

And watching… and watching… and, well, yeah, that’s where the problems cropped up. Waiting for an answer to some of these problems, if not done carefully, can require suspended animation so that you can be reawakened in some future year or century when the calculation is complete.

Which meant paring down the size of circuits that can be handled, and knowing how to do that properly was hard. So the various companies that make use of formal technology – names like Jasper and Real Intent and OneSpin and even Mentor – had to go back and simplify how the tools are used.

So what you see now are lots of specific applications built over formal technology. Whereas the technology used to be the focus, now the specific problem/solution becomes the focus. The directing of the formal technology to solve that specific problem has already been done, so many of these apps are push-button, to a large extent.

Problem solved, then… right? Well, yes – for those specific problems addressed by those specific applications. So does that mean that the initial promise of formal verification has now been reduced only to the things that can be made push-button? Not necessarily. But the initial challenges remain, making this not for the faint of heart.

All of the formal applications are for verifying specific things as a complement to simulation and other verification techniques. But some folks are trying to leverage formal technology in a manner that makes simulation unnecessary – at least at the block level.

I learned about this in a conversation with Jin Zhang of Oski Technology*. They were introduced to me as a company specializing in formal verification consulting. That jogged me out of my “formal is easy these days” bliss, because if you need consulting for a specific technology like formal, that means it’s hard. And she confirmed this. And the things that are hard are the things that have always been hard.

She describes three levels of formal tool as layers on a pyramid, where the full pyramid represents all the things that could theoretically be done using formal technology. Along the bottom is a stripe for fully-automated applications like clock domain crossings. You can think of these as super-lint or lint-on-steroids tools: they check for very specific problems with your RTL code, and mostly they run with a simple push of the button.

Next is a layer of semi-automatic tools – ones that require some input. An example of this is equivalence checking to ensure that clock gating has been done correctly. And above this layer? Well, here there be dragons. The rest is the wild, wooly space of things that are hard. And that’s where Oski plays. They address the classic issue: verification that would take far too long without hard, specialized work – work that most companies don’t have the expertise to do.

Here’s the deal: full-on equivalence checking means comparing an implementation (your circuit) to a known-good model (from a spec). But doing an exhaustive check means exploring a design space that explodes exponentially as the circuit grows. It rapidly becomes untenable.

Formal vendors have worked hard at taking large circuit blocks and pruning away things that don’t matter, focusing on the cone of influence to narrow the search space. But even so, a subcircuit with only 30 flip-flops will have over a billion states. (OK, slightly over a billion: 1,073,741,824). Cones of influence are extremely likely to have far more flops that this, and so you’re still stuck with an unwieldy solution.

These problems can be made tractable, but that takes some specialized work. Each project that Oski takes on has two major aspects: generating the reference model and abstracting parts of the circuit.

The reference model seems like an obvious thing, but it’s not. The whole point of formal equivalence checking is to prove that a circuit is identical to a known-good model, so you first need that known-good model – and they don’t grow on trees. Typically, this model must be generated from a paper spec. And with the complexity of some of these blocks, this is not trivial. For instance, Oski modeled ARM’s new cache coherency protocol – a project that took about six months.

Of course, this assumes that a paper spec exists. Some companies have a “just do it” philosophy exhorting folks not to write a spec; just write code. So then it becomes an even harder task to assemble a reference model that isn’t itself flawed. The good news is that this process can often uncover problems and ambiguities in the spec.

Once a golden reference is in place, then the circuit can be tested against it. But in order to get a solution in our lifetime, they have to work on the circuit to add abstractions. You might think that this means simplifying various parts of the logic, but, if anything, it means making them larger or more general.

Jin illustrated the counterintuitive nature of this with an example of a resettable counter. Such a counter can take on any value – by resetting and then counting up to the desired state. The effort it takes to acquire any arbitrary state can be reduced by replacing the specific counter with a preloadable version – one that does everything the original counter does, but also allows any arbitrary state to be preloaded directly.

It’s extremely important that the abstracted circuit be a strict superset of the original circuit. You have to add the preload feature, for example, to the specific counter circuit being tested; you can’t replace the whole thing with some other counter. Otherwise, if there were a bug in the original counter, you’d miss it by replacing it with the other counter. So you have to augment the existing circuits, bugs and all, to ensure that you’ll be able to find those bugs.

Of course, this means proving that the abstracted circuit is a strict superset, and that becomes part of the methodology. These abstractions take problems that would take years to converge (or might even have trouble converging) and makes them doable in seconds to hours. Of course, there’s a balancing act – the added logic can result in false negatives, so you want to abstract, but not too much.

Ultimately, given a good reference model and a well-abstracted circuit, you can prove in a reasonable timeframe that a circuit is good (or not) with 100% coverage. And this is what they call an end-to-end proof – once it’s done, you need no simulation of the block. The fact that they can attain 100% coverage – including bugs that would likely not have been found through simulation – makes this what they call a sign-off-quality process.

Not that simulation is going anywhere: the full-up SoC, created by assembling these already-verified blocks into a whole, still requires simulation and other techniques to pass muster. The scale of such a circuit is still beyond what formal can reasonably accomplish by itself; “end-to-end” refers to the ends of the block, not of the IC.

So why can’t any company simply do this themselves? In theory, they can. But, according to Jin, doing this effectively requires people that live and breathe formal; you need dedicated engineers. An engineer who jumps back and forth between formal and simulation paradigms is likely to have a much harder time. So larger companies may form dedicated formal analysis teams; smaller companies, which rely on much more hat-swapping and employee versatility, are less likely to be able to afford that luxury.

Or so Oski believes. They’re still proving their value to companies, with the most effective demonstrations happening when they start finding surprising bugs. That gets people’s attention.

You might also wonder which formal tools they prefer, and the official answer is “none; we’ll use whatever our customer wants us to use.” Oski was founded by the founder of Jasper, so there’s probably a bit of proud papa there, but they say that all of the tools out there have improved their run times and capacity so that they’re all viable. Yes, there are subtle differences in timing, but the big win comes not from using one tool that runs slightly faster, but from the abstractions that slash orders of magnitude off the run time. Everything else becomes less important.

All in all, the lesson from this is that, yes, formal is still hard. Applications have made some very specific uses of formal technology more accessible to the everyday engineer, but fully exploiting the promise of formal verification still takes a cadre of experts to transform a ridiculously tough problem into something doable.


* For you Bear fans, yes… it’s that Oski… with a gratuitous shout out to my son, working at Camp Oski – as soon as the smoke clears enough for folks to go back


More info:

Oski Technology

One thought on “Formal: It’s Still Hard”

Leave a Reply

featured blogs
Sep 22, 2021
3753 Cruithne is a Q-type, Aten asteroid in orbit around the Sun in 1:1 orbital resonance with the Earth, thereby making it a co-orbital object....
Sep 21, 2021
Placing component leads accurately as per the datasheet is an important task while creating a package footprint symbol. As the pin pitch goes down, the size and location of the component lead play a... [[ Click on the title to access the full blog on the Cadence Community si...
Sep 21, 2021
Learn how our high-performance FPGA prototyping tools enable RTL debug for chip validation teams, eliminating simulation/emulation during hardware debugging. The post High Debug Productivity Is the FPGA Prototyping Game Changer: Part 1 appeared first on From Silicon To Softw...
Aug 5, 2021
Megh Computing's Video Analytics Solution (VAS) portfolio implements a flexible and scalable video analytics pipeline consisting of the following elements: Video Ingestion Video Transformation Object Detection and Inference Video Analytics Visualization   Because Megh's ...

featured video

Gesture Detection for Automotive In-Cabin Applications

Sponsored by Texas Instruments

See how using 60GHz radar for automotive in-cabin gesture is ideal due to its small size and ability to sense through various materials. Applications using gesture control include changing radio stations, answering phone calls, opening windows, and more.

Click to learn more about gesture detection using 60GHz mmWave radar sensors

featured paper

Designing an Accurate, Multifunction Lithium-Ion Battery-Testing Solution

Sponsored by Texas Instruments

This paper highlights the benefits of a discrete solution over an integrated solution in order to meet current and future battery testing challenges. It also includes an example of a highly flexible battery testing design.

Click to read more

featured chalk talk

Using the Graphical PMSM FOC Component in Harmony3

Sponsored by Mouser Electronics and Microchip

Developing embedded software, and particularly configuring your embedded system can be a major pain for development engineers. Getting all the drivers, middleware, and libraries you need set up and in the right place and working is a constant source of frustration. In this episode of Chak Talk, Amelia Dalton chats with Brett Novak of Microchip about Microchip’s MPLAB Harmony 3, with the MPLAB Harmony Configurator - an embedded development framework with a drag-and-drop GUI that makes configuration a snap.

Click here for more information about Microchip Technology MPLAB® X Integrated Development Environment (IDE)