Virtual pi network

bindings/mnt/pyfiction/include/pyfiction/pybind11_mkdoc_docstrings.hpp

@@ -3761,6 +3761,20 @@ Parameter ``neutral_defect_spacing_overwrite``:
     A pair of uint16_t values representing the number of horizontal
     and vertical SiDBs affected by the given defect type.)doc";
 
+static const char *__doc_fiction_delete_virtual_pis =
+R"doc(Deletes virtual primary inputs from a network. This can mainly be used
+for equivalence checking. If the network does not have any virtual PIs
+stored, the network is returned.
+
+Template parameter ``Ntk``:
+    The type of network.
+
+Parameter ``ntk``:
+    The input network.
+
+Returns:
+    The resulting network after virtual primary inputs are deleted.)doc";
+
 static const char *__doc_fiction_dependent_cell_mode = R"doc(An enumeration of modes for the dependent cell.)doc";
 
 static const char *__doc_fiction_dependent_cell_mode_FIXED =
@@ -4583,6 +4597,16 @@ Parameter ``bdl_iterator``:
 
 static const char *__doc_fiction_detail_critical_temperature_impl_stats = R"doc(Statistics.)doc";
 
+static const char *__doc_fiction_detail_delete_virtual_pis_impl = R"doc()doc";
+
+static const char *__doc_fiction_detail_delete_virtual_pis_impl_delete_virtual_pis_impl = R"doc()doc";
+
+static const char *__doc_fiction_detail_delete_virtual_pis_impl_ntk = R"doc()doc";
+
+static const char *__doc_fiction_detail_delete_virtual_pis_impl_ntk_topo = R"doc()doc";
+
+static const char *__doc_fiction_detail_delete_virtual_pis_impl_run = R"doc()doc";
+
 static const char *__doc_fiction_detail_delete_wires =
 R"doc(This function deletes wires from the provided
 `wiring_reduction_layout` based on the specified coordinates and
@@ -12405,6 +12429,8 @@ static const char *__doc_fiction_has_foreach_incoming_clocked_zone = R"doc()doc"
 
 static const char *__doc_fiction_has_foreach_outgoing_clocked_zone = R"doc()doc";
 
+static const char *__doc_fiction_has_foreach_real_pi = R"doc()doc";
+
 static const char *__doc_fiction_has_foreach_sidb_defect = R"doc()doc";
 
 static const char *__doc_fiction_has_foreach_tile = R"doc()doc";
@@ -12417,6 +12443,8 @@ static const char *__doc_fiction_has_get_gate_ports = R"doc()doc";
 
 static const char *__doc_fiction_has_get_layout_name = R"doc()doc";
 
+static const char *__doc_fiction_has_get_real_pi = R"doc()doc";
+
 static const char *__doc_fiction_has_get_sidb_defect = R"doc()doc";
 
 static const char *__doc_fiction_has_high_degree_fanin_nodes =
@@ -12501,6 +12529,10 @@ static const char *__doc_fiction_has_is_outgoing_clocked = R"doc()doc";
 
 static const char *__doc_fiction_has_is_po = R"doc()doc";
 
+static const char *__doc_fiction_has_is_real_pi = R"doc()doc";
+
+static const char *__doc_fiction_has_is_virtual_pi = R"doc()doc";
+
 static const char *__doc_fiction_has_is_wire_tile = R"doc()doc";
 
 static const char *__doc_fiction_has_is_xnor = R"doc()doc";
@@ -12513,6 +12545,10 @@ static const char *__doc_fiction_has_north_east = R"doc()doc";
 
 static const char *__doc_fiction_has_north_west = R"doc()doc";
 
+static const char *__doc_fiction_has_num_real_pis = R"doc()doc";
+
+static const char *__doc_fiction_has_num_virtual_pis = R"doc()doc";
+
 static const char *__doc_fiction_has_ordinal_operations = R"doc()doc";
 
 static const char *__doc_fiction_has_post_layout_optimization = R"doc()doc";
@@ -18405,6 +18441,169 @@ static const char *__doc_fiction_vertical_shift_cartesian =
 R"doc(\verbatim +-------+ | | | +-------+ | | | +-------+ | | | +-------+
 \endverbatim)doc";
 
