lowRISC C.I.C. powers-up influential technology toolbox

It has added formal verification to the toolbox of open source design verification techniques used to ensure the commercial level quality of the Microsoft-created CHERIoT-Ibex core – the processor at the heart of the UKRI-funded Sonata™ platform.

And a key Oxbridge alliance is at the heart of the initiative.

Prof. Tom Melham and Louis-Emile Ploix of the University of Oxford, and Alasdair Armstrong of the University of Cambridge, have created an extensive formal verification framework to establish observational equivalence, using unbounded proofs, between the hardware and the RISC-V International Sail specification of instruction behaviour. This greatly strengthens confidence in the design’s conformance to the specification.

The verification uses the Cadence Jasper™ tool, along with new Sail support to automatically build a SystemVerilog reference model from the specification.

They collaborated with Microsoft to upstream this into the open source CHERIoT-Ibex repository.

CHERIoT-Ibex is Microsoft’s open-source extension of lowRISC’s Ibex®, a 32-bit RISC-V processor. CHERIoT provides fine-grained memory protection for embedded systems, which deterministically mitigates over two thirds of memory vulnerabilities and enables efficient compartmentalisation.

This new formal verification framework and proof developed by the Universities of Oxford and Cambridge and lowRISC takes the formal specification for CHERIoT – written in Sail – and checks that for any stream of instructions the CHERIoT-Ibex implementation performs the same memory operations.

Besides the work on CHERIoT-Ibex, lowRISC has also published an adaptation of this proof for regular Ibex (which of course also has extensive conventional DV), the main microprocessor core used in the OpenTitan® root of trust.

Dr. Gavin Ferris, CEO of lowRISC, said: “We’re thrilled to see the achievement of this milestone, demonstrating that well managed open-source silicon designs can not just match the DV quality of commercial IP, in some cases they’re beginning to lead the field.

“The successful formal verification of CHERIoT-Ibex exemplifies our Silicon Commons approach, bringing the best of industry, academia and the open source community together through collaborative engineering — and moving the game forward for everyone.

“Now, not only can companies bring products to market cheaper and faster by leveraging open-source silicon designs, they can do so with the strongest possible assurance that specification fidelity has been maintained.”

lowRISC was founded in 2014 at the University of Cambridge Department of Computer Science and Technology.