Tools for verifying properties of Hardcaml circuits.
Combinational circuits can be converted to 'conjunctive normal form' for input into SAT solvers via DIMAC files. Support for a few opensource solvers is integrated - minisat, picosat, Z3 - just ensure they are in your PATH.
Circuits can also be converted to NuSMV format for advanced bounded and unbounded model checking tasks.
Published: 21 Mar 2022
"Hardcaml Verification Tools"
Verification support for Hardcaml.
Interface to SAT solvers for combinational logic problems.
Code generation for NuSMV for sequential model checking.