Effective Pre-Silicon Verification of Processor Cores by Breaking the Bounds of Symbolic Quick Error Detection

Abstract

This paper introduces a novel pre-silicon verification approach that extends Symbolic Quick Error Detection (SQED) by incorporating symbolic starting states, effectively breaking the bounds of conventional verification. This methodology allows Bounded Model Checking (BMC) to select arbitrary initial conditions, restricted only by defined constraints that prevent false positives from unreachable states. The new technique successfully discovered previously unknown logic bugs and hardware Trojans in open-source RISC-V processor cores, demonstrating superior performance in detecting defects requiring long instruction traces.

Report

Key Highlights

• Novel Verification Technique: Introduces an extension to Symbolic Quick Error Detection (SQED) for effective pre-silicon verification of processor cores.
• Symbolic Starting States: The core innovation is enabling symbolic starting states, allowing the verification tool to arbitrarily select initial conditions for trace generation.
• Bug Discovery: Successfully discovered previously unknown logic bugs in existing open-source RISC-V processor cores.
• Superior Performance: Outperforms existing verification methods in detecting complex bugs that require long instruction traces.
• Hardware Trojan Detection: Demonstrated capability in identifying hardware Trojans (unauthorized modifications) within the design.

Technical Details

• Methodology Foundation: The approach relies on Symbolic Quick Error Detection (SQED), which combines bounded model checking (BMC) with Quick Error Detection (QED) tests.
• SQED Extension: The symbolic starting states enable BMC to initiate verification from a much larger, symbolically defined set of processor states, rather than a fixed reset state.
• False Positive Avoidance: To ensure practical relevance and prevent traces starting in states that violate the Instruction Set Architecture (ISA), the authors defined constraints and reasonable assumptions about system behavior.
• Target Architecture: The approach was empirically validated by discovering bugs within open-source RISC-V processor core designs.
• Test Generation: QED tests are used to generate short instruction sequences (traces) designed to trigger potential logic bugs.

Implications

• Enhanced RISC-V Reliability: By proving its effectiveness on open-source RISC-V cores, this method significantly increases the confidence in the reliability and correctness of the rapidly evolving RISC-V ecosystem.
• Pre-Silicon Cost Savings: Effective pre-silicon verification drastically reduces the risk, time, and immense cost associated with discovering and debugging logic bugs post-silicon.
• Security Validation: The explicit focus and success in detecting hardware Trojans are critical for security assurance, especially for processors using open-source IP or those manufactured in untrusted foundries.
• Verification Completeness: The ability to find bugs that manifest over long traces addresses a major blind spot in verification, where traditional methods often struggle due to the state space explosion associated with long instruction sequences.