update for exact synthesis

src/commands/exact/exact_lut.hpp

@@ -21,6 +21,7 @@
 
 #include "../../core/exact/exact_dag.hpp"
 #include "../../core/exact/exact_lut.hpp"
+#include "../core/exact/lut_rewriting.hpp"
 
 using namespace std;
 using namespace percy;
@@ -38,6 +39,8 @@ class exact_command : public command {
              "stp based cegar encoding and partial DAG structure");
     add_flag("--dag_depth, -t",
              "cegar encoding and partial DAG structure for Delay");
+    add_flag("--decomposition, -p",
+             "using decomposition before exact synthesis");
     add_option("--output, -o", filename, "the verilog filename");
     add_flag("--enumeration, -e", "enumerate all solutions");
     add_flag("--new_entry, -w", "adds k-LUT store entry");
@@ -46,6 +49,7 @@ class exact_command : public command {
     add_flag("--xag, -g", "enable exact synthesis for XAG, default = false");
     add_flag("--npn, -n", "print result for NPN storing, default = false");
     add_flag("--depth, -d", "print the depth of each result, default = false");
+    add_flag("--parallel, -l", "parallel exact synthesis");
     add_flag("--verbose, -v", "verbose results, default = true");
   }
 
@@ -200,6 +204,29 @@ class exact_command : public command {
     }
   }
 
