Presentation
Securing Safe Customization of RISC-V Cores via Rigorous Sequential RTL Comparison
DescriptionThis paper presents an innovative approach to "no-harm" verification using Formal Sequential Equivalence Checking (FSEC) for the comprehensive comparison of original and customized designs, specifically targeting equivalence without the introduction of new instructions. The discussion delves into the challenges inherent in FSEC and proposes a set of customization rules designed to produce a new Register-Transfer Level (RTL) with minimal modifications. In instances where automatic proof strategies prove insufficient, the paper advocates for a manual, divide-and-conquer verification approach. Notably, it provides insights into the verification of entire design with a black-boxed execute stage. By showcasing the ongoing relevance of formal verification, this work underscores its effectiveness in identifying issues beyond the scope of contemporary verification methodologies, establishing its pivotal role in ensuring design integrity
Event Type
Front-End Design
TimeMonday, June 242:30pm - 2:45pm PDT
Location2010, 2nd Floor
Design
Engineering Tracks
Front-End Design