Virtual pi network

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/network_transformation/delete_virtual_pis.hpp

@@ -0,0 +1,236 @@
+//
+// Created by benjamin on 14.06.24.
+//
+
+#ifndef FICTION_DELETE_VIRTUAL_PIS_HPP
+#define FICTION_DELETE_VIRTUAL_PIS_HPP
+
+#include "fiction/utils/name_utils.hpp"
+
+#include <mockturtle/traits.hpp>
+#include <mockturtle/utils/node_map.hpp>
+#include <mockturtle/views/topo_view.hpp>
+
+#include <cassert>
+#include <cstdint>
+#include <cstdlib>
+#include <utility>
+#include <vector>
+
+#if (PROGRESS_BARS)
+#include <mockturtle/utils/progress_bar.hpp>
+#endif
+
+namespace fiction
+{
+
+namespace detail
+{
+
+template <typename Ntk>
+class delete_virtual_pis_impl
+{
+  public:
+    explicit delete_virtual_pis_impl(const Ntk& ntk_src) : ntk{ntk_src}, ntk_topo{ntk_src} {}
+
+    Ntk run()
+    {
+        auto  init     = initialize_copy_virtual_pi_network(ntk);
+        auto& ntk_dest = init.first;
+        auto& old2new  = init.second;
+
+        const auto gather_fanin_signals = [this, &ntk_dest, &old2new](const auto& n)
+        {
+            std::vector<typename Ntk::signal> children{};
+
+            ntk.foreach_fanin(n,
+                              [this, &ntk_dest, &old2new, &children](const auto& f)
+                              {
+                                  auto fn = ntk.get_node(f);
+
+                                  if (ntk.is_virtual_pi(fn))
+                                  {
+                                      fn = ntk.get_real_pi(fn);
+                                  }
+                                  auto tgt_signal = old2new[fn];
+
+                                  children.emplace_back(ntk.is_complemented(f) ? ntk_dest.create_not(tgt_signal) :
+                                                                                 tgt_signal);
+                              });
+
+            return children;
+        };
+
+#if (PROGRESS_BARS)
+        // initialize a progress bar
+        mockturtle::progress_bar bar{static_cast<uint32_t>(ntk.num_gates()), "[i] network conversion: |{0}|"};
+#endif
+
+        ntk_topo.foreach_gate(
+            [&, this](const auto& g, [[maybe_unused]] auto i)
+            {
+                auto children = gather_fanin_signals(g);
+
+#if (PROGRESS_BARS)
+                // update progress
+                bar(i);
+#endif
+
+                if constexpr (mockturtle::has_is_and_v<Ntk> && mockturtle::has_create_and_v<Ntk>)
+                {
+                    if (ntk.is_and(g))
+                    {
+                        old2new[g] = ntk_dest.create_and(children[0], children[1]);
+                        return true;
+                    }
+                }
+                if constexpr (mockturtle::has_is_or_v<Ntk> && mockturtle::has_create_or_v<Ntk>)
+                {
+                    if (ntk.is_or(g))
+                    {
+                        old2new[g] = ntk_dest.create_or(children[0], children[1]);
+                        return true;
+                    }
+                }
+                if constexpr (mockturtle::has_is_xor_v<Ntk> && mockturtle::has_create_xor_v<Ntk>)
+                {
+                    if (ntk.is_xor(g))
+                    {
+                        old2new[g] = ntk_dest.create_xor(children[0], children[1]);
+                        return true;
+                    }
+                }
+                if constexpr (mockturtle::has_is_maj_v<Ntk> && mockturtle::has_create_maj_v<Ntk>)
+                {
+                    if (ntk.is_maj(g))
+                    {
+                        old2new[g] = ntk_dest.create_maj(children[0], children[1], children[2]);
+                        return true;
+                    }
+                }
+                if constexpr (fiction::has_is_buf_v<Ntk> && mockturtle::has_create_buf_v<Ntk>)
+                {
+                    if (ntk.is_buf(g))
+                    {
+                        old2new[g] = ntk_dest.create_buf(children[0]);
+                        return true;
+                    }
+                }
+                if constexpr (mockturtle::has_node_function_v<Ntk> && mockturtle::has_create_node_v<Ntk>)
+                {
+                    old2new[g] = ntk_dest.create_node(children, ntk.node_function(g));
+                    return true;
+                }
+
+                return true;
+            });
+
+        ntk.foreach_po(
+            [this, &ntk_dest, &old2new](const auto& po)
+            {
+                const auto tgt_signal = old2new[ntk.get_node(po)];
+                const auto tgt_po     = ntk.is_complemented(po) ? ntk_dest.create_not(tgt_signal) : tgt_signal;
+
+                ntk_dest.create_po(tgt_po);
+            });
+
+        // restore signal names if applicable
+        restore_names(ntk, ntk_dest, old2new);
+
+        return ntk_dest;
+    }
+
+  private:
+    /**
+     * Type alias for the topological view of the network.
+     */
+    using TopoNtkSrc = mockturtle::topo_view<Ntk>;
+    /**
+     * Network without virtual PIs.
+     */
+    Ntk ntk;
+    /**
+     * Topological view of the input network.
+     */
+    TopoNtkSrc ntk_topo;
+
+    /**
+     * Initialize a network without virtual primary inputs by copying the given network.
+     *
+     * This function takes a network `src` and returns a new network `dest` without virtual primary inputs.
+     * It creates a map `old2new` to associate the signals from the old network to the corresponding signals in the new
+     * network.
+     *
+     * @tparam Ntk The type of the network.
+     * @param src The source network to be copied.
+     * @return A pair containing the new network without virtual primary inputs and the signal mapping from old to new
+     * network.
+     */
+    [[nodiscard]] std::pair<Ntk, mockturtle::node_map<mockturtle::signal<Ntk>, Ntk>>
+    initialize_copy_virtual_pi_network(const Ntk& src)
+    {
+        static_assert(mockturtle::is_network_type_v<Ntk>, "Ntk is not a network type");
+        static_assert(mockturtle::has_get_constant_v<Ntk>, "Ntk does not implement the get_constant method");
+        static_assert(mockturtle::has_create_pi_v<Ntk>, "Ntk does not implement the create_pi method");
+        static_assert(mockturtle::has_get_node_v<Ntk>, "Ntk does not implement the get_node method");
+        static_assert(fiction::has_foreach_real_pi_v<Ntk>, "Ntk does not implement the foreach_pi method");
+
+        mockturtle::node_map<mockturtle::signal<Ntk>, Ntk> old2new(src);
+        Ntk                                                dest;
+
+        old2new[src.get_constant(false)] = dest.get_constant(false);
+        if (src.get_node(src.get_constant(true)) != src.get_node(src.get_constant(false)))
+        {
+            old2new[src.get_constant(true)] = dest.get_constant(true);
+        }
+        src.foreach_real_pi([&](auto const& n) { old2new[n] = dest.create_pi(); });
+
+        return {dest, old2new};
+    }
+};
+}  // namespace detail
+
+/**
+ * Deletes virtual primary inputs from a network and maps all signals connected to virtual PIs back to the corresponding
+ * real PI. The main use is equivalence checking. If the network does not have any virtual PIs stored, the
+ * network is returned.
+ *
+ * @tparam Ntk The type of network.
+ * @param ntk The input network.
+ * @return The resulting network after virtual primary inputs are deleted.
+ */
+template <typename Ntk>
+Ntk delete_virtual_pis(const Ntk& ntk) noexcept
+{
+    static_assert(mockturtle::is_network_type_v<Ntk>, "Ntk is not a network type");
+    static_assert(mockturtle::has_clone_v<Ntk>, "Ntk does not implement the clone constructor");
+    static_assert(mockturtle::has_get_node_v<Ntk>, "Ntk does not implement the get_node function");
+    static_assert(mockturtle::has_is_complemented_v<Ntk>, "Ntk does not implement the is_complemented function");
+    static_assert(mockturtle::has_foreach_pi_v<Ntk>, "Ntk does not implement the foreach_pi function");
+    static_assert(mockturtle::has_foreach_gate_v<Ntk>, "Ntk does not implement the foreach_gate function");
+    static_assert(mockturtle::has_foreach_po_v<Ntk>, "Ntk does not implement the foreach_po function");
+    static_assert(mockturtle::has_foreach_fanin_v<Ntk>, "Ntk does not implement the foreach_fanin function");
+    static_assert(mockturtle::has_get_constant_v<Ntk>, "Ntk does not implement the get_constant function");
+    static_assert(mockturtle::has_create_pi_v<Ntk>, "Ntk does not implement the create_pi function");
+    static_assert(mockturtle::has_create_po_v<Ntk>, "Ntk does not implement the create_po function");
+    static_assert(mockturtle::has_create_not_v<Ntk>, "Ntk does not implement the create_not function");
+    static_assert(fiction::is_virtual_network_type_v<Ntk>, "Ntk does not implement the get_real_pi function");
+
+    assert(ntk.is_combinational() && "Network has to be combinational");
+
+    // to match the return type the network has to be cloned.
+    if (ntk.num_virtual_pis() == 0)
+    {
+        return ntk;
+    }
+
+    detail::delete_virtual_pis_impl<Ntk> p{ntk};
+
+    const auto result = p.run();
+
+    return result;
+}
+
+}  // namespace fiction
+
+#endif  // FICTION_DELETE_VIRTUAL_PIS_HPP

