hardcaml_verifyversion
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
