日本語

RISC-V Formal Verification IP

Overview

Why formal?

Modern processors implement numerous optimizations for power, performance, and area. Optimizations such as pipelining, interlocking, and data forwarding introduce numerous data dependencies and hazards causing processors to deadlock or produce incorrect results. The number of instruction combinations, together with instruction interleaving and multiple register files and operands make it impossible for any simulation-based verification to be exhaustive.

Challenges with formal

Formal verification produces exhaustive proof of correctness and finds corner-case bugs in design implementations. The challenges with formal verification, however, are:

    • Proof convergence is not guaranteed
    • No consistency of formal coverage models across different formal verification tools
    • No consistency between formal coverage models and simulation

Automated formal verification of RISC-V processors

The formalISA® app is a verification IP that addresses all these challenges successfully using formal methods. Built on top of the first-generation ISA formal verification proof kit from Axiomise, the formalISA® app is powered by a clean graphical-user-interface that allows the end-user to push a few buttons to obtain formal verification results on a RISC-V core of their choice, using a commercial formal verification tool of their choice.

The push-button ‘ Prove’ & ‘Cover’ solution eliminates the need to:

    • Write a single test case
    • Write complex test sequences
    • Write scoreboard or checkers
    • Write constraints
    • Randomize stimulus

Key Features of formalISA

Architectural Compliance

    • Establish ISA compliance via mathematical proofs for RISC-V processors

Exhaustive Proofs

    • Builds mathematical proofs of bug absence for architectural and micro-architectural checks and covers for RISC-V processors

Bug Hunting

    • Finds bugs, including corner-case bugs in processor implementation for 32-bit and 64-bit processors

Automation

    • Easy-to-setup and use
    • Push-button
    • GUI based
    • Vendor-neutral – use any formal verification tool of your choice
    • Visualize instruction-set behaviour using the scenario coverage solution

Micro-architecture independent

    • In-order and out-of-order cores
    • App tested on in-order cores as well as out-of-order cores
    • Support ready for RV32IMCZb*, and RV64IMCZb* instruction set
    • Predictable & Scalable run times

Debug

    • Intelligent debug via i-RADAR saves time in debugging and handover to designers

Coverage

    • Scenario coverage is generated automatically
    • Scheduler and Reporter for formal (SURF) provides all the essential summary in a dashboard

 

formalISA Results

Have More Questions?

Why do you need formal methods for RISC-V?

What is the coverage model for formal verification?

How do you avoid over-constraining?

What does debug look like with formal verification?

 How do you sign-off with formal?

Check out Axiomise Formal Verification Vodcast

We have deployed our formalISA app in the field since last four years and found numerous bugs in previously verified processors as well as exhaustively proving bug absence. For details of our technology,  and the results, head to the RISC-V studio. This will show you the background technology.

RISC-V Studio

To see formalISA in action, head straight to the formalISA studio. Here you can see how the app is orchestrated to find bugs, and establish proofs. You will also see our cutting-edge intelligent debugger i-RADAR®, SURF, and ISA coverage analyzer® solution using scenario coverage.

formalISA Studio
RISC-V is a registered trademark of the RISC-V International.
Formal Proof Kit is a registered trademark of Axiomise Limited.
formalISA, i-RADAR, and ISA Coverage Analyzer are registered trademarks of Axiomise Limited.