Hardcaml_verify_kernel.SecSequential 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 ... endControl comparison of instantiation inputs and outputs.
val sexp_of_t : t -> Sexplib0.Sexp.tmodule Proposition : sig ... endA proposition derived from the circuits being compared.
module Equivalence_result : sig ... endResult of a proposition check.
val create :
?instantiation_ports_match:Instantiation_ports_match.t ->
Hardcaml.Circuit.t ->
Hardcaml.Circuit.t ->
t Base.Or_error.tConstruct 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.tAll circuit outputs match
val find_circuit_output_port_proposition :
t ->
port_name:Base.string ->
Proposition.t Base.optionGet the proposition for a single circuit output
val find_register_inputs_proposition :
t ->
name:Base.string ->
Proposition.t Base.optionGet 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.optionGet the proposition for a single input port of an instantiation
val find_instantiation_inputs_proposition :
t ->
name:Base.string ->
Proposition.t Base.optionGet the proposition for all inputs to an instantiation.
val equivalent :
Proposition.t Base.list ->
Equivalence_result.t Base.Or_error.tCheck equivalence of the given proposition.
val circuits_equivalent : t -> Equivalence_result.t Base.Or_error.tCheck circuit equivlance (all propositions included).