Module `Hardcaml_verify_kernel.Sec`Source

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.

Sourcemodule Instantiation_ports_match : sig ... end

Control comparison of instantiation inputs and outputs.

Sourcetype t

Sourceval sexp_of_t : t -> Sexplib0.Sexp.t

Sourcemodule Proposition : sig ... end

A proposition derived from the circuits being compared.

Sourcemodule Equivalence_result : sig ... end

Result of a proposition check.

Source

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.

Sourceval circuit_outputs_proposition : t -> Proposition.t

All circuit outputs match

Source

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

Get the proposition for a single circuit output

Source

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

Get the proposition for a the inputs to a register.

Source

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

Source

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

Get the proposition for all inputs to an instantiation.

Source

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

Check equivalence of the given proposition.

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

Check circuit equivlance (all propositions included).

Install

Dune Dependency

Authors

Maintainers

Sources

doc/hardcaml_verify.kernel/Hardcaml_verify_kernel/Sec/index.html

Module `Hardcaml_verify_kernel.Sec`Source

package hardcaml_verify

Install

Dune Dependency

Authors

Maintainers

Sources

doc/hardcaml_verify.kernel/Hardcaml_verify_kernel/Sec/index.html

Module Hardcaml_verify_kernel.SecSource

Module `Hardcaml_verify_kernel.Sec`Source