VC Formal Enabled QED Proofs on a RISC-V Core

The Synopsys VC Formal group have a real talent for finding industry speakers to talk on illuminating outside-the-box-topics in formal verification. Not too long ago I covered an Intel talk of this kind. A recent webinar highlighted use of formal methods used together with a cool technique I have covered elsewhere called Quick Error Detection (QED). This for me is a good example of what really makes formal so fascinating – not so much the engines behind the scenes as the intellectual freedom they enable in solving a problem. Frederik Möllerström Lauridsen, a verification engineer at SyoSil, shared his experience using this method for Synopsys VC Formal for proofs on a RISC-V core.

The verification objective

Considering only the base ISA plus possible custom extensions, Frederick wanted a generic setup for RISC-V cores, in part through how they define their SVA assertions. He doesn’t go into detail in his talk, but I believe this means assertions which reference only the start and end of the pipeline, not the internals or the number of cycles required to complete. His goal is to detect both single instruction bugs and multi-instruction bugs. Single instruction bugs are relatively easy to find, but multi-instruction bugs are harder to uncover thanks to context dependent stalls without which for example register read/write conflicts might occur.

Single-instruction bugs (eg does an ADD really add) are not context dependent so can be checked by running the instruction through an otherwise empty pipeline. But multi-instruction bugs are context specific. How can you verify against all legal contexts? To see how, first you need to understand a little about QED.

QED

Quick Error Detection (QED) is a method first invented for post-silicon validation. There you start with machine-level code and regularly duplicate instructions reading and writing through a parallel set of registers / memory locations. You then compare original values with duplicated values; a difference signals an error. Similar techniques are migrating to pre-silicon verification, for an interesting reason. The intent is to regularly compare consistency between parallel implementations, with the promise that root cause errors may be caught long before being flagged by some more functionally meaningful assertion we might think to write. (Incidentally, this technique is not limited to formal verification. It is just as valuable in dynamic verification.)

Combining formal methods and QED

To apply QED you need a reference design and a design under test (DUT). Here the reference design is a single-instruction pipeline test, eg pushing an ADD instruction through an otherwise empty pipeline. In parallel the DUT will push though the same instruction, but how do you define context as an arbitrary selection of possible surrounding instructions? For this Frederick used a variant on QED called C-S²QED.

Without dropping too much into the technical weeds, S² means “symbolic state”, which allows for arbitrary instructions going through the pipeline, constrained so that the first instruction entering the pipeline is the same as the instruction entering the reference pipeline. The “symbolic” part of this is key. It is not necessary to define what other instructions are going through. These are only constrained to be legal instructions. Since we are applying formal methods, all possibilities will be considered together in proofs. The other neat trick that Frederick applied was first to demonstrate that all instructions would pass through the pipeline within at most a fixed number of cycles, providing a limit for bounded proofs.

Now using the QED methodology, comparing the reference design and DUT through formal methods provides proof that there are no multi-instruction bugs in the pipeline implementation, or it provides a counterexample. Pretty cool! Frederick did acknowledge that they had not extended their method to any of the standard RISC-V ISA extensions (M, A, F, etc) though you could use VC Formal DPV for the M extension and no doubt clever folks can come up with creative possibilities for other extensions.

Very cool stuff. You can register to watch the webinar HERE.

For enthusiasts of this line of thinking check out a blog I wrote back in 2018, on the Wolper method to verify the correctness of data transport logic in network switches or on-chip interconnects or memory subsystems. I love the way formal has been applied so creatively in QED and in Wolper. There must be more opportunities like this 😊