include/fiction/algorithms/verification/virtual_miter.hpp

@@ -0,0 +1,126 @@
+//
+// Created by benjamin on 31.07.24.
+//
+
+#ifndef FICTION_VIRTUAL_MITER_HPP
+#define FICTION_VIRTUAL_MITER_HPP
+
+#include "fiction/traits.hpp"
+
+#include <fiction/algorithms/network_transformation/delete_virtual_pis.hpp>
+
+#include <mockturtle/traits.hpp>
+
+#include <algorithm>
+#include <optional>
+#include <vector>
+
+namespace fiction
+{
+
+/**
+ * Removes virtual primary inputs from a network if supported. Otherwise the input network is returned unmodified.
+ *
+ * @tparam Ntk The network type.
+ * @param network The input network to process.
+ * @return The network with virtual primary inputs removed, or the original network if unsupported.
+ */
+template <typename Ntk>
+Ntk handle_virtual_pis(const Ntk& network)
+{
+    if constexpr (has_num_virtual_pis_v<Ntk>)
+    {
+        return delete_virtual_pis(network);
+    }
+    else
+    {
+        return network;
+    }
+}
+
+/**
+ * Combines two networks into a combinational miter, similar to `mockturtle::miter`. Either input network  may include
+ * virtual primary inputs (PIs). Virtual PIs are removed during miter construction, and all edges connected to them are
+ * remapped to their corresponding original PIs, ensuring consistent PI counts when the networks are equivalent.
+ *
+ * The resulting miter connects two networks with the same number of inputs and produces a single primary output. This
+ * output represents the OR of the XORs of all primary output pairs. Thus, the miter outputs 1 for any input assignment
+ * where the primary outputs of the two networks differ.
+ *
+ * The input networks may have different types. If the two input networks have mismatched numbers of primary inputs or
+ * outputs, the method returns `nullopt`.
+ *
+ * @tparam NtkDest The type of the resulting network.
+ * @tparam NtkSource1 The type of the first input network.
+ * @tparam NtkSource2 The type of the second input network.
+ * @param ntk1_in The first input network.
+ * @param ntk2_in The second input network.
+ * @return An `optional` containing the virtual miter network if successful, or `nullopt` if the networks are
+ * incompatible.
+ */
+
+template <typename NtkDest, typename NtkSrc1, typename NtkSrc2>
+[[nodiscard]] std::optional<NtkDest> virtual_miter(const NtkSrc1& ntk1_in, const NtkSrc2& ntk2_in) noexcept
+{
+    static_assert(mockturtle::is_network_type_v<NtkSrc1>, "NtkSource1 is not a network type");
+    static_assert(mockturtle::is_network_type_v<NtkSrc2>, "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<NtkSrc1>, "NtkSource1 does not implement the num_pis method");
+    static_assert(mockturtle::has_num_pos_v<NtkSrc1>, "NtkSource1 does not implement the num_pos method");
+    static_assert(mockturtle::has_num_pis_v<NtkSrc2>, "NtkSource2 does not implement the num_pis method");
+    static_assert(mockturtle::has_num_pos_v<NtkSrc2>, "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
+    const NtkSrc1 ntk1 = handle_virtual_pis(ntk1_in);
+    const NtkSrc2 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{};
+    pis.reserve(ntk1.num_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.cbegin(), pis.cend());
+    const auto pos2 = cleanup_dangling(ntk2, dest, pis.cbegin(), pis.cend());
+
+    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{};
+    xor_outputs.reserve(ntk1.num_pos());
+    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