RISC-V Summit

Pre-silicon verification of processors is a challenging, time-consuming task. IP providers offering proprietary ISA cores leverage decades of effort and state-of-the-art EDA tools. RISC-V cores for commercial applications must achieve the same level of quality while facing the additional challenge of their own custom instructions of registers.

This demo session presents a fully-fledged environment for the formal verification signoff of RISC-V cores. Its main inputs are the target RTL core and a description of the custom extensions. It produces a set of assertions capturing that the RTL faithfully implements the chosen ISA with its custom extensions and nothing else. These assertions are exhaustively proven on the RTL.