Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

RTL Code Coverage Hole in cv32e40p_EX_stage module line 396 for FPU configuration #1018

Open
YoannPruvost opened this issue Jul 2, 2024 · 0 comments
Labels
Component:RTL For issues in the RTL (e.g. for files in the rtl directory) WAIVED:CV32E40P Issue does not impact a major release of CV32E40P and is waived

Comments

@YoannPruvost
Copy link
Contributor

Component

Component:RTL

Issue Description

One of the possible combination in the if statement line 396 of cv32e40p_EX_stage was not covered during all the simulation non-regressions.

After analysis we suspected that this scenario was in fact unreachable.
Siemens Questa Static formal tool was used to prove that this scenario was unreachable. For this scenario a dedicated assertion was written, named assert_unreachable_ex_396.

All information necessary to reproduce and analyze our work with formal can be found in the ReadMe in the cv32e40p/scripts/formal folder

As it was too late to implement a fix in the RTL due to long RISC-V ISA Formal Verification runs and requiring to update all waivers files as well, it has been decided to waive this scenario hole in v2.

387-396
396

@YoannPruvost YoannPruvost added Component:RTL For issues in the RTL (e.g. for files in the rtl directory) WAIVED:CV32E40P Issue does not impact a major release of CV32E40P and is waived labels Jul 2, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Component:RTL For issues in the RTL (e.g. for files in the rtl directory) WAIVED:CV32E40P Issue does not impact a major release of CV32E40P and is waived
Projects
None yet
Development

No branches or pull requests

1 participant