package hardcaml_verify
Hardcaml Verification Tools
Install
Dune Dependency
Authors
Maintainers
Sources
hardcaml_verify-v0.16.0.tar.gz
sha256=b475dc8e540d9855b438309de3cf1984b28d29e7cd8a4d2b76d58a68894a8749
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: 14 Jun 2023
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.16" & < "v0.17" -
ppx_jane
>= "v0.16" & < "v0.17" -
ppx_deriving_hardcaml
>= "v0.16" & < "v0.17" -
hardcaml_waveterm
>= "v0.16" & < "v0.17" -
hardcaml
>= "v0.16" & < "v0.17" -
base
>= "v0.16" & < "v0.17" -
ocaml
>= "4.14.0"
Dev Dependencies
None
Used by (1)
-
hardcaml_of_verilog
= "v0.16.0"
Conflicts
None
On This Page