package hardcaml_verify
Hardcaml Verification Tools
Install
Dune Dependency
Authors
Maintainers
Sources
v0.17.0.tar.gz
sha256=a09a904776ad848f685afb4ebe85e0d449acb81f6f2425fccc52a3c5b76be629
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: 26 May 2024
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
>= "3.11.0" -
stdio
>= "v0.17" & < "v0.18" -
ppx_jane
>= "v0.17" & < "v0.18" -
ppx_hardcaml
>= "v0.17" & < "v0.18" -
hardcaml_waveterm
>= "v0.17" & < "v0.18" -
hardcaml
>= "v0.17" & < "v0.18" -
base
>= "v0.17" & < "v0.18" -
ocaml
>= "5.1.0"
Dev Dependencies
None
Used by (1)
-
hardcaml_of_verilog
>= "v0.17.0"
Conflicts
None
On This Page