+static const char *__doc_fiction_virtual_pi_network = R"doc()doc";
+
+static const char *__doc_fiction_virtual_pi_network_clone = R"doc(Clones the virtual_pi_network object.)doc";
+
+static const char *__doc_fiction_virtual_pi_network_create_virtual_pi =
+R"doc(Create a virtual PI, which is a mapping to a real PI.
+
+This function adds a PI to the parent network, but marks it as virtual
+and stores a mapping to a real PI.
+
+Parameter ``real_pi``:
+    The node representing the real PI in the network.
+
+Returns:
+    The signal of the newly created virtual PI.)doc";
+
+static const char *__doc_fiction_virtual_pi_network_foreach_real_ci =
+R"doc(Iterates over the virtual CIs of the circuit and applies a given
+function.
+
+Template parameter ``Fn``:
+    The type of the function to be applied.
+
+Parameter ``fn``:
+    The function to be applied.)doc";
+
+static const char *__doc_fiction_virtual_pi_network_foreach_real_pi =
+R"doc(Iterates over the real PIs of the circuit and applies a given
+function.
+
+Template parameter ``Fn``:
+    The type of the function to be applied.
+
+Parameter ``fn``:
+    The function to be applied.)doc";
+
+static const char *__doc_fiction_virtual_pi_network_foreach_virtual_ci =
+R"doc(Iterates over the virtual CIs of the circuit and applies a given
+function.
+
+Template parameter ``Fn``:
+    The type of the function to be applied.
+
+Parameter ``fn``:
+    The function to be applied.)doc";
+
+static const char *__doc_fiction_virtual_pi_network_foreach_virtual_pi =
+R"doc(Iterates over the virtual PIs of the circuit and applies a given
+function.
+
+Template parameter ``Fn``:
+    The type of the function to be applied.
+
+Parameter ``fn``:
+    The function to be applied.)doc";
+
+static const char *__doc_fiction_virtual_pi_network_get_real_pi =
+R"doc(Get the real PI associated with a virtual PI node.
+
+Parameter ``v_pi``:
+    The virtual pi node to retrieve the real pi for.
+
+Returns:
+    The real pi associated with the virtual pi node.)doc";
+
+static const char *__doc_fiction_virtual_pi_network_is_real_ci =
+R"doc(Check if a given node is a real CI in the virtual_pi_network.
+
+Parameter ``n``:
+    The node to check.
+
+Returns:
+    True if the node is a real CI, false otherwise.)doc";
+
+static const char *__doc_fiction_virtual_pi_network_is_real_pi =
+R"doc(Check if a given node is a real PI. Real PIs are created with
+create_pi().
+
+Parameter ``n``:
+    The node to check.
+
+Returns:
+    True if the node is a real PI, false otherwise.)doc";
+
+static const char *__doc_fiction_virtual_pi_network_is_virtual_ci =
+R"doc(Check if a given node is a virtual CI in the virtual_pi_network.
+
+Parameter ``n``:
+    The node to check.
+
+Returns:
+    True if the node is a virtual CI, false otherwise.)doc";
+
+static const char *__doc_fiction_virtual_pi_network_is_virtual_pi =
+R"doc(Check if a given node is a virtual PI. Virtual PIs are created with
+create_virtual_pi().
+
+Parameter ``n``:
+    The node to check.
+
+Returns:
+    True if the node is a virtual PI, false otherwise.)doc";
+
+static const char *__doc_fiction_virtual_pi_network_num_real_cis =
+R"doc(Get the number of real CIs in the virtual_pi_network.
+
+Returns:
+    The number of real CIs as a uint32_t.)doc";
+
+static const char *__doc_fiction_virtual_pi_network_num_real_pis =
+R"doc(Get the number of real PIs in the virtual_pi_network.
+
+Returns:
+    The number of real PIs as a uint32_t.)doc";
+
+static const char *__doc_fiction_virtual_pi_network_num_virtual_cis =
+R"doc(Get the number of virtual CIs in the virtual_pi_network.
+
+Returns:
+    The number of virtual CIs as a uint32_t.)doc";
+
+static const char *__doc_fiction_virtual_pi_network_num_virtual_pis =
+R"doc(Get the number of virtual PIs in the virtual_pi_network.
+
+Returns:
+    The number of virtual PIs as a uint32_t.)doc";
+
+static const char *__doc_fiction_virtual_pi_network_real_size =
+R"doc(Calculate the real size of the virtual_pi_network.
+
+The real size of the network is considered the size without virtual
+PIs.
+
+Returns:
+    The real size of the virtual_pi_network as a uint32_t.)doc";
+
+static const char *__doc_fiction_virtual_pi_network_v_storage = R"doc(Shared pointer of the virtual PI storage.)doc";
+
+static const char *__doc_fiction_virtual_pi_network_virtual_pi_network =
+R"doc(Default constructor for the `virtual_pi_network` class. Initializes
+`v_storage` as a shared pointer.)doc";
+
+static const char *__doc_fiction_virtual_pi_network_virtual_pi_network_2 =
+R"doc(Constructor for the `virtual_pi_network` class that takes a network
+and a shared pointer to a `virtual_storage` object. This is used for
+cloning.
+
+Template parameter ``Ntk``:
+    Network type.
+
+Parameter ``ntk``:
+    Input network.
+
+Parameter ``s``:
+    Shared pointer to the `virtual_storage` object to be used by this
+    `virtual_pi_network`.)doc";
+
+static const char *__doc_fiction_virtual_pi_network_virtual_storage = R"doc()doc";
+
+static const char *__doc_fiction_virtual_pi_network_virtual_storage_map_virtual_to_real_pi = R"doc(Map from virtual_pis to real_pis.)doc";
+
+static const char *__doc_fiction_virtual_pi_network_virtual_storage_virtual_inputs = R"doc(Vector storing virtual_inputs.)doc";
+
 static const char *__doc_fiction_volume =
 R"doc(Computes the volume of a given coordinate assuming its origin is (0,
 0, 0). Calculates :math:`(|x| + 1) \cdot (|y| + 1) \cdot (|z| + 1)` by

