Prove mode support

[coreyqh]

Hello,

Is riscv-formal intended to support unbounded model checks with the mode prove option in checks.cfg?

It is mentioned in the docs, but both nerv and picorv32 seem to fail the induction step when I add mode prove under [options]

Is this a bug? Or is unbounded model checking not supported?

Let me know, thanks!

[KrystalDelusion]

Looking at the cores/nerv/imemcheck.sby there is the following:

`define NERV_FAIRNESS  # Required to make k-induction work

This NERV_FAIRNESS define is in the checks.cfg for the liveness test which doesn't actually get run in the default configuration. For picorv32 the corresponding flag is PICORV32_FAIRNESS. Adding this flag to the main defines section for the checks.cfg isn't enough for all the checks to pass (e.g. reg), but it does make some pass (e.g. pc_fwd, at least in NERV).

It seems like not all checks are able to be used in prove mode, but unfortunately there is very little documentation about it so I don't know if for example the reg check used to pass induction but no longer does, or if it was never able to be used. And unfortunately because SBY returns a status of "unknown" when the basecase and induction differ in result it causes the makefile to fail instead of being able to run all the checks and report at the end. Lines 385 and 657 of genchecks.py have a expect pass,fail, if you change that to expect pass,fail,unknown then you should be able to keep the makefile happy and get all of the tests to run. Doing this for NERV shows that most do pass, unique fails, and causal/pc_bwd/reg fail return unknown.

[coreyqh]

Thank you for the response! I was able to recreate your changes and confirm that most checks pass induction.

I looked in the docs and I could not find anything linking the fairness conditions to k-induction, and the nerv and pico fairness code in the wrapper is a bit cryptic. Are you able to explain what the purpose of this code is and why it allows for k-induction to work? Is there any chance of getting the docs updated with instructions for prove mode?

Thanks again!

[KrystalDelusion]

Are you able to explain what the purpose of this code is and why it allows for k-induction to work?

There is a Simple and Oversimplified K-Induction Explanation in one of the appnotes you can take a look at. My understanding is that without the fairness guarantee it's possible for the system to stall indefinitely, meaning there exists a path which never reaches the success state and the proof fails. Note that it's the inputs to the core that need the fairness guarantees, if its possible for the core to stall indefinitely due to internal signals it should fail at least the liveness check.

Is there any chance of getting the docs updated with instructions for prove mode?

Yes, pending an investigation into whether the checks that are failing in NERV are because of a failure in NERV or the design of the checks. If you're willing/able to look into that it would be very helpful, otherwise it might be a couple months :)