Boosting the Bounds of Symbolic QED for Effective Pre-Silicon Verification of Processor Cores

Abstract

This work introduces a novel pre-silicon verification approach that systematically leverages Symbolic Quick Error Detection (SQED) combined with symbolic starting states to drastically improve the detection of deep logic bugs and Hardware Trojans. The method overcomes the limitations of traditional Bounded Model Checking (BMC) by finding flaws requiring long activation sequences without needing skilled manual assertion guidance. Applied to various RISC-V cores, this technique quickly detected 100% of known commercial bugs and identified new flaws, significantly boosting verification efficiency and hardware trust.

Report

Key Highlights

• Novel Verification Method: The research systematically combines Symbolic Quick Error Detection (SQED) with Symbolic starting states to enhance pre-silicon verification capabilities.
• High Detection Rate: Demonstrated 100% detection of hundreds of logic bug and Hardware Trojan scenarios derived from commercial chips and research literature on open-source RISC-V cores.
• Overcoming BMC Limitations: The technique is highly effective against "difficult" logic bugs and Trojans requiring long activation sequences, where conventional Bounded Model Checking (BMC) fails.
• Automation: The method eliminates the need for skilled manual guidance, assertion writing, or complex debugging of spurious counter-examples.
• Speed: Bug detection times were exceptionally quick, ranging from less than 5 minutes for in-order scalar cores to under 2.5 hours for complex out-of-order superscalar cores.

Technical Details

• Core Technology: The system is built upon Symbolic Quick Error Detection (SQED), a bug detection and localization technique primarily using Bounded Model Checking (BMC).
• Key Innovation: The bounds of BMC are "boosted" by the introduction of Symbolic starting states, allowing the verification tool to efficiently check much deeper activation sequences.
• Bug Resilience Tested: The method successfully handled "extremal" bugs—randomly generated flaws requiring approximately 100,000 activation instructions—with a 97.9% detection rate.
• Target Architecture: The approach was validated using open-source RISC-V processor cores, covering both simpler in-order scalar designs and highly complex out-of-order superscalar designs.
• Discovery of Unknown Bugs: The technique demonstrated its utility by quickly (around 1 minute) detecting several previously unknown bugs in the evaluated open-source RISC-V designs.

Implications

• Enhanced Hardware Trust: By offering a highly effective and automated way to find subtle logic bugs and malicious implants (Hardware Trojans), this methodology significantly improves trust in pre-silicon designs, which is critical for security-sensitive applications.
• Boosting RISC-V Quality: As the RISC-V ecosystem expands, the need for scalable and automated formal verification tools increases. This technique provides a powerful, fast, and accessible method for verifying the functional correctness and security of diverse open-source RISC-V implementations.
• Reducing Verification Cost: The elimination of the need for specialized manual guidance (e.g., writing design-specific assertions or complex testbenches) slashes the labor and expertise required for formal verification, making advanced verification techniques more practical for smaller design teams or open-source projects.
• Advancement in Formal Methods: The successful application of Symbolic QED combined with symbolic starting states pushes the practical boundaries of what Bounded Model Checking can achieve in complex, deep-state processor verification.