✨ Defect-aware on-the-fly SiDB circuit designer (#317)

* 🎨 Refactored the technology mapping interface into its own header for better re-usability * 📝 Added documentation * 🎨 Addressed `clang-tidy`'s warnings * ✅ Increased test coverage * 👷 Updated workflows to disable benchmark compilation * ✨ Introduce support for 2-ary LT, GT, LE, and GE gates * ✨ Introduce support for the LT, GT, LE, and GE gates in the truth table utils * ✨ Added the outline for the SiDB dynamic gate library for on-the-fly gate generation * ✨ Added the outline for the SiDB dynamic gate library experiment script * 🎨 Added folder to write layouts into * 🎨 Utilize ALL 2-input functions * 📝 Added truth table helper functions to the RST documentation * ✨ support defects in the ``SiDB Gate Designer`` * 🎨 update docu. * 🎨 delete redundant line. * 🎨 implement Marcel's suggestions. * 🚀 P&R and gate on the fly works. * 🎨 shift skeletons to have same position as the bestagon gates * 🎨 add skeletons * 🎨 delete redundant code. * 🎨 choose correct order * 🎨 add mode to use for gate design * 🎨 add check to ensure that placed SiDBs have the specified distance to neutral defects. * 🎨 code cleanup * 🚧 latest version. * 🎨 commit before architectural change * 🎨 architectural change * 🎨 architectural change and update blacklist. * ✨ defect-aware SiDB circuit designer with on-the-fly gate design. * 🎨 small fix. * 🔥 delete bestagon.json * 🎨 add previous bestagon.json file * 🎨 add additional parameter ``influence_radius_charged_defects`` * 🐛 fix smaller bugs. * 🎨 update evaluation script. * 🎨 small fix. * 🔥 delete skeletons. * 🔥 delete .gitkeep. * 🎨 take original generate_defective_surface.py file * 🎨 ClangFormat changes Signed-off-by: ClangFormat <[email protected]> * 🐛 fix docu issue. * 🎨 update lambda expression. * 🎨 update docu. * 🐛 add runtime digit. * 🎨 delete ``const`` * 🎨 define error gate in fcn_gate_library.hpp * 🐛 fix small issue. * ✨ function to check if gate design is impossible due to defects * ✅ add test. * 🎨 small adaptations. * 🎨 ClangFormat changes Signed-off-by: ClangFormat <[email protected]> * 🎨 small adaptations. * 🎨 add note. * 🎨 remove ``const``. * 🎨 ClangFormat changes Signed-off-by: ClangFormat <[email protected]> * 🎨 treat neutral atomic defects differently in quickexact.hpp. * 🎨 use exceptions instead of ``ERROR`` gate * 🎨 ClangFormat changes Signed-off-by: ClangFormat <[email protected]> * 🎨 add more exceptions. * 🎨 ClangFormat changes Signed-off-by: ClangFormat <[email protected]> * 🎨 change structure. * 🎨 implement clang-tidy suggestion. * 🎨 smaller changes here and there. * 🎨 ClangFormat changes Signed-off-by: ClangFormat <[email protected]> * 🎨 revert changes in experiment script. * 🎨 implement Marcel's suggestions, first batch. * 🎨 ClangFormat changes Signed-off-by: ClangFormat <[email protected]> * 🎨 rename dynamic to on-the-fly. * 🎨 introduce new exception class. * 🎨 rename ``tile`` to ``error_tile``. * 🎨 fix typo. * 🎨 small fix. * 🎨 add reference. * 🎨 ClangFormat changes Signed-off-by: ClangFormat <[email protected]> * ✅ update unit test. * 🎨 implement Marcel's suggestions. * 🎨 ClangFormat changes Signed-off-by: ClangFormat <[email protected]> * 🎨 small fix. * 🎨 add parameter as typename. * 🎨 allow fiction coordinates for simulation. * 🎨 remove redundant static_cast. * 🎨 add static_cast * ✅ add further test for bdl input iterator. * 🎨 add missing namespace. * 🎨 allow offset coordinates for gate design * 🎨 reformat code * 🎨 small fix. * 🎨 structural changes. * 🎨 small change. * 🎨 add termination condition. * 🎨 small fix. * 🚧 trying to fix windows CI issue. * 🎨 ClangFormat changes Signed-off-by: ClangFormat <[email protected]> * 🚧 trying to fix windows CI issue. * 🚧 trying to fix windows CI issue. * 🎨 ClangFormat changes Signed-off-by: ClangFormat <[email protected]> * 🚧 trying to fix windows CI issue. * 🎨 implement the first batch. * 🎨 some changes here and there. * 🎨 ClangFormat changes Signed-off-by: ClangFormat <[email protected]> * 🎨 more consistency. * 🎨 ClangFormat changes Signed-off-by: ClangFormat <[email protected]> * 🎨 update experiments. * ✅ add unit test. * 🔀 resolve merge conflict. * 🎨 small update of experiment script. * 🔀 merge ``main`` in. * 🎨 ClangFormat changes Signed-off-by: ClangFormat <[email protected]> * 🎨 Incorporated pre-commit fixes * 🎨 update code after merge. * 🎨 update code after merge. * 📝 small fix. * 📝 small fix. * 📝 small fix. * 📝 small fix. * 📝 small fix. * 🎨 small update of experiments. * 🎨 fix smaller issues. * 📝 Update pyfiction docstrings Signed-off-by: GitHub Actions <[email protected]> * 🎨 small fix. * 🎨 add defect support to bounding box. * 🎨 small fixes. * 🎨 Incorporated pre-commit fixes * 🐛 ``min`` and ``max`` are calculated correctly. * 🎨 small fix. * 🎨 simplify the experiment script. * 🎨 small fix. * 🎨 small fix. * 🎨 minor changes. * 🎨 resize via bb. * 🎨 a few structural changes. * 📝 Update pyfiction docstrings Signed-off-by: GitHub Actions <[email protected]> * 🎨 delete header comments. * 🎨 add missing header. * 🎨 small fix. * 🎨 small fix. * 🎨 small renaming. * 🎨 small change. * 🎨 small fixes. * 📝 Update pyfiction docstrings Signed-off-by: GitHub Actions <[email protected]> * 🎨 small fixes. * 📝 Update pyfiction docstrings Signed-off-by: GitHub Actions <[email protected]> * 🎨 small fixes. * 🎨 small fixes. * 📝 Update pyfiction docstrings Signed-off-by: GitHub Actions <[email protected]> * 🎨 integrate first batch of Marcel's comments. * 📝 Update pyfiction docstrings Signed-off-by: GitHub Actions <[email protected]> * 🎨 small fix. * 🎨 Incorporated pre-commit fixes * 📝 Update pyfiction docstrings Signed-off-by: GitHub Actions <[email protected]> * 🎨 implement Marcel's suggestions. * 📝 add docu. * 🎨 Incorporated pre-commit fixes * 📝 small fix. * 📝 small fix. * 📝 update docu. * 📝 Update pyfiction docstrings Signed-off-by: GitHub Actions <[email protected]> * 🎨 remove superfluous header files. * 🎨 add missing headers. * 🎨 fix headers. * 🎨 Incorporated pre-commit fixes * 📝 Update pyfiction docstrings Signed-off-by: GitHub Actions <[email protected]> * 📝 small fix. * 🎨 Consistency changes and docstring fixes * 📝 Update pyfiction docstrings Signed-off-by: GitHub Actions <[email protected]> * 🎨 small renaming. * 🎨 small fix. * 📝 Update pyfiction docstrings Signed-off-by: GitHub Actions <[email protected]> * 🎨 Incorporated pre-commit fixes * 🎨 small fix. * 🎨 symplify code. * 🎨 Incorporated pre-commit fixes * 🎨 integrate Marcel's comment. * 📝 Update pyfiction docstrings Signed-off-by: GitHub Actions <[email protected]> * 🎨 fix missing renaming. * 🎨 integrate marcel's feedback. * 💚 try to fix codecov issue. * 📝 Update pyfiction docstrings Signed-off-by: GitHub Actions <[email protected]> * 💚 try to fix codecov issue. * 💚 try to fix codecov issue. * 💚 try to fix codecov issue. * 💚 try to fix codecov issue. * 💚 try to fix codecov issue. * 💚 try to fix codecov issue. * 💚 try to fix codecov issue. * 💚 try to fix codecov issue. * 💚 try to fix codecov issue. * 💚 try to fix codecov issue. * ⏪ revert changes. * 📝 small fix. * 📝 small fix. --------- Signed-off-by: ClangFormat <[email protected]> Signed-off-by: GitHub Actions <[email protected]> Co-authored-by: Marcel Walter <[email protected]> Co-authored-by: ClangFormat <[email protected]> Co-authored-by: pre-commit-ci[bot] <66853113+pre-commit-ci[bot]@users.noreply.github.com> Co-authored-by: GitHub Actions <[email protected]>
cda-tum · Aug 17, 2024 · 246bb8d · 246bb8d
1 parent 93da76b
commit 246bb8d
Show file tree

Hide file tree

Showing 57 changed files with 4,762 additions and 1,194 deletions.
diff --git a/...ngs/pyfiction/include/pyfiction/algorithms/network_transformation/fanout_substitution.hpp b/...ngs/pyfiction/include/pyfiction/algorithms/network_transformation/fanout_substitution.hpp
@@ -10,6 +10,7 @@
 
 #include <fiction/algorithms/network_transformation/fanout_substitution.hpp>
 
+#include <pybind11/cast.h>
 #include <pybind11/pybind11.h>
 
 namespace pyfiction

diff --git a/...ings/pyfiction/include/pyfiction/algorithms/network_transformation/technology_mapping.hpp b/...ings/pyfiction/include/pyfiction/algorithms/network_transformation/technology_mapping.hpp
@@ -10,6 +10,7 @@
 
 #include <fiction/algorithms/network_transformation/technology_mapping.hpp>
 
+#include <pybind11/cast.h>
 #include <pybind11/pybind11.h>
 
 namespace pyfiction

diff --git a/bindings/pyfiction/include/pyfiction/layouts/cartesian_layout.hpp b/bindings/pyfiction/include/pyfiction/layouts/cartesian_layout.hpp
@@ -8,6 +8,7 @@
 #include "pyfiction/documentation.hpp"
 #include "pyfiction/types.hpp"
 
+#include <fiction/io/print_layout.hpp>
 #include <fiction/traits.hpp>
 
 #include <pybind11/pybind11.h>

diff --git a/bindings/pyfiction/include/pyfiction/pybind11_mkdoc_docstrings.hpp b/bindings/pyfiction/include/pyfiction/pybind11_mkdoc_docstrings.hpp
diff --git a/bindings/pyfiction/include/pyfiction/technology/sidb_defects.hpp b/bindings/pyfiction/include/pyfiction/technology/sidb_defects.hpp
@@ -67,7 +67,8 @@ inline void sidb_defects(pybind11::module& m)
     m.def("is_neutrally_charged_defect", &fiction::is_neutrally_charged_defect, "defect"_a,
           DOC(fiction_is_neutrally_charged_defect));
 
-    m.def("defect_extent", &fiction::defect_extent, "defect"_a, DOC(fiction_defect_extent));
+    m.def("defect_extent", &fiction::defect_extent, "defect"_a, "charged_defect_spacing_overwrite"_a,
+          "neutral_defect_spacing_overwrite"_a, DOC(fiction_defect_extent));
 }
 
 }  // namespace pyfiction

