close By using this website, you agree to the use of cookies. Detailed information on the use of cookies on this website can be obtained on OneSpin's Privacy Policy. At this point you may also object to the use of cookies and adjust the browser settings accordingly.

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

More information…

the RISC-V Verification App is the industry’s first tool to address the needs of both core providers and core integrators. It leverages OneSpin’s advanced formal verification expertise for high-integrity processor applications.

»Download the data sheet…

OneSpin’s Operational SVA enables formal verification enthusiasts to develop high-level, non-overlapping assertions that capture end-to-end transactions and requirements in a concise, elegant way.

»Learn more…

The OneSpin 360 Design Verification (DV) product line leverages the most advanced, high-performance formal technology as the basis for a range of verification solutions, from automated design analysis to advanced property checking.

»Download the flyer…

OneSpin’s Quantify measures the quality of a formal verification test bench. It provides precise, actionable information on what parts of the design-under-test (DUT) are verified, and it highlights RTL code that could still hide bugs.

»Download the data sheet…

OneSpin’s Connectivity XL App is the industry’s first and only solution for the efficient specification and formal verification of huge numbers of deep connections in multi-billion-gate chips.

»Download the data sheet…

OneSpin’s VCI App enables users to export structural coverage results produced by OneSpin’s QuantifyTM in different database formats with a single command.

»Download the data sheet…

OneSpin 360 DV-Verify adds coverage-driven assertion-based verification (ABV) to the DVInspect platform.

»Download the data sheet…

In a systematic verification flow, requirements tracking and coverage play an indispensable role. Generally, this starts from requirements specification, where individual requirements are broken down into features, implementations, verification goals, and metrics.

»Download the data sheet…

Design verification has a lot in common with human hygiene practices. The goal of both activities is to remove all dirt, grime, and bugs through an active process of establishing good hygiene.

»Download the white paper…

Fault-tolerant hardware development is no longer a niche and presents new challenges. Many engineers face the daunting task of having to examine countless faulty variants of their design in order to integrate and verify multiple safety mechanisms within complex Systems-on-Chip (SoCs).

»Download the white paper…

Get in touch!

Learn more about RISC-V verification with OneSpin!

portrait of Sven Beyer

Sven Beyer, Product Manager Design Verification

» Contact