Support rIC3 model checker as backend

[gipsyh]

Support rIC3 as backend
https://github.com/gipsyh/rIC3

rIC3 achieved excellent performance in this year’s Hardware Model Checking Competition https://hwmcc.github.io/2024/

[georgerennie]

Other than the comments on documentation this PR seems fine, but I am currently unable to actually build rIC3 as the build commands for satift-kissat and satif-cadical try to mount a temp directory, which at least on my machine requires superuser privileges. Is there a way to get around this?

One other question - the readme says that rIC3 cannot be used for commercial purposes. Given the GPL license I take this to mean it cannot be modified/redistributed for commercial purposes, but can be used in its unmodified form to verify commercial designs? If this is not the case and this is forbidden we should have a note about this.

[georgerennie]

Oh also as the test failures highlight if we want rIC3 to be a target for some of the demos we need to add it to oss-cad-suite. For now it might be easier to leave it out of the demos and add it subsequently.

[gipsyh]

I fixed rIC3 so that it no longer needs to be mounted to a temporary directory, in its latest version 1.2.3.

I also fixed the 4 ^s in install.rst

[gipsyh]

It cannot verify commercial designs in its unmodified form without proper copyright. However, there’s no need for a note, as rIC3 requires manual installation, and this PR only provides an interface for rIC3 within sby.

One other question - the readme says that rIC3 cannot be used for commercial purposes. Given the GPL license I take this to mean it cannot be modified/redistributed for commercial purposes, but can be used in its unmodified form to verify commercial designs? If this is not the case and this is forbidden we should have a note about this.

[georgerennie]

Thanks for addressing those points, I appreciate your help!

However, there’s no need for a note, as rIC3 requires manual installation, and this PR only provides an interface for rIC3 within sby.

Thanks for clarifying that. I think we should definitely still include a note as all other backends for SBY can be used on commercial designs and we want to make it really clear for anyone installing SBY dependencies.

Other issues I see at the moment:

• We should specify the minimum rIC3 version needed in the install guide too
• rIC3 currently doesn't support multiple properties at once, but SBY happily creates designs with these. We could hack around this in SBY (there is a similar hack for pono in the btor backend) but it would be much nicer to do this directly in rIC3 (for now you can probably just take the disjunction of the bad properties)
• As the tests run in CI they would need rIC3 in oss-cad-suite which it isn't yet so I think for now we should not include it in the up_down_counter example
• You currently run rIC3 with -v0, which means if for some reason rIC3 has an internal error (e.g. I found this when trying to run it with a multiple property environment), this doesn't get reported back to the user. It would probably be better if we have some verbosity on so the user gets some output.

[gipsyh]

We should specify the minimum rIC3 version needed in the install guide too

Sure, I’ve updated it accordingly.

rIC3 currently doesn't support multiple properties at once, but SBY happily creates designs with these. We could hack around this in SBY (there is a similar hack for pono in the btor backend) but it would be much nicer to do this directly in rIC3 (for now you can probably just take the disjunction of the bad properties)

rIC3 now supports multiple properties in the latest version (v1.3.0).

As the tests run in CI they would need rIC3 in oss-cad-suite which it isn't yet so I think for now we should not include it in

I’ve fixed that.

You currently run rIC3 with -v0, which means if for some reason rIC3 has an internal error (e.g. I found this when trying to run it with a multiple property environment), this doesn't get reported back to the user. It would probably be better if we have some verbosity on so the user gets some output.

I’ve fixed that.

Thank you!