NeoRV32 formal verification results

[mikaelsky]

Over the summer Skyworks has run an older version of the NeoRV32 core though RISCV-Formal. Beyond 1 bug (illegal instruction access fault), the core came back clean. See screen caps below.

Getting NeoRV32 through formal verification is quite cumbersome, hence why I haven't pushed the core changes needed for formal verification. Suffice to say the requirements are that the RVFI interface must be added to the core and the whole thing is required to be synthesizable. Meaning RVFI is sticky in the core.
Further formal verification using symbiyosys requires verilog as an input code base. Using GHDL to convert NeoRV32 to verilog, while feasible, is error prone as there are bugs in the GHDL->Verilog conversion. These require post processing of the resulting verilog code base to make it "sane".
To highlight the amount of wrapping required:

With that said here are the good results:
Restricted bounded model checks (we only check the NeoRV32 internal state is valid at the end of the formal check)

Full bounded model checks (the NeoRV32 internal state is check on all "clocks")

Note: the failing test case here is a bug in yosys that has been reported.
Note: the floating point instruction tests are Skyworks specific and not part of the official RISCV-formal suite.

For completeness we also run NeoRV32 through a commercial tool, in this case JasperGold. The results where:

The interpretation here is:

• Proven means an formal property has been proven for all time.
• CEX (Counter Example) means a property failed. These are aligned to challenges with the riscv formal properties, except for the illegal access.
• Undetermined means that a formal property could be proved as a bounded constraint but not unbounded/infinite.

As we are still on quite an old version of the core the applicability on the current RTL I will leave up to the reader.

[stnolting]

Wow, that's really impressive! Thanks for sharing this!

[...] an older version of the NeoRV32 core [...]

v1.9.3, right? Are you planning to update to a newer version?

Suffice to say the requirements are that the RVFI interface must be added to the core

That's still on my TODO list... At least we already have a simple trace port, but it doesn't provide nearly all the information required by RVFI. Anyway, I would of course like to have full support for RVFI + frameworkat some point... Maybe we should set up a few "help wanted" issues...

[...] there are bugs in the GHDL->Verilog conversion. These require post processing of the resulting verilog code base to make it "sane".

Do you have any further details? I think your findings could be very valuable for the further improvement of GHDL.

To highlight the amount of wrapping required:

That looks great! Did you integrate the RVFI directly into the core, or are you using VHDL's external names at the top level?

With that said here are the good results:

I'm definitely no expert when it comes to formal verification, but as far as I can tell, it looks pretty good! Thank you for publishing these results. I think this gives the project another little boost in quality. 😉

CEX (Counter Example) means a property failed. These are aligned to challenges with the riscv formal properties, except for the illegal access.

That's the bug you've reported in #1373, right?

[mikaelsky]

As you know formal verification of the neorv32 has been on both our lists for quite a while. This summer I had the opportunity to get a skilled intern to look at the task. So why not share the good results with you all :)

Its on my list to upgrade to a newer version. I've held of mostly because the older version we have is currently in silicon so any upgrade of the core for that project has big impact on the overall verification effort.

It was a bit easier for us to get to RVFI as we already had an RVVI interface setup. Beyond the interface there are a number of additional models that are required around the core. When I get to upgrading the core I can see what can be done to push up an example for formal verification.

For GHDL I believe we issued a bug report.. I think. In our case GHDL consistently removes 1 signal driver inside the core. The signal removed was always the same signal which is why we could script our way out of it.

For RVFI, as it has to be synthesizable we can't use anything by reference like we do for RVVI. A lot of the VHDL external name stuff/by reference etc are for test only per the standard.. I think.. I might be wrong?. This means we have to route signal up to the top from various sub-modules into the RVFI test framework.
Further as we have to pass the VHDL code through GHDL all port types, like records etc have to be unraveled as we are basically instantiating a verilog mapped netlist (GHDL output) into a verilog test harness where we repack them into usable structs for our verilog models. If we don't unravel all that stuff the names are assigned sorta randomly by GHDL.. and decoding those names are.. less than fun and they can change with code changes etc.
Basically its a big ole mess as everything going into yosys must be verilog. With JasperGold we can consume the core as straight up VHDL so simpler with the caveat that JasperGold is closed source and costly :)

The yosys results includes our fix to #1373 of where you already caught the main one which is that illegal access are allowed to execute. The fix in the latest version of the core is identical to our fix to the problem :)
I should have highlighted that. Without a fix #1373 also shows up with yosys. So Yosys is good enough to prove the NeoRV32 core using formal, with some caveats that are noted in the riscv-formal documentation.

One caveat here is that we are waiving the FSR write on illegal access from e.g. an FADD getting kicked off. I think this is a side effect of having the FSR inside the FPU without the ability to flag to the FPU that write backs should be blocked.
Do note here that riscv-formal does not include any coverage of floats. Nor does it really cover mult/div either. As a test we added a few float instructions to gain some insights into how we can add more instructions to riscv-formal.

The CEX is #1373 and bugs in our porting of riscv-formal to SVA properties syntax for JasperGold.

[stnolting]

[...] is currently in silicon.

Oh cool, now I'm curious. 😅 I guess you can't give any more details, right?

It was a bit easier for us to get to RVFI as we already had an RVVI interface setup. Beyond the interface there are a number of additional models that are required around the core. When I get to upgrading the core I can see what can be done to push up an example for formal verification.

That's a good point. I would like to extend the trace interface to support at least the minimum features of RVFI. Do you use the CSR signals? Could you perhaps give an overview of which signals from the spec you have used?

For GHDL I believe we issued a bug report..

That's great! 👍

For RVFI, as it has to be synthesizable we can't use anything by reference like we do for RVVI. A lot of the VHDL external name stuff/by reference etc are for test only per the standard.. I think.. I might be wrong?

Ah, I see. I'm not sure if synthesizers support VHDL external names at all, but they should be synthesizable.

This means we have to route signal up to the top from various sub-modules into the RVFI test framework.

That's why I would like to extend the trace port. Since it is already used by the processor's trace buffer, this would also ensure that the RVFI is synthesizable.

Further as we have to pass the VHDL code through GHDL all port types, like records etc have to be unraveled as we are basically instantiating a verilog mapped netlist (GHDL output) into a verilog test harness where we repack them into usable structs for our verilog models. If we don't unravel all that stuff the names are assigned sorta randomly by GHDL.. and decoding those names are.. less than fun and they can change with code changes etc.

For this, I always use a VHDL top wrapper that only has individual wires or vectors, but no structs/records.
(e.g. https://github.com/stnolting/neorv32/blob/main/rtl/system_integration/neorv32_vivado_ip.vhd)

One caveat here is that we are waiving the FSR write on illegal access from e.g. an FADD getting kicked off.

That should now be fixed with #1376 too.

[stnolting]

Btw, I am working on expanding the trace port so that it is compatible with the RISC-V Formal Interface (RVFI): -> #1385

RVVI looks a little different, but I think both interfaces contain the same information.