diff --git a/cli/cmd/logic/map.hpp b/cli/cmd/logic/map.hpp
@@ -38,6 +38,10 @@ class map_command : public command
         add_flag("--nor", ps.nor2, "Enable the use of NOR gates");
         add_flag("--xor,-x", ps.xor2, "Enable the use of XOR gates");
         add_flag("--xnor", ps.xnor2, "Enable the use of XNOR gates");
+        add_flag("--lt", ps.lt2, "Enable the use of LT gates");
+        add_flag("--gt", ps.gt2, "Enable the use of GT gates");
+        add_flag("--le", ps.le2, "Enable the use of LE gates");
+        add_flag("--ge", ps.ge2, "Enable the use of GE gates");
         add_flag("--inv,-i", ps.inv, "Enable the use of NOT gates");
 
         add_flag("--maj,-m", ps.maj3, "Enable the use of MAJ gates");

diff --git a/docs/algorithms/algorithms.rst b/docs/algorithms/algorithms.rst
@@ -58,6 +58,7 @@ Physical Design
    determine_clocking.rst
    apply_gate_library.rst
    design_sidb_gates.rst
+   on_the_fly_circuit_design_on_defective_surface.rst
 
 
 Verification

diff --git a/docs/algorithms/apply_gate_library.rst b/docs/algorithms/apply_gate_library.rst
@@ -12,6 +12,7 @@ implementations for each gate present in the passed ``gate_level_layout``.
         **Header:** ``fiction/algorithms/physical_design/apply_gate_library.hpp``
 
         .. doxygenfunction:: fiction::apply_gate_library(const GateLyt& lyt)
