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!

[SeddonShen]

Will this backend be merged into the mainline as soon as possible? I can't wait to use it!

[georgerennie]

Sorry I have been busy and haven't had much time to return to this.

We discussed this in one of the YosysHQ Dev JF meetings, and the main blocker was that we don't think your license terms are enforceable. I believe that GPLv3 does not allow you to add terms preventing use on commercial designs. In particular GPLv3 contains the following, which suggests an end user is allowed to simply ignore your restriction on commercial use:

All other non-permissive additional terms are considered “further restrictions” within the meaning of section 10. If the Program as you received it, or any part of it, contains a notice stating that it is governed by this License along with a term that is a further restriction, you may remove that term.

Additionally it states the following. I do not believe that the output (whether the system is safe or not) constitutes a covered work, similar to how a program compiled by GCC would not be a covered work.

A “covered work” means either the unmodified Program or a work based on the Program.

This License explicitly affirms your unlimited permission to run the unmodified Program. The output from running a covered work is covered by this License only if the output, given its content, constitutes a covered work

@jix and @widlarizer may have more on this also as they looked into it.

In terms of moving forwards, I think to merge support we would like rIC3 to have a license that is consistent/enforceable. My personal preference would be for this to be GPLv3 without the restriction on use on commercial designs. I think this restriction is not well defined or enforceable as the solver result is not a work in itself and blanket bans on commercial use limit open source freedoms. For example, if a user writes an open source verilog library with an open source license, by verifying it with rIC3 they are now no longer compliant with the open source license even if they themselves don't use it commercially as the rIC3 terms prevent any downstream users using it commercially.

If you do retain a restriction (without GPLv3), the suggestion in the Dev JF was that we gate rIC3 support behind an explicit makefile flag, so users can only opt into it explicitly as using it poisons licenses.

Hopefully we can work this out because it would be great to add support! Other than these license issues I have run this patch and am happy to approve it.

[gipsyh]

Hello! I have removed the restriction on commercial use and released rIC3 version 1.3.5 with the updated licensing terms. Additionally, I have updated the latest commit in the PR to reflect this change.

Thank you!

[georgerennie]

Thanks a lot for your contribution!