package hardcaml_verify

  1. Overview
  2. Docs
Hardcaml Verification Tools

Install

Dune Dependency

github.com Readme MIT License Edit opam file Versions (2)

Authors

  1. J
    Jane Street Group, LLC

Maintainers

  1. J
    Jane Street developers

Sources

hardcaml_verify-v0.15.0.tar.gz
sha256=a469d63c76bd86fbd04aa38d391dc736d4bc291ad5ffe0090b31cc4ae3ba6622

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: 21 Mar 2022

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.15" & < "v0.16"
  4. ppx_jane >= "v0.15" & < "v0.16"
  5. ppx_deriving_hardcaml >= "v0.15" & < "v0.16"
  6. hardcaml_waveterm >= "v0.15" & < "v0.16"
  7. hardcaml >= "v0.15" & < "v0.16"
  8. base >= "v0.15" & < "v0.16"
  9. ocaml >= "4.08.0"

Dev Dependencies

None

Used by

None

Conflicts

None