+        .. doxygenfunction:: fiction::apply_parameterized_gate_library(const GateLyt& lyt, const Params& params)
 
     .. tab:: Python
         .. autofunction:: mnt.pyfiction.apply_qca_one_library

diff --git a/docs/algorithms/on_the_fly_circuit_design_on_defective_surface.rst b/docs/algorithms/on_the_fly_circuit_design_on_defective_surface.rst
@@ -0,0 +1,33 @@
+.. _on_the_fly_design:
+
+SiDB Circuit Design Algorithm in the Presence of Atomic Defects
+---------------------------------------------------------------
+
+This algorithm is designed to create SiDB circuits on a clocked surface, accommodating the presence of atomic defects.
+
+1. **Blacklist Generation**:
+
+   Initially, a blacklist of gate-tile pairs is generated. This blacklist is based on the locations of neutrally charged atomic defects and their overlap with the I/O pins of the SiDB skeletons.
+
+2. **Gate-Level Layout Design**:
+
+   Using the generated blacklist, a gate-level layout is designed with the ``exact`` algorithm. This process involves:
+
+   - **Valid Layout Found**:
+
+     If a valid gate-level layout is found, the corresponding gates are implemented with SiDBs.
+
+   - **Invalid Layout**:
+
+     If a valid layout is not found, the blacklist is updated, and the placement and routing process is repeated.
+
+This iterative approach ensures that the designed SiDB circuits can effectively handle defects present on the surface.
+
+
+**Header:** ``fiction/algorithms/physical_design/on_the_fly_circuit_design_on_defective_surface.hpp``
+
+.. doxygenstruct:: fiction::on_the_fly_circuit_design_params
+   :members:
+.. doxygenstruct:: fiction::on_the_fly_circuit_design_stats
+    :members:
+.. doxygenfunction:: fiction::on_the_fly_circuit_design_on_defective_surface
diff --git a/docs/technology/gate_libraries.rst b/docs/technology/gate_libraries.rst
@@ -20,7 +20,9 @@ Abstract Gate Library
    :members:
 
 .. doxygenclass:: fiction::unsupported_gate_type_exception
