hardcaml_verify

Hardcaml Verification Tools
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.

Install
Published
21 Mar 2022
Authors
Maintainers
Sources
hardcaml_verify-v0.15.0.tar.gz
sha256=a469d63c76bd86fbd04aa38d391dc736d4bc291ad5ffe0090b31cc4ae3ba6622
Dependencies
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"
Reverse Dependencies