package hardcaml_verify

  1. Overview
  2. Docs
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)

  1. re >= "1.8.0"
  2. dune >= "2.0.0"
  3. stdio >= "v0.16" & < "v0.17"
  4. ppx_jane >= "v0.16" & < "v0.17"
  5. ppx_deriving_hardcaml >= "v0.16" & < "v0.17"
  6. hardcaml_waveterm >= "v0.16" & < "v0.17"
  7. hardcaml >= "v0.16" & < "v0.17"
  8. base >= "v0.16" & < "v0.17"
  9. ocaml >= "4.14.0"

Dev Dependencies

None

Used by (1)

  1. hardcaml_of_verilog >= "v0.16.0"

Conflicts

None