docs/networks/virtual_pi_network.rst

@@ -0,0 +1,20 @@
+Technology Network
+==================
+
+A logic network type that extends any ``mockturtle`` logic network. It enables copies of PIs, called virtual PIs.
+Virtual PIs are created by passing an existing ``real_pi`` to the ``create_virtual_pi`` function. This function
+calls the ``create_pi`` function of the extended network and stores the newly created ``virtual_pi`` in a node map,
+which maps it to the originating ``real_pi``. Additionally, ``delete_virtual_pis`` returns a network with all
+``virtual_pi`` nodes removed and reassigns the edges connected to them to the corresponding ``real_pi`` node stored in
+the ``node_map``.
+
+.. tabs::
+    .. tab:: C++
+        **Header:** ``fiction/networks/virtual_pi_network.hpp``
+
+        .. doxygenclass:: fiction::virtual_pi_network
+           :members:
+
+    .. tab:: Python
+        .. autoclass:: mnt.pyfiction.virtual_pi_network
+           :members:

include/fiction/algorithms/verification/virtual_miter.hpp

@@ -0,0 +1,107 @@
+//
+// Created by benjamin on 7/31/24.
+//
+
+#ifndef FICTION_VIRTUAL_MITER_HPP
+#define FICTION_VIRTUAL_MITER_HPP
+
+#include "fiction/networks/virtual_pi_network.hpp"
+
+#include <mockturtle/traits.hpp>
+
+#include <algorithm>
+#include <optional>
+#include <vector>
+
+namespace fiction
+{
+
+template <typename Ntk>
+auto handle_virtual_pis(const Ntk& network)
+{
+    if constexpr (has_num_virtual_pis_v<Ntk>)
+    {
+        return delete_virtual_pis(network);
+    }
+    else
+    {
+        return network;
+    }
+}
+
+/**
+ * This method combines two networks into a combinational miter, similar to a mockturtle::miter. Either of the input
+ * networks may include virtual inputs (duplicated PIs). During the construction of the virtual miter, duplicated PIs
+ * are removed, and all edges connected to them are remapped to their corresponding original PIs. This ensures that
+ * the number of PIs in the miter networks is consistent when the networks are equivalent.
+ *
+ * The resulting miter has the same number of inputs as the input networks and a single primary output. This output
+ * represents the OR of the XORs of all primary output pairs. In other words, the miter outputs 1 for any input
+ * assignment where the primary outputs of the two input networks differ.
+ *
+ * The input networks may have different types. The method returns an `optional`, which is `nullopt` if the two input
+ * networks have mismatched numbers of primary inputs or primary outputs.
+ */
+template <typename NtkDest, typename NtkSource1, typename NtkSource2>
+std::optional<NtkDest> virtual_miter(const NtkSource1& ntk1_in, const NtkSource2& ntk2_in)
+{
+    static_assert(mockturtle::is_network_type_v<NtkSource1>, "NtkSource1 is not a network type");
+    static_assert(mockturtle::is_network_type_v<NtkSource2>, "NtkSource2 is not a network type");
+    static_assert(mockturtle::is_network_type_v<NtkDest>, "NtkDest is not a network type");
+
+    static_assert(mockturtle::has_num_pis_v<NtkSource1>, "NtkSource1 does not implement the num_pis method");
+    static_assert(mockturtle::has_num_pos_v<NtkSource1>, "NtkSource1 does not implement the num_pos method");
+    static_assert(mockturtle::has_num_pis_v<NtkSource2>, "NtkSource2 does not implement the num_pis method");
+    static_assert(mockturtle::has_num_pos_v<NtkSource2>, "NtkSource2 does not implement the num_pos method");
+    static_assert(mockturtle::has_create_pi_v<NtkDest>, "NtkDest does not implement the create_pi method");
+    static_assert(mockturtle::has_create_po_v<NtkDest>, "NtkDest does not implement the create_po method");
+    static_assert(mockturtle::has_create_xor_v<NtkDest>, "NtkDest does not implement the create_xor method");
+    static_assert(mockturtle::has_create_nary_or_v<NtkDest>, "NtkDest does not implement the create_nary_or method");
+
+    /* handle (delete and remap) virtual primary inputs */
+    auto ntk1 = handle_virtual_pis(ntk1_in);
+    auto ntk2 = handle_virtual_pis(ntk2_in);
+
+    /* both networks must have same number of inputs and outputs */
+    if ((ntk1.num_pis() != ntk2.num_pis()) || (ntk1.num_pos() != ntk2.num_pos()))
+    {
+        return std::nullopt;
+    }
+
+    /* create primary inputs */
+    NtkDest                                  dest;
+    std::vector<mockturtle::signal<NtkDest>> pis;
+    for (auto i = 0u; i < ntk1.num_pis(); ++i)
+    {
+        pis.push_back(dest.create_pi());
+    }
+
+    /* copy networks */
+    const auto pos1 = cleanup_dangling(ntk1, dest, pis.begin(), pis.end());
+    const auto pos2 = cleanup_dangling(ntk2, dest, pis.begin(), pis.end());
+
+    if constexpr (mockturtle::has_EXODC_interface_v<decltype(ntk1)>)
+    {
+        ntk1.build_oe_miter(dest, pos1, pos2);
+        return dest;
+    }
+    if constexpr (mockturtle::has_EXODC_interface_v<decltype(ntk2)>)
+    {
+        ntk2.build_oe_miter(dest, pos1, pos2);
+        return dest;
+    }
+
+    /* create XOR of output pairs */
+    std::vector<mockturtle::signal<NtkDest>> xor_outputs;
+    std::transform(pos1.begin(), pos1.end(), pos2.begin(), std::back_inserter(xor_outputs),
+                   [&](auto const& o1, auto const& o2) { return dest.create_xor(o1, o2); });
+
+    /* create big OR of XOR gates */
+    dest.create_po(dest.create_nary_or(xor_outputs));
+
+    return dest;
+}
+
+}  // namespace fiction
+
+#endif  // FICTION_VIRTUAL_MITER_HPP