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
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
|
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
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
Comment by
Felix Yan (felixonmars) - Thursday,
11 August 2022, 08:33 GMT
Bump? This is effectively a three-line change.
mathsat-5 is also in the AUR. I'll be adding cvc4, yices, and z3.