package hardcaml_verify

You can search for identifiers within the package.

in-package search v0.2.0

Hardcaml Verification Tools

Install

Dune Dependency

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

Authors

J

Jane Street Group, LLC

Maintainers

J

Jane Street developers

Sources

v0.17.0.tar.gz

sha256=a09a904776ad848f685afb4ebe85e0d449acb81f6f2425fccc52a3c5b76be629

doc/hardcaml_verify.kernel/Hardcaml_verify_kernel/Nusmv/index.html

Module `Hardcaml_verify_kernel.Nusmv`Source

Sourcetype property =

| LTL of Hardcaml.Property.LTL.path
| CTL of Hardcaml.Property.CTL.state

Sourceval sexp_of_property : property -> Sexplib0.Sexp.t

Sourcetype t

Sourceval sexp_of_t : t -> Sexplib0.Sexp.t

Source

val create : 
  ?outputs:Hardcaml.Signal.t Base.list ->
  name:Base.string ->
  property Base.list ->
  t

create ?outputs ~name properties creates a NuSMV model with the provided name.

properties is a list of LTL and/or CTL formula that should be satified by the circuit. During construction all atomic_propositions (which are the signals in the design used to build the temporal formula) are created as outputs. They are given the prefix "__ap_" which should not otherwise be used to name signals.

The important part of the circuit is traced back from the atomic_propositions. However, it is possible to include the complete circuit if required by passing outputs.

Sourceval circuit : t -> Hardcaml.Circuit.t

Return the circuit generated for the NuSMV model.

Sourceval write : Stdio.Out_channel.t -> t -> Base.unit

Write the NuSMV model to a file.

Sourcemodule Counter_example_trace : sig ... end

Sourcemodule Proof_result : sig ... end

Sourcemodule Output_parser : sig ... end

Sourceval run : t -> Proof_result.t Base.list

Sourcemodule Circuit_properties : sig ... end