package hardcaml_verify

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Parameters
Signature

hardcaml_verify
- Library hardcaml_verify
  - Hardcaml_verify
    
    Basic_gates
    
    Cnf
    
    Comb_gates
    
    Dimacs
    
    Is_one_hot
    
    Label
    
    Sat
    
    Sec
    
    Solver
    
    Tseitin
    
    Nusmv
    
    Proof_result
    
    Output_parser
    
    Circuit_properties
    
    With_interface
    
    Counter_example_trace
- Library hardcaml_verify.kernel
  - Hardcaml_verify_kernel
    
    Basic_gates
    
    Uid
    
    Cnf
    
    Literal
    
    Disjunction
    
    Conjunction
    
    Model
    
    Model_with_bits
    
    Model_with_vectors
    
    Comb_gates
    
    TypedMath
    
    Unsigned
    
    Signed
    
    Uop
    
    Sop
    
    Dimacs
    
    Is_one_hot
    
    Make
    
    Label
    
    Uid
    
    Nusmv
    
    Counter_example_trace
    
    Proof_result
    
    Output_parser
    
    Circuit_properties
    
    With_interface
    
    Sat
    
    Sec
    
    Instantiation_ports_match
    
    Proposition
    
    Equivalence_result
    
    Solver
    
    Tseitin
    
    S
    
    Make
- Sources
  - hardcaml_verify
    
    hardcaml_verify.ml
    
    hardcaml_verify__.ml
    
    nusmv.ml
  - hardcaml_verify.kernel
    
    basic_gates.ml
    
    cnf.ml
    
    comb_gates.ml
    
    config.ml
    
    dimacs.ml
    
    hardcaml_verify_kernel.ml
    
    hardcaml_verify_kernel__.ml
    
    is_one_hot.ml
    
    label.ml
    
    nusmv.ml
    
    sat.ml
    
    sec.ml
    
    solver.ml
    
    tseitin.ml
    
    uid.ml

Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module `Nusmv.With_interface`Source

Parameters

module I : Hardcaml.Interface.S

module O : Hardcaml.Interface.S

Signature

type model := t

Sourcetype t

type ltl := Hardcaml.Property.LTL.path

type ctl := Hardcaml.Property.CTL.state

Sourceval create : name:Base.string -> Hardcaml.Interface.Create_fn(I)(O).t -> t

Sourceval ltl : t -> (ltl Base.array I.t, ltl Base.array O.t) Circuit_properties.t

Sourceval ctl : t -> (ctl Base.array I.t, ctl Base.array O.t) Circuit_properties.t

Sourceval create_specification : t -> property Base.list -> model

package hardcaml_verify

Module Nusmv.With_interfaceSource

Parameters

Signature

Module `Nusmv.With_interface`Source