package hardcaml_verify

  1. Overview
  2. Docs
package hardcaml_verify
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Hardcaml_verify_kernel.SecSource

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.

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

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

Get the proposition for a single circuit output

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

Get the proposition for a the inputs to a register.

Sourceval 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

Sourceval 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.

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

Check circuit equivlance (all propositions included).

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct