hardcaml_verify v0.15.0 · OCaml Package

Sequential equivalence checking.

This module will take 2 circuits, and perform a SAT check on the combinational logic. Stateful logic must be the same between the 2 circuits - this is not a true equivalence check, but much simpler to implement.

It will return Unsat if the two circuits are equivalent, or Sat otherwise.

It may be useful when optimising the combinational logic of a circuit, or when porting code to hardcaml with Hardcaml_of_verilog.

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.

val equivalent : 
  Proposition.t Base.list ->
  Equivalence_result.t Base.Or_error.t

Check equivalence of the given proposition.

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

Check circuit equivlance (all propositions included).

package hardcaml_verify