Feature: Verification
Figure 1: Verifying RISC-V correctness
Functional correctness When it comes to verification, simulation is often the first thing that comes to mind. However, formal proofs are much more powerful than simply passing a traditional compliance test suite running in simulation. Simulation, no matter how extensive, can exercise only
such as ensuring the cores do what they are supposed to but also don’t do what they are not supposed to. One of the biggest challenges of verifying RISC-V cores is
the many options allowed by this highly configurable ISA; user extensions are allowed into the architecture, including custom instructions. Any verification solution must be flexible enough to expand to verify such extensions whilst also checking that no extension has violated any aspect of the baseline ISA. In addition, verification must include the core’s microarchitecture. RISC-V was developed to map onto a wide range of implementations, including different chip technologies, a wide range of PPA tradeoffs, deep processor pipelines and out-of-order execution of instructions. Te verification approach must be general enough to span all these variations; see Figure 1.
Good design hygiene Verification begins with automatic code inspection applicable to the RISC-V cores, the SoCs that contain them and any register transfer level (RTL) design code. Tis process eliminates many classes of common coding and design errors prior to functional verification and logic synthesis, but may take some time. Using the right automated solution can speed up this code inspection process and debug, making it easy to fix any violations discovered. Ideally, three perspectives should be considered: • Structural analysis that focuses on syntactic and semantic analysis of source code;
• Safety checks to perform exhaustive verification of the absence of common sequential design operation issues;
• Activation checks to prove that specific design functions can be executed and are not blocked due to unreachable code.
an infinitesimal portion of possible design behaviours. Even the most carefully crafted compliance suite leaves gaps in design coverage. There are countless cases where specific operand values or corner-case conditions are untested, which could trigger hidden design bugs. Arithmetic operations are especially prone to this problem. A single mistyped array index in an RTL description can yield a design where unexpected and non-intuitive operands produce wrong output. The very nature of simulation, as well as acceleration and emulation, makes it impossible to try every possible case. Formal tools do not iterate through test cases – they mathematically analyse a design in its entirety. A formal methodology that uses operational SystemVerilog Assertions (SVA) enables high-level, non-overlapping assertions that capture end-to-end transactions and requirements in a concise way: • Capture functional requirements in a formal and simulation executable format;
• Capture entire circuit transactions in a concise way, similar to timing diagrams;
• Achieve 100% functional coverage with high-level, easy- to-review assertions;
• Adopt a consistent assertion style that’s applicable to a wide range of applications and can deliver optimal performances for both simulators and formal tools;
• Cleanly separate implementation-specific supporting verification code from reusable specification-level code. Each instruction in the RISC-V ISA 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. A solution like the RISC-V Verification App from OneSpin 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 re-use. Regardless of the approach used, it should be flexible enough to ensure that nothing is broken if custom extensions are added, and powerful enough to verify the new functionality. The Operational Assertions can be used for automatic
detection of specification omissions and errors, holes in the verification plan and unverified RTL functions. Verification must be performed to confirm that the set of assertions is sufficient to cover the RISC-V core design, and to ensure there’s no unverified RTL functionality.
www.electronicsworld.co.uk September/October 2020 45
Page 1 |
Page 2 |
Page 3 |
Page 4 |
Page 5 |
Page 6 |
Page 7 |
Page 8 |
Page 9 |
Page 10 |
Page 11 |
Page 12 |
Page 13 |
Page 14 |
Page 15 |
Page 16 |
Page 17 |
Page 18 |
Page 19 |
Page 20 |
Page 21 |
Page 22 |
Page 23 |
Page 24 |
Page 25 |
Page 26 |
Page 27 |
Page 28 |
Page 29 |
Page 30 |
Page 31 |
Page 32 |
Page 33 |
Page 34 |
Page 35 |
Page 36 |
Page 37 |
Page 38 |
Page 39 |
Page 40 |
Page 41 |
Page 42 |
Page 43 |
Page 44 |
Page 45 |
Page 46 |
Page 47 |
Page 48 |
Page 49 |
Page 50 |
Page 51 |
Page 52 |
Page 53 |
Page 54 |
Page 55 |
Page 56 |
Page 57 |
Page 58 |
Page 59 |
Page 60 |
Page 61 |
Page 62 |
Page 63 |
Page 64 |
Page 65 |
Page 66 |
Page 67 |
Page 68
