include module type of Hardcaml_verify_kernel.Nusmv
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
module Proof_result : sig ... end
module Output_parser : sig ... end
module Circuit_properties : sig ... end
module Counter_example_trace : sig ... end