hardcaml_verifyversion Documentation on ocaml.org
Hardcaml Verification Tools
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.
| Author | Jane Street Group, LLC |
|---|---|
| License | MIT |
| Published | |
| Homepage | https://github.com/janestreet/hardcaml_verify |
| Issue Tracker | https://github.com/janestreet/hardcaml_verify/issues |
| Maintainer | Jane Street developers |
| Available | arch != "arm32" & arch != "x86_32" |
| Dependencies |
|
| Source [http] | https://github.com/janestreet/hardcaml_verify/archive/refs/tags/v0.17.0.tar.gz sha256=a09a904776ad848f685afb4ebe85e0d449acb81f6f2425fccc52a3c5b76be629 |
| Edit | https://github.com/ocaml/opam-repository/tree/master/packages/hardcaml_verify/hardcaml_verify.v0.17.0/opam |
Required by
- hardcaml_of_verilog>=v0.17.0
