OneSpin Processor Verification Solution

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.