July 23, 2025
LUBIS EDA was able to find some undetected bugs that led to RTL changes in a pipelined RISC-V core, adapted and used by a company developing NAND Flash Memory controller. Some of them were detected within the first day.
These bugs had escaped or weren’t triggered by traditional simulation-based approaches, which is highlighting the importance of formal methods in verifying processor designs — especially as RISC-V adoption grows in critical applications.
The Formal Verification approach: property-based assertion checks using our in-house SystemVerilog Assertions (SVA) targeting the full R32I instruction set architecture (ISA). The effort revealed both functional violations and corner-case bugs.
However, it was found that the core doesn’t raise an exception and doesn’t update the PC with the MEPC’s value but increments the PC as if it was not an unknown opcode.
Figure 1: Unknown opcode handling bug
Figure 2: JALR misalignment exception bug
The results demonstrate how formal verification can uncover deep corner-case failures — even in mature RTL code — that would otherwise remain hidden, due to its deterministic approach providing a clear yes/no answer.
Are you building your own RISC-V core and want to make sure it’s not happening in yours? Feel free to reach out
As a leading formal verification service provider, LUBIS EDA has collected the pain points of manual formal verification through extensive hands-on project work. LUBIS EDA’s consulting services fit seamlessly into already existing verification flows, streamlining the process by introducing unique solutions that significantly enhance efficiency and automate most tasks involved.
For those interested in running similar verification efforts or formal sign-off flows on their own RISC-V designs, LUBIS EDA provides tailored consulting and assertion IP.
Link to Press Release
News
In an industry where missed corner cases can delay products by weeks or even months, LUBIS EDA recently demonstrated how formal verification can catch critical design bugs early — in some cases, within hours of the verification start.LUBIS EDA was able to find some undetected bugs that led to RTL changes in a pipelined RISC-V core, adapted and used by a company developing NAND Flash Memory controller. Some of them were detected within the first day.
These bugs had escaped or weren’t triggered by traditional simulation-based approaches, which is highlighting the importance of formal methods in verifying processor designs — especially as RISC-V adoption grows in critical applications.
The Formal Verification approach: property-based assertion checks using our in-house SystemVerilog Assertions (SVA) targeting the full R32I instruction set architecture (ISA). The effort revealed both functional violations and corner-case bugs.
Example Bug Fundings
Several bugs in different instructions were found that would have been able to cause major issues during the runtime of the core. Here are two specific bug examples:Bug 1 – Wrong exception handling
A bug was found in handling unknown opcodes. Per RISC-V specifications: once an unknown opcode is fetched, an exception should be raised, and the PC value should be updated with the MEPC’s value.However, it was found that the core doesn’t raise an exception and doesn’t update the PC with the MEPC’s value but increments the PC as if it was not an unknown opcode.
Figure 1: Unknown opcode handling bug
Bug 2 – Wrong instruction implementation
A bug was found in the JALR instruction where the design wrongly writes the fetching address of the JALR instruction to the register file in case of a misalignment exception. In the counterexample the design fetches the JALR instruction from address 0x84 where it calculates the target address. In case of a misalignment, a misalignment exception should be generated and the JALR should not take effect. The design was correctly generating a misalignment exception, but it was wrongly writing the fetching PC value to the destination register.
Figure 2: JALR misalignment exception bug
Why bother?
These bugs were just two of a set of bugs that have been identified in this RISC-V design. While some might be called “subtle”, others could lead to unpredictable system behaviour up to a deadlock. Especially worrying in safety- or security-critical applications.The results demonstrate how formal verification can uncover deep corner-case failures — even in mature RTL code — that would otherwise remain hidden, due to its deterministic approach providing a clear yes/no answer.
Are you building your own RISC-V core and want to make sure it’s not happening in yours? Feel free to reach out
About LUBIS EDA
With years of experience in formal verification, a standardized formal sign-off methodology, and a proven track record, LUBIS EDA specializes in supporting the design of bug-free chips — ensuring tape-out deadlines are met without delays from late bug discoveries.As a leading formal verification service provider, LUBIS EDA has collected the pain points of manual formal verification through extensive hands-on project work. LUBIS EDA’s consulting services fit seamlessly into already existing verification flows, streamlining the process by introducing unique solutions that significantly enhance efficiency and automate most tasks involved.
For those interested in running similar verification efforts or formal sign-off flows on their own RISC-V designs, LUBIS EDA provides tailored consulting and assertion IP.
Link to Press Release