FS#62064 - [yosys] Add optional packages for SMT solvers

Attached to Project: Community Packages
Opened by Sean Anderson (Forty-Bot) - Tuesday, 19 March 2019, 01:23 GMT
Last edited by Felix Yan (felixonmars) - Thursday, 11 August 2022, 09:02 GMT
Task Type Feature Request
Category Packages
Status Closed
Assigned To Felix Yan (felixonmars)
Architecture All
Severity Very Low
Priority Normal
Reported Version
Due in Version Undecided
Due Date Undecided
Percent Complete 100%
Votes 2
Private No

Details

Yosys now has support for formal verification, and has several supported backends:

$ yosys-smtbmc

yosys-smtbmc [options] <yosys_smt2_output>
...
-s <solver>
set SMT solver: z3, yices, boolector, cvc4, mathsat, dummy
default: yices
...

The default solver "yices" is not in any repository (but is in the AUR as "yices" and "yices-bin"). "boolector" is also only available from the AUR. I suggest adding the following optional dependencies:

z3
cvc4
mathsat-5
This task depends upon

Closed by  Felix Yan (felixonmars)
Thursday, 11 August 2022, 09:02 GMT
Reason for closing:  Implemented
Additional comments about closing:  0.12-7
Comment by Sean Anderson (Forty-Bot) - Wednesday, 03 August 2022, 22:29 GMT
Bump? This is effectively a three-line change.
Comment by Felix Yan (felixonmars) - Thursday, 11 August 2022, 08:33 GMT
mathsat-5 is also in the AUR. I'll be adding cvc4, yices, and z3.

Loading...