Visual Debug for Formal Verification

Success with Open-Source Formal Verification

The dream of 100% confidence is compelling for silicon engineers. We all want that big red button to push that magically finds all of our bugs for us. Verification, after all, accounts for roughly two-thirds of logic design effort. Without that button, we have to create reference models, focused tests, random stimuli, checkers, coverage monitors, regression suites, etc.

Of course, there is no big red button, and I’d be crazy to suggest that we could abandon all of that work altogether. But, at the same time, that’s not far from what Akos Hadnagy and I did, several years ago, in developing the WARP-V CPU generator.

I wrote WARP-V initially to explore code generation using the emerging Transaction-Level Verilog language. I brought the model to life with a simple test program that summed numbers from 1 to 10. Then, Akos put RISC-V configurations of WARP-V through the wringer, as a student in Google Summer of Code, using the open-source RISC-V Formal framework. By completing formal verification (which has now also been done independently by Axiomise using different tools and checkers), we felt no inclination to bother with any of the standard RISC-V tools and compliance tests.

Formal Verification Hurdles

While our formal-focused approach helped eliminate a considerable amount of work, in other ways it did add some effort, too. Of course it did. If formal verification were a panacea, everyone would be taking this approach, and while formal verification has been around for a long time, it still struggles to attain first-class status in the verification landscape. This has little to do with the core science and everything to do with usability.

The first big leap in usability for formal verification came with the provision of counterexample traces. These let you debug formal failures much like simulation failures, using a waveform viewer. This, however, is not enough to put formal verification on a level playing field with dynamic verification. For one thing, simulations can produce log files in addition to waveforms. These provide high-level context about simulations to help with debugging. For aggressive use of formal verification, getting big picture context is important. Here’s why:

Traditionally, focused testing plays a major role in stabilizing the model. The myriad basic bugs are identified by focused tests, which are written for a specific purpose in a very controlled context. You know what they are doing. You know what to look for. Formal verification, however, will identify a counterexample that could be doing absolutely anything (within your constraints). Fortunately, the trace will be short, but formal tools have a way of finding really gnarly corners you would never expect or never be able to hit in a controlled fashion. That’s what’s so great about formal!

So if we’re going to find a significant portion of our bugs using formal methods, we’d better make it easier to figure out what’s going on in the counterexamples. That’s where visualization comes in.

Streamlining Debugging with Visualization

WARP-V utilizes the Visual Debug framework, now freely available to open-source projects in the Makerchip.com IDE. Visual Debug (or VIZ) makes it easy to define simulation visualizations. These aid in the debugging process of any digital circuit developed using any hardware description language and any design environment that produces industry-standard (.vcd) trace files. You may have seen screenshots of visualizations similar to those of WARP-V in various of my posts about my RISC-V CPU design courses, in which hundreds of students have developed their own RISC-V CPUs.

Using Visual Debug for the first time is like turning the lights on in a room you didn’t realize was dark. Just as you wouldn’t walk into a dark room to find your car keys without turning on the lights, you shouldn’t start debugging without first enabling Visual Debug. Though it wasn’t the case at the start of WARP-V development, as you’ve undoubtedly guessed by now, VIZ now works for formal counterexamples as well as it does for simulation.

Implications of Easier Debugging

Let’s put these visualization benefits in the context of WARP-V’s design methodology. This means, I first get to talk about the benefits of TL-Verilog–my favorite topic. Utilizing TL-Verilog, WARP-V is able to support different pipeline depths and even different instruction set architectures from the same codebase. And it is able to do so in less code (and correspondingly fewer bugs) than a single RTL-based CPU core. Furthermore, transaction-level design greatly simplifies the task of creating test harnesses to connect any RISC-V hardware configuration to the RISC-V Formal checkers. As described in “Verifying RISC-V in One Page of Code!”, the reduction in modeling effort across four different CPU configurations was arguably a factor of 70x or more! (These benefits would apply to test harnesses for dynamic verification as well.)

In the face of these TL-Verilog benefits, the effort to debug formal verification failures became a significant portion of the remaining work, and Visual Debug would have streamlined this effort. More generally, being able to easily decipher formal counterexamples can be the boost in productivity that tips the scales for formal verification. This, in turn, makes our resulting hardware more robust and secure. And security is quite possibly the biggest challenge faced by design teams today.

Visual Debug in Action

I leave you with a screen-capture, narrated by yours truly, demonstrating debugging of a register bypass (aka register forwarding) bug in WARP-V.

Related Links: Makerchip.com, Visual Debug, WARP-V CPU generator, RISC-V Formal, RISC-V CPU design courses, “Verifying RISC-V in One Page of Code!”