+  void es_parallel(int nr_in, chain& result) {
+    spec spec;
+    chain c;
+
+    spec.add_alonce_clauses = false;
+    spec.add_nontriv_clauses = false;
+    spec.add_lex_func_clauses = false;
+    spec.add_colex_clauses = false;
+    spec.add_noreapply_clauses = false;
+    spec.add_symvar_clauses = false;
+    spec.verbosity = 0;
+
+    kitty::dynamic_truth_table f(nr_in);
+    kitty::create_from_hex_string(f, tt);
+    spec[0] = f;
+
+    spec.preprocess();
+    auto res = pd_ser_synthesize_parallel(spec, c, 4, "../src/pd/");
+    // auto res = pf_fence_synthesize(spec, c, 8);
+
+    if (res == success) result.copy(c);
+  }
+
   void es_delay(int nr_in, list<chain>& chains) {
     int node = nr_in - 1, max_level = 0, count = 0;
     bool target = false;
@@ -338,6 +365,12 @@ class exact_command : public command {
     return target;
   }
 
+  void es_after_decomposition() {
+    dec_network = store<mockturtle::klut_network>().current();
+    phyLS::lut_rewriting_params ps;
+    dec_network = phyLS::lut_rewriting_c(dec_network, ps);
+  }
+
   void execute() {
     t.clear();
     t.push_back(binary_to_hex());
@@ -544,10 +577,45 @@ class exact_command : public command {
         totalTime = (double)(end - begin) / CLOCKS_PER_SEC;
         cout << "[Total realization]: " << nr_in << endl;
       }
+    } else if (is_set("decomposition")) {
+      begin = clock();
+      es_after_decomposition();
+      end = clock();
+      totalTime = (double)(end - begin) / CLOCKS_PER_SEC;
+    } else if (is_set("parallel")) {
+      int64_t total_elapsed = 0;
+      auto start = std::chrono::steady_clock::now();
+      chain chain;
+      es_parallel(nr_in, chain);
+      const auto elapsed1 =
+          std::chrono::duration_cast<std::chrono::microseconds>(
+              std::chrono::steady_clock::now() - start)
+              .count();
+      total_elapsed += elapsed1;
+      if (ps.verbose) {
+        chain.print_bench();
+        if (ps.depth) {
+          klut_network klut = create_network(chain);
+          mockturtle::depth_view depth_lut{klut};
+          std::cout << "level = " << depth_lut.depth() - 1 << std::endl;
+        }
+      }
+      if (ps.npn) {
+        chain.print_npn();
+        if (ps.depth) {
+          klut_network klut = create_network(chain);
+          mockturtle::depth_view depth_lut{klut};
+          std::cout << "l{" << depth_lut.depth() - 1 << "}" << std::endl;
+        } else {
+          std::cout << std::endl;
+        }
+      }
+      printf("[Total CPU time]   : %ldus\n", total_elapsed);
     } else {
       if (is_set("enumeration")) {
         begin = clock();
-        phyLS::exact_lut_enu(tt_h, nr_in);
+        int cut_size = 0;
+        phyLS::exact_lut_enu(tt_h, nr_in, cut_size);
         end = clock();
         totalTime = (double)(end - begin) / CLOCKS_PER_SEC;
         int count = 0;
@@ -558,7 +626,8 @@ class exact_command : public command {
         cout << "[Total realization]: " << count << endl;
       } else {
         begin = clock();
-        phyLS::exact_lut(tt_h, nr_in);
+        int cut_size = 0;
+        phyLS::exact_lut(tt_h, nr_in, cut_size);
         end = clock();
         totalTime = (double)(end - begin) / CLOCKS_PER_SEC;
         int count = 0;
@@ -582,6 +651,7 @@ class exact_command : public command {
   double min_delay = 0.00;
   int mapping_gate = 0;
   std::string filename = "techmap.v";
+  klut_network dec_network;
 };
 
 ALICE_ADD_COMMAND(exact, "Synthesis")

src/commands/exact/exact_multi.hpp

@@ -0,0 +1,121 @@
+#ifndef EXACT_MULTI_HPP
+#define EXACT_MULTI_HPP
+
+#include <alice/alice.hpp>
+#include <iostream>
+#include <mockturtle/algorithms/klut_to_graph.hpp>
+#include <mockturtle/mockturtle.hpp>
+#include <percy/percy.hpp>
+#include <string>
+#include <vector>
+
+#include "../store.hpp"
+
+using namespace std;
+using namespace percy;
+using namespace mockturtle;
+using kitty::dynamic_truth_table;
+
+using namespace std;
+
+namespace alice {
+
+class exact_window_command : public command {
+ public:
+  explicit exact_window_command(const environment::ptr& env)
+      : command(env, "using exact synthesis to find optimal window") {
+    add_flag("--cegar, -c", "cegar encoding");
+    add_option("--num_functions, -n", num_functions,
+               "set the number of functions to be synthesized, default = 1");
+    add_option("--file, -f", filename, "input filename");
+    add_flag("--verbose, -v", "print the information");
+  }
+
+ private:
+  int num_functions = 1;
+  std::string filename;
+  vector<string> iTT;
+
+  aig_network create_network(chain& c) {
+    klut_network klut;
+    c.store_bench(0);
+    std::string filename = "r_0.bench";
+    if (lorina::read_bench(filename, mockturtle::bench_reader(klut)) !=
+        lorina::return_code::success) {
+      std::cout << "[w] parse error\n";
+    }
+    aig_network aig = convert_klut_to_graph<aig_network>(klut);
+    return aig;
+  }
+
+ protected:
+  void execute() {
+    spec spec;
+    aig_network aig;
+    if (is_set("file")) {
+      ifstream fin_bench(filename);
+      string tmp;
+      if (fin_bench.is_open()) {
+        while (getline(fin_bench, tmp)) {
+          iTT.push_back(tmp);
+        }
+        fin_bench.close();
+        int nr_in = 0, value = 0;
+        while (value < iTT[0].size()) {
+          value = pow(2, nr_in);
+          if (value == iTT[0].size()) break;
+          nr_in++;
+        }
+        for (int i = 0; i < iTT.size(); i++) {
+          kitty::dynamic_truth_table f(nr_in);
+          kitty::create_from_binary_string(f, iTT[i]);
+          spec[i] = f;
+        }
+      }
+    } else {
+      auto store_size = store<optimum_network>().size();
+      assert(store_size >= num_functions);
+      if (!is_set("num_functions")) num_functions = 1;
+      for (int i = 0; i < num_functions; i++) {
+        auto& opt = store<optimum_network>()[store_size - i - 1];
+        auto copy = opt.function;
+        spec[i] = copy;
+      }
+    }
+
+    stopwatch<>::duration time{0};
+    if (is_set("cegar")) {
+      bsat_wrapper solver;
+      msv_encoder encoder(solver);
+      chain c;
+      call_with_stopwatch(time, [&]() {
+        if (synthesize(spec, c, solver, encoder) == success) {
+          c.print_bench();
+          aig = create_network(c);
+          store<aig_network>().extend();
+          store<aig_network>().current() = aig;
+        }
+      });
+    } else {
+      bsat_wrapper solver;
+      ssv_encoder encoder(solver);
+      chain c;
+      call_with_stopwatch(time, [&]() {
+        if (synthesize(spec, c, solver, encoder) == success) {
+          c.print_bench();
+          aig = create_network(c);
+          store<aig_network>().extend();
+          store<aig_network>().current() = aig;
+        }
+      });
+    }
+
+    std::cout << fmt::format("[Total CPU time]   :  {:5.3f} seconds\n",
+                             to_seconds(time));
+  }
+};
+
+ALICE_ADD_COMMAND(exact_window, "Synthesis")
+}  // namespace alice
+
+#endif

src/commands/functional_reduction.hpp

@@ -95,7 +95,7 @@ class fr_command : public command {
   }
 
  private:
-  int max_tfi_node = 10000;
+  int max_tfi_node = 1000;
   string filename = "pattern.log";
 };
 

src/commands/lut_mapping.hpp

@@ -34,10 +34,12 @@ class lut_mapping_command : public command {
       : command(env, "LUT mapping [default = AIG]") {
     add_option("cut_size, -k", cut_size,
                "set the cut size from 2 to 8, default = 4");
-    add_flag("--verbose, -v", "print the information");
     add_flag("--satlut, -s", "satlut mapping");
     add_flag("--xag, -g", "LUT mapping for XAG");
     add_flag("--mig, -m", "LUT mapping for MIG");
+    add_flag("--klut, -l", "LUT mapping for k-LUT");
+    add_flag("--area, -a", "area-oriented mapping, default = no");
+    add_flag("--verbose, -v", "print the information");
   }
 
  protected:
@@ -45,6 +47,9 @@ class lut_mapping_command : public command {
     clock_t begin, end;
     double totalTime;
     lut_mapping_params ps;
+    if (is_set("area")){
+      ps.rounds_ela = 4u;
+    }
 
     if (is_set("mig")) {
       /* derive some MIG */
@@ -78,6 +83,22 @@ class lut_mapping_command : public command {
       totalTime = (double)(end - begin) / CLOCKS_PER_SEC;
       store<klut_network>().extend();
       store<klut_network>().current() = klut;
+    } else if (is_set("klut")) {
+      /* derive some kLUT */
+      assert(store<klut_network>().size() > 0);
+      begin = clock();
+      klut_network klut = store<klut_network>().current();
+
+      mapping_view<klut_network, true> mapped_klut{klut};
+      ps.cut_enumeration_ps.cut_size = cut_size;
+      lut_mapping<mapping_view<klut_network, true>, true>(mapped_klut, ps);
+
+      /* collapse into k-LUT network */
+      const auto klut_new = *collapse_mapped_network<klut_network>(mapped_klut);
+      end = clock();
+      totalTime = (double)(end - begin) / CLOCKS_PER_SEC;
+      store<klut_network>().extend();
+      store<klut_network>().current() = klut_new;
     } else {
       if (store<aig_network>().size() == 0) {
         assert(false && "Error: Empty AIG network\n");

src/commands/techmap.hpp

@@ -49,8 +49,8 @@ namespace alice {
     /* derive genlib */
     std::vector<mockturtle::gate> gates =
         store<std::vector<mockturtle::gate>>().current();
-
     mockturtle::tech_library<5> lib(gates);
+
     mockturtle::map_params ps;
     mockturtle::map_stats st;
 
@@ -79,12 +79,10 @@ namespace alice {
             "[i] Mapped XMG into #gates = {} area = {:.2f} delay = {:.2f}\n",
             res.num_gates(), st.area, st.delay);
       }
-      }
-      else if (is_set("mig")) {
+    } else if (is_set("mig")) {
       if (store<mig_network>().size() == 0u) {
         std::cerr << "[e] no MIG in the store\n";
-        }
-        else {
+      } else {
         auto mig = store<mig_network>().current();
 
         auto res = mockturtle::map(mig, lib, ps, &st);
@@ -97,12 +95,10 @@ namespace alice {
             "Mapped MIG into #gates = {} area = {:.2f} delay = {:.2f}\n",
             res.num_gates(), st.area, st.delay);
       }
-      }
-      else if (is_set("lut")) {
+    } else if (is_set("lut")) {
       if (store<klut_network>().size() == 0u) {
         std::cerr << "[e] no k-LUT in the store\n";
-        }
-        else {
+      } else {
         auto lut = store<klut_network>().current();
 
         auto res = mockturtle::map(lut, lib, ps, &st);
@@ -115,25 +111,26 @@ namespace alice {
             "Mapped k-LUT into #gates = {} area = {:.2f} delay = {:.2f}\n",
             res.num_gates(), st.area, st.delay);
       }
-      }
-      else {
+    } else {
       if (store<aig_network>().size() == 0u) {
         std::cerr << "[e] no AIG in the store\n";
-        }
-        else {
+      } else {
         auto aig = store<aig_network>().current();
-
         auto res = mockturtle::map(aig, lib, ps, &st);
 
-          if (is_set("output")) {
-            write_verilog_with_binding(res, filename);
-          }
+        if (is_set("output")) write_verilog_with_binding(res, filename);
 
-          std::cout << fmt::format(
-            "Mapped AIG into #gates = {} area = {:.2f} delay = {:.2f}\n",
-            res.num_gates(), st.area, st.delay);
+        // std::cout << fmt::format(
+        //     "Mapped AIG into #gates = {}, area = {:.2f}, delay = {:.2f}, "
+        //     "power = {:.2f}\n",
+        //     res.num_gates(), st.area, st.delay, st.power);
       }
     }
+    if (is_set("verbose")) {
+      st.report();
+      cout << "Cut enumeration stats: " << endl;
+      st.cut_enumeration_st.report();
+    }
   }
 };
 

src/phyLS.cpp

@@ -76,7 +76,7 @@
 #include "commands/xag/xagrs.hpp"
 #include "commands/xmg/xmgrs.hpp"
 #include "commands/xmg/xmgrw.hpp"
-#include "commands/exact/exact_multi.hpp"
+// #include "commands/exact/exact_multi.hpp"
 #include "commands/exact/exact_klut.hpp"
 #include "commands/exact/exactlut.hpp"
 #include "commands/to_npz.hpp"