Quick and exhaustive verification and proof of compliance to instruction set architecture (ISA) with no gaps or inconsistencies

RISC-V is an open-source hardware instruction set architecture (ISA) widely supported by IP, EDA, and software suppliers. Providers of RISC-V IP cores face a high bar for verification and compliance to the published ISA. Meeting these challenges is essential to successfully compete with older, well established ISAs with many silicon implementations and design-ins. In addition, core providers need to ensure that their designs meet the trust and security expectations of their customers, including the absence of hardware Trojans or other unintended functionality that could enable adversary attacks. 

The OneSpin Processor Verification Solution is the industry’s first commercial tool suite to address the needs of both core providers and core integrators. It leverages OneSpin’s advanced formal verification expertise for automotive and other high-integrity processor applications to exhaustively verify the implementation with minimal set up and runtime. The core of the solution is the formalization of the RISC-V ISA as a set of SystemVerilog Assertions (SVA) using the unique OneSpin Operational Assertion approach. Operational SVA enables high-level, non-overlapping assertions that capture end-to-end transactions and requirements in a concise, elegant way:

• Translate functional requirements in a formal and simulation executable format
• Capture entire circuit transactions in a concise and elegant way, similar to timing diagrams
• Achieve 100% functional coverage with high-level and easy-to-review assertions
• Adopt a consistent assertion style that is applicable to a wide range of applications and able to deliver optimal performances for both simulators and formal tools
• Cleanly separate implementation-specific supporting verification code from reusable specification-level code
• Further leverage the assertion set using OneSpin’s GapFreeVerification™ for automatic detection of specification omissions and errors, holes in the verification plan, and unverified RTL functions

This methodology is ideal for capturing the key rules for the RISC-V ISA. Each operation is captured in a single Operational Assertion. These assertions capture the high-level operational view, and map to sequential or pipelined implementation, out-of-order execution, and other possible options in the RTL core. 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’s formal engines detect any inconsistencies between an RTL core implementation and the ISA as captured by the assertions. The application of GapFreeVerification™ goes beyond proving equivalence between the RTL and the set of Operational SVA. It also verifies that the set of assertions is sufficient to cover the RISC-V core design and ensures that there is no unverified RTL functionality. Any extra functionality in the design, including hardware Trojans, is detected and reported as a violation of the ISA. This includes the systematic discovery of any hidden instructions or unintended side effects of instructions. This enables both core providers and customers to have the highest confidence in the trust and security of RISC-V implementations.

OneSpin’s Processor Verification Solution ensures that an IP core implementation does everything it's supposed to do and does not do anything it's not supposed to do. 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.

Check out our library of RISC-V content

• RISC-V Verification Q & A
  »Check out the Videos
• Formal Verification of RISC-V Cores
  »Watch the Video
• RISC-V Summit 2019 Videos
  »Watch the Videos
• “A Holistic View Of RISC-V Verification”
  by Nicolae Tusinschi, Semiconductor Engineering, 7 August 2019
  »https://semiengineering.com/a-holistic-view-of-risc-v-verification/
• “Assuring the Integrity of RISC-V Cores and SoCs”
  white paper, OneSpin Solutions, July 2019
  »Download White Paper
• “Enabling The RISC-V Ecosystem”
  by Nicolae Tusinschi, Semiconductor Engineering, 27 June 2019
  »https://semiengineering.com/enabling-the-risc-v-ecosystem/
• “Lösung zum Sicherstellen der Integrität von RISC-V-Kernen”
  by Sven Beyer and Tom Anderson, Elektronik Industrie, 19 June 2019
  »https://www.all-electronics.de/loesung-zum-sicherstellen-der-integritaet-von-risc-v-kernen/
• “Formalizing the RISC-V ISA in a set of SystemVerilog assertions that can be proven
  to be complete, consistent, and free from gaps”
  by Sergio Marchese, Verification Futures, 13 June 2019
  »https://www.testandverification.com/conferences/verification-futures/vf2019/
• “Formal Verification of PULPino and other RISC-V SoCs”
  by Nicolae Tusinschi and Sven Beyer, RISC-V Workshop Zurich, 12 June 2019
  »Download pdf
• “Unbounded Formal Verification of RISC-V CSRs with Interval Property Checking”
  by Nicolae Tusinschi and Sven Beyer, RISC-V Workshop, Zurich, 11 June 2019
• “Unbounded Formal Verification of RISC‑V CSRs with Interval Property Checking”
  by Nicolae Tusinschi and Sven Beyer, Design Automation Conference (DAC), Las Vegas, 2 June 2019
• “Verification Challenges for RISC-V Adoption”
  by Tom Anderson, GSA Forum, 2 May 2019
  »https://www.gsaglobal.org/forums/1386/verification-challenges-for-risc-v-adoption/
• “In the middle of every difficulty lies opportunity.” – Albert Einstein
• “Complete Formal Verification of RISC-V Processor IPs for Trojan-Free Trusted ICs”
  by Paul McHale (Edaptive) and David Landoll, GOMACTech Conference, Albuquerque, 28 March 2019
• “Ensure Compliance and Trust for RISC-V Cores and SoCs with Complete Formal Verification”
  by Sasa Stamenkovic, Verification 3.0 Innovation Summit, Santa Clara, 19 March 2019
  »https://www.youtube.com/watch?v=bC2-11q9QS4
• "Unbounded Formal Verification of RISC-V CSRs with Interval Property Checking”
  by Nicolae Tusinschi, RISC-V Workshop, Taiwan, 12 March 2019
  »Download pdf
• “Formal Verification Of RISC-V Cores”
  by Sven Beyer, Semiconductor Engineering, 28 February 2019
  »https://semiengineering.com/formal-verification-of-risc-v-cores/