https://github.com/kristerw/smtgcc
@kristerw Boolector (the predecessor) is really damn good for verifying that RISC-V soft-cores behave as expected. Unfortunately, I've found it difficult to build Bitwuzla on Windoze, so I've stuck w/ Boolector.
(Also I can't remember if it's faster or slower than Boolector on the RISC-V stuff. But hey, that's SMT solvers for you.)
@kristerw Boolector (the predecessor) is really damn good for verifying that RISC-V soft-cores behave as expected. Unfortunately, I've found it difficult to build Bitwuzla on Windoze, so I've stuck w/ Boolector.
(Also I can't remember if it's faster or slower than Boolector on the RISC-V stuff. But hey, that's SMT solvers for you.)
@kristerw Boolector (the predecessor) is really damn good for verifying that RISC-V soft-cores behave as expected. Unfortunately, I've found it difficult to build Bitwuzla on Windoze, so I've stuck w/ Boolector.
(Also I can't remember if it's faster or slower than Boolector on the RISC-V stuff. But hey, that's SMT solvers for you.)
@kristerw Boolector (the predecessor) is really damn good for verifying that RISC-V soft-cores behave as expected. Unfortunately, I've found it difficult to build Bitwuzla on Windoze, so I've stuck w/ Boolector.
(Also I can't remember if it's faster or slower than Boolector on the RISC-V stuff. But hey, that's SMT solvers for you.)