OneSpin Launches First Formal RISC-V Integrity Verification Solution
February 21, 2019
Completeness of ISA Specification Ensures Absence of Functional Errors, Hardware Trojans, Security Vulnerabilities
OneSpin® Solutions, provider of innovative verification solutions for highly reliable, digital integrated circuits (ICs), today unleashed its RISC-V Integrity Verification Solution for development and assessment of RISC-V cores, leveraging its advanced formal verification expertise for automotive and other high-integrity processor applications.
The RISC-V Integrity Verification Solution, based on the RISC-V instruction set architecture (ISA) formalized in a set of SystemVerilog Assertions (SVA), is delivered as a series of formal applications (Apps) and integrated into an exhaustive verification framework. The Solution verifies compliance for the open standard RISC-V ISA is met, critical for both IP core suppliers and their customers. It also verifies that cores do not contain hardware Trojans or other unintended functionality to ensure trust and security.
“Even though past efforts have failed to achieve 100% proof, verification of an instruction set architecture’s conformance is a natural fit for formal technology,” remarks Sven Beyer, OneSpin’s product manager for design verification. “Our RISC-V integrity Verification Solution converges for all properties on real-world implementations, a valuable resource to the many users trying to meet this processor standard.”
OneSpin’s RISC-V Integrity Verification Solution
OneSpin validated its Solution using leading RISC-V core implementations. This approach brings value to the ecosystem with exhaustive formal analysis of implementations and a formal, lean bug-hunting environment to quickly uncover corner-case bugs. It adds a formal bug absence core assessment environment for unbounded proofs and systematic discovery of all hidden instructions or unintended side effects of instructions. Detection of hardware Trojans for trust assurance and detection of security vulnerabilities is part of the solution as well.
Benefits of using formal verification such as OneSpin’s are numerous. It can verify compliance to the open standard RISC-V ISA, something simulation-based approaches cannot, especially useful for a RISC-V IP supplier’s commercial success. A high degree of verification is essential when facing competition from older, well -established ISAs. The supplier must ensure the IP does everything it's supposed to do and does not do anything it's not supposed to do for trust and security.
System-on-chip (SoC) designers can license a RISC-V core confident that it complies with the ISA specification, while IP vendors can support their own ecosystems and ensure that ecosystem partners also comply. Further, SoC designers can add custom features to the RISC-V ISA to support their specific applications. OneSpin’s Solution ensures nothing is broken as features are added and is flexible enough to verify new functionality.
The RISC-V Integrity Verification Solution includes privileged ISA, Control and Status Registers (CSRs), an exception mechanism and other extensions. Its verification framework splits the specification side from mapping to implementation to enable full SVA reuse. Mapping to the target implementation is eased through a OneSpin-provided guiding procedure.
OneSpin will highlight the RISC-V Integrity Verification Solution during DVCon U.S. in Booth #301 February 25-27 at the DoubleTree Hotel in San Jose, Calif., and at embedded world Conference February 26-28 in Nuremberg, Germany. OneSpin will be located in eVision System's embedded world booth (Hall 4, Booth 4-560).
OneSpin will exhibit at the Government Microcircuit Applications & Critical Technology Conference (GOMAC) (Booth #610) March 25-28, in Albuquerque, New Mexico. OneSpin and Edaptive Computing will present “Complete Formal Verification of RISC-V Processor IPs for Trojan-Free Trusted ICs” during Session 41 Thursday.
Availability and Pricing
The RISC-V Integrity Verification Solution is shipping now. Pricing is available upon request. To learn more, visit https://www.onespin.com/solutions/risc-v/
OneSpin has direct sales channels in the United States, Europe and throughout Asia, backed by a variety of customer service and support options including on-site training, hotline support and consulting services.
About OneSpin Solutions
OneSpin Solutions has emerged as a leader in verification through a range of advanced electronic design automation (EDA) solutions for digital integrated circuits. Headquartered in Munich, Germany, OneSpin enables users to address design challenges in areas where reliability really counts: safety-critical verification, SystemC/C++ high-level synthesis (HLS) code analysis and FPGA equivalence checking. OneSpin’s advanced formal verification platform and dedication to getting it right the first time have fueled dramatic growth over the past five years as the company forges partnerships with leading electronics suppliers to pursue design perfection. OneSpin: Making Electronics Reliable.