+    :members:
 .. doxygenclass:: fiction::unsupported_gate_orientation_exception
+    :members:
 
 **Header:** ``fiction/technology/cell_ports.hpp``
 
@@ -58,3 +60,16 @@ SiDB Bestagon Library
 
 .. doxygenclass:: fiction::sidb_bestagon_library
    :members:
+
+Parameterized SiDB Library
+--------------------------
+
+**Header:** ``fiction/technology/sidb_on_the_fly_gate_library.hpp``
+
+.. doxygenstruct:: fiction::sidb_on_the_fly_gate_library_params
+   :members:
+.. doxygenclass:: fiction::sidb_on_the_fly_gate_library
+   :members:
+
+.. doxygenclass:: fiction::gate_design_exception
+   :members:
diff --git a/docs/technology/simulation.rst b/docs/technology/simulation.rst
@@ -56,6 +56,16 @@ distributions of the SiDBs. Charge distribution surfaces are returned by the SiD
             :members:
 
 
+Is SiDB gate design deemed impossible
+-------------------------------------
+
+**Header:** ``fiction/technology/is_sidb_gate_design_impossible.hpp``
+
+.. doxygenstruct:: fiction::is_sidb_gate_design_impossible_params
+   :members:
+.. doxygenfunction:: fiction::is_sidb_gate_design_impossible
+
+
 Physical Constants
 ------------------
 

