package hardcaml_verify

  1. Overview
  2. Docs
package hardcaml_verify
Legend:
Library
Module
Module type
Parameter
Class
Class type
val sexp_of_property : property -> Sexplib0.Sexp.t
type t
val sexp_of_t : t -> Sexplib0.Sexp.t
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.

val circuit : t -> Hardcaml.Circuit.t

Return the circuit generated for the NuSMV model.

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

Write the NuSMV model to a file.

module Counter_example_trace : sig ... end
module Proof_result : sig ... end
module Output_parser : sig ... end
module Circuit_properties : sig ... end