Formal Verification of a RISC-V Processor

Lana Perkins Lab Alumni

Michael Castiglia Undergraduate Student Researcher

Primary Research Question: Can Formal Verification Methods be applied to a unverified RISC-V processor to confirm its logical equivalence to one that is verified?

Objective:

This research project focuses on using Formal Verification, specifically Formal Equivalence Checking, to verify the equivalence(s) of two RISC-V processors. The goal is to compare the behavior of an already verified RISC-V processor with an unverified one using mathematical proofs, identifying, and addressing any discrepancies.

Key Objectives:

1. Formal Equivalence Checking: a. Implement Formal Equivalence Checking to compare the behavior of a verified RISC-V processor with an unverified one. b. Use mathematical proofs to verify the correctness of the unverified processor’s functionality. c. Document any differences in behavior between the two processors.
2. Knowledge Application: a. Apply Formal Verification methodology to find issues in the unverified processor’s design and functionality. b. Gain practical insights into the strengths and limitations of Formal Verification in RISC-V processor verification. c. Develop a systematic approach to address and correct identified discrepancies.
3. Educational Component: a. Provide undergraduate researchers with hands-on experience in Formal Verification techniques. b. Foster understanding of RISC-V architecture and the importance of formal methods for processor reliability. c. Enhance analytical and problem-solving skills through practical application.
4. Documentation and Reporting: a. Document the Formal Verification process, including methodology, tools used, and results. b. Generate reports outlining the processors’ behavior and a detailed analysis of any corrections made. c. Provide clear documentation for future research and industry applications.

Expected Outcomes:

The project aims to:

1. Identify and correct potential discrepancies in the unverified processor’s functionality.
2. Validate the Formal Verification methodology for RISC-V processors.
3. Create educational resources for undergraduate researchers in computer engineering and formal methods.

This research project, led by undergraduate researchers, seeks to contribute practical insights to the field of Formal Verification and provide a learning experience in RISC-V processor design and analysis.

Public Description

When a user buys a product, they expect that it will work how it’s supposed to. They don’t want to buy a device, provide some random sequence of inputs, and then have the device shut down forever. This type of edge-case behavior can be mitigated more emphasis on verification, a stage in development devoted to ensuring everything works as designed. The DRACO Lab is exploring a facet of this process, Formal Verification, by doing Formal Equivalence Checking on two RISC-V processors. By using an already verified processor, the team can test the unverified processors correct or incorrect behavior by mathematical proofs and compare their functionality for equivalence. The goal of this process will be to apply the Formal Verification methodology and use this knowledge to verify and correct any of the processor’s functionality.