hardcaml_verify

Hardcaml Verification Tools
IN THIS PACKAGE
module Instantiation_ports_match : sig ... end

Control comparison of instantiation inputs and outputs.

type t
val sexp_of_t : t -> Sexplib0.Sexp.t
module Proposition : sig ... end

A proposition derived from the circuits being compared.

module Equivalence_result : sig ... end

Result of a proposition check.

val create : ?instantiation_ports_match:Instantiation_ports_match.t -> Hardcaml.Circuit.t -> Hardcaml.Circuit.t -> t Base.Or_error.t

Construct the logic for comparing two circuits via their outputs, registers and instantiations.

instantiation_ports_match allows the left (first passed) circuit to contain instantiations which have a subset of the ports on instantiations in the right (second passed) circuit. This comes up when comparing with a circuit that was converted from verilog and has floating ports.

val circuit_outputs_proposition : t -> Proposition.t

All circuit outputs match

val find_circuit_output_port_proposition : t -> port_name:Base.string -> Proposition.t Base.option

Get the proposition for a single circuit output

val find_register_inputs_proposition : t -> name:Base.string -> Proposition.t Base.option

Get the proposition for a the inputs to a register.

val find_instantiation_input_port_proposition : t -> instantiation_name:Base.string -> port_name:Base.string -> Proposition.t Base.option

Get the proposition for a single input port of an instantiation

val find_instantiation_inputs_proposition : t -> name:Base.string -> Proposition.t Base.option

Get the proposition for all inputs to an instantiation.

Check equivalence of the given proposition.

val circuits_equivalent : t -> Equivalence_result.t Base.Or_error.t

Check circuit equivlance (all propositions included).