embedded world 2020
Nuremberg, Germany | February 25 - 27, 2020
The embedded world Exhibition & Conference is the world's leading meeting place for the embedded community. OneSpin will co-exhibit at booth 4-560 in partnership with eVision Systems, so please stop by the booth and have a chat with us!
TUESDAY February 25, 03:00 PM - 03:30 PM
Verification of RISC-V SoC Designs Using Formal Methods
Sven Beyer, OneSpin Solutions
Verification of system-on-chip (SoC) designs containing RISC-V processor cores is challenging. The cores can come from many sources, so they must be vetted for compliance to the instruction set architecture (ISA) specification. Beyond the ISA, optional features, custom extensions, and microarchitectural implementation must also be verified. The SoC team must guarantee proper integration of the cores and the entire chip must be screened for design issues that could hinder proper operation. Further, both cores and SoC must be checked thoroughly to ensure that no hardware Trojans or security risks are present. Only formal methods can provide full proofs for all these verification tasks and build confidence in the integrity of the design. This paper describes a formal-based methodology to meet these challenges, summarizes previous work on multiple RISC-V cores and SoCs, and presents previously unpublished results.