package hardcaml_verify
Hardcaml Verification Tools
Install
Dune Dependency
Authors
Maintainers
Sources
hardcaml_verify-v0.15.0.tar.gz
sha256=a469d63c76bd86fbd04aa38d391dc736d4bc291ad5ffe0090b31cc4ae3ba6622
Description
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
README
"Hardcaml Verification Tools"
Verification support for Hardcaml.
Interface to SAT solvers for combinational logic problems.
Code generation for NuSMV for sequential model checking.
Dependencies (9)
-
re
>= "1.8.0" -
dune
>= "2.0.0" -
stdio
>= "v0.15" & < "v0.16" -
ppx_jane
>= "v0.15" & < "v0.16" -
ppx_deriving_hardcaml
>= "v0.15" & < "v0.16" -
hardcaml_waveterm
>= "v0.15" & < "v0.16" -
hardcaml
>= "v0.15" & < "v0.16" -
base
>= "v0.15" & < "v0.16" -
ocaml
>= "4.08.0"
Dev Dependencies
None
Used by
None
Conflicts
None
On This Page