include module type of Hardcaml_verify_kernel.Nusmvtype property = Hardcaml_verify_kernel.Nusmv.property = | LTL of Hardcaml.Property.LTL.path| CTL of Hardcaml.Property.CTL.stateval sexp_of_property : property -> Sexplib0.Sexp.ttype t = Hardcaml_verify_kernel.Nusmv.tval sexp_of_t : t -> Sexplib0.Sexp.tval create :
?outputs:Hardcaml.Signal.t Base.list ->
name:Base.string ->
property Base.list ->
tcreate ?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.tReturn the circuit generated for the NuSMV model.
val write : Stdio.Out_channel.t -> t -> Base.unitWrite the NuSMV model to a file.
module Proof_result = Hardcaml_verify_kernel.Nusmv.Proof_resultmodule Output_parser = Hardcaml_verify_kernel.Nusmv.Output_parserval run : t -> Proof_result.t Base.listmodule Circuit_properties = Hardcaml_verify_kernel.Nusmv.Circuit_propertiesmodule With_interface = Hardcaml_verify_kernel.Nusmv.With_interfacemodule Counter_example_trace : sig ... end