diff --git a/...ysical_design_with_on_the_fly_gate_design/physical_design_with_on_the_fly_gate_design.cpp b/...ysical_design_with_on_the_fly_gate_design/physical_design_with_on_the_fly_gate_design.cpp
@@ -0,0 +1,190 @@
+//
+// Created by Jan Drewniok on 20.10.23.
+//
+
+#if (FICTION_Z3_SOLVER)
+
+#include "fiction_experiments.hpp"
+
+#include <fiction/algorithms/network_transformation/technology_mapping.hpp>
+#include <fiction/algorithms/physical_design/design_sidb_gates.hpp>
+#include <fiction/algorithms/physical_design/on_the_fly_circuit_design_on_defective_surface.hpp>
+#include <fiction/algorithms/simulation/sidb/sidb_simulation_engine.hpp>
+#include <fiction/io/read_sidb_surface_defects.hpp>
+#include <fiction/layouts/bounding_box.hpp>
+#include <fiction/technology/area.hpp>
+#include <fiction/technology/cell_technologies.hpp>
+#include <fiction/technology/sidb_defect_surface.hpp>
+#include <fiction/technology/sidb_defects.hpp>
+#include <fiction/traits.hpp>
+#include <fiction/types.hpp>
+
+#include <fmt/format.h>
+#include <lorina/lorina.hpp>
+#include <mockturtle/algorithms/cut_rewriting.hpp>
+#include <mockturtle/algorithms/equivalence_checking.hpp>
+#include <mockturtle/algorithms/miter.hpp>
+#include <mockturtle/algorithms/node_resynthesis/xag_npn.hpp>
+#include <mockturtle/io/verilog_reader.hpp>
+#include <mockturtle/networks/klut.hpp>
+#include <mockturtle/networks/xag.hpp>
+#include <mockturtle/utils/stopwatch.hpp>
+#include <mockturtle/views/depth_view.hpp>
+
+#include <cassert>
+#include <cstdlib>
+#include <string>
+
+// This script conducts defect-aware placement and routing with defect-aware on-the-fly SiDB gate design. Thereby, SiDB
+// circuits can be designed in the presence of atomic defects.
+
+int main()  // NOLINT
+{
+    using gate_lyt = fiction::hex_even_row_gate_clk_lyt;
+    using cell_lyt = fiction::sidb_cell_clk_lyt_cube;
+
+    fiction::design_sidb_gates_params<fiction::cell<cell_lyt>> design_gate_params{};
+    design_gate_params.simulation_parameters = fiction::sidb_simulation_parameters{2, -0.32};
+    // needs to be changed if a different skeleton is used.
+    design_gate_params.canvas = {{24, 17}, {34, 28}};
+
+    design_gate_params.number_of_sidbs = 3;
+    design_gate_params.sim_engine      = fiction::sidb_simulation_engine::QUICKEXACT;
+    design_gate_params.termination_cond =
+        fiction::design_sidb_gates_params<fiction::cell<cell_lyt>>::termination_condition::AFTER_FIRST_SOLUTION;
+
+    // save atomic defects which their respective physical parameters as experimentally determined by T. R. Huff, T.
+    // Dienel, M. Rashidi, R. Achal, L. Livadaru, J. Croshaw, and R. A. Wolkow, "Electrostatic landscape of a
+    // Hydrogen-terminated Silicon Surface Probed by a Moveable Quantum Dot."
+    const auto stray_db   = fiction::sidb_defect{fiction::sidb_defect_type::DB, -1, 4.1, 1.8};
+    const auto si_vacancy = fiction::sidb_defect{fiction::sidb_defect_type::SI_VACANCY, -1, 10.6, 5.9};
+
+    static const std::string layouts_folder =
+        fmt::format("{}/physical_design_with_on_the_fly_gate_design/layouts", EXPERIMENTS_PATH);
+
+    // read-in the initial defects. Physical parameters of the defects are not stored yet.
+    auto surface_lattice_initial = fiction::read_sidb_surface_defects<cell_lyt>(
+        "../../experiments/physical_design_with_on_the_fly_gate_design/1_percent_with_charged_surface.txt");
+
+    // create an empty surface.
+    fiction::sidb_defect_surface<cell_lyt> surface_lattice{};
+
+    // add physical parameters of the defects to the surface_lattice.
+    surface_lattice_initial.foreach_sidb_defect(
+        [&surface_lattice, &stray_db, &si_vacancy](const auto& cd)
+        {
+            if (cd.second.type == fiction::sidb_defect_type::DB)
+            {
+                surface_lattice.assign_sidb_defect(cd.first, stray_db);
+            }
+            else if (cd.second.type == fiction::sidb_defect_type::SI_VACANCY)
+            {
+                surface_lattice.assign_sidb_defect(cd.first, si_vacancy);
+            }
+            else
+            {
+                surface_lattice.assign_sidb_defect(cd.first, cd.second);
+            }
+        });
+
+    // determine bounding-box of the surface to set the aspect ratio of the surface lattice.
+    const auto bb_defect_surface = fiction::bounding_box_2d{surface_lattice};
+    surface_lattice.resize(bb_defect_surface.get_max());
+
+    const auto lattice_tiling = gate_lyt{{11, 30}};
+
+    experiments::experiment<std::string, double, uint64_t, bool> sidb_circuits_with_defects{
+        "sidb_circuits_with_defects", "benchmark", "runtime", "number of aspect ratios", "equivalent"};
+
+    constexpr const uint64_t bench_select =
+        fiction_experiments::all & ~fiction_experiments::parity & ~fiction_experiments::two_bit_add_maj &
+        ~fiction_experiments::b1_r2 & ~fiction_experiments::clpl & ~fiction_experiments::iscas85 &
+        ~fiction_experiments::epfl & ~fiction_experiments::half_adder & ~fiction_experiments::full_adder &
+        ~fiction_experiments::one_bit_add_aoig & ~fiction_experiments::one_bit_add_maj & ~fiction_experiments::cm82a_5;
+
+    for (const auto& benchmark : fiction_experiments::all_benchmarks(bench_select))
+    {
+        fmt::print("[attempts] processing {}\n", benchmark);
+        mockturtle::xag_network xag{};
+
+        [[maybe_unused]] const auto read_verilog_result =
+            lorina::read_verilog(fiction_experiments::benchmark_path(benchmark), mockturtle::verilog_reader(xag));
+        assert(read_verilog_result == lorina::return_code::success);
+
+        // compute depth
+        const mockturtle::depth_view depth_xag{xag};
+
+        const fiction::technology_mapping_params tech_map_params = fiction::all_2_input_functions();
+
+        // parameters for cut rewriting
+        mockturtle::cut_rewriting_params cut_params{};
+        cut_params.cut_enumeration_ps.cut_size = 4;
+
+        const mockturtle::xag_npn_resynthesis<mockturtle::xag_network,                    // the input network type
+                                              mockturtle::xag_network,                    // the database network type
+                                              mockturtle::xag_npn_db_kind::xag_complete>  // the kind of database to use
+
+            resynthesis_function{};
+
+        // rewrite network cuts using the given re-synthesis function
+        const auto cut_xag = mockturtle::cut_rewriting(xag, resynthesis_function, cut_params);
+
+        // perform technology mapping
+        const auto mapped_network = fiction::technology_mapping(cut_xag, tech_map_params);
+
+        fiction::on_the_fly_circuit_design_params<cell_lyt> params{};
+        params.exact_design_parameters.scheme        = "ROW4";
+        params.exact_design_parameters.crossings     = true;
+        params.exact_design_parameters.border_io     = false;
+        params.exact_design_parameters.desynchronize = true;
+        params.exact_design_parameters.upper_bound_x = 11;         // 12 x 31 tiles
+        params.exact_design_parameters.upper_bound_y = 30;         // 12 x 31 tiles
+        params.exact_design_parameters.timeout       = 3'600'000;  // 1h in ms
+
+        params.sidb_on_the_fly_gate_library_parameters.defect_surface     = surface_lattice;
+        params.sidb_on_the_fly_gate_library_parameters.design_gate_params = design_gate_params;
+
+        fiction::on_the_fly_circuit_design_stats<gate_lyt> st{};
+
+        const auto result =
+            fiction::on_the_fly_circuit_design_on_defective_surface<decltype(mapped_network), cell_lyt, gate_lyt>(
+                mapped_network, lattice_tiling, params, &st);
+
+        // check equivalence
+        const auto miter = mockturtle::miter<mockturtle::klut_network>(mapped_network, st.gate_layout.value());
+        const auto eq    = mockturtle::equivalence_checking(*miter);
+        assert(eq.has_value());
+
+        // determine bounding box and exclude atomic defects
+        const auto bb = fiction::bounding_box_2d<cell_lyt>(static_cast<cell_lyt>(result));
+
+        // compute area
+        fiction::area_stats                            area_stats{};
+        fiction::area_params<fiction::sidb_technology> area_ps{};
+        fiction::area(bb, area_ps, &area_stats);
+
+        sidb_circuits_with_defects(benchmark, mockturtle::to_seconds(st.time_total), st.exact_stats.num_aspect_ratios,
+                                   *eq);
+        sidb_circuits_with_defects.save();
+        sidb_circuits_with_defects.table();
+
+        // write a SiQAD simulation file
+        // fiction::write_sqd_layout(result, fmt::format("{}/{}.sqd", layouts_folder, benchmark));
+    }
+
+    return EXIT_SUCCESS;
+}
+
+#else  // FICTION_Z3_SOLVER
+
+#include <cstdlib>
+#include <iostream>
+
+int main()  // NOLINT
+{
+    std::cerr << "[e] Z3 solver is not available, please install Z3 and recompile the code" << std::endl;
+
+    return EXIT_FAILURE;
+}
+
+#endif  // FICTION_Z3_SOLVER