Add ConstEvalAig specialised for AIGs

diff --git a/frontends/aiger/aigerparse.cc b/frontends/aiger/aigerparse.cc
index 72b37d21dae7916dac602d04b96b8356119ca4de..42b3c7624f666b2ecb529f381da547f0233b0977 100644 (file)
--- a/frontends/aiger/aigerparse.cc
+++ b/frontends/aiger/aigerparse.cc
@@ -234,7 +234,7 @@ void AigerReader::parse_xaiger()
                                uint32_t lutNum = parse_xaiger_literal(f);
                                uint32_t lutSize = parse_xaiger_literal(f);
                                log_debug("m: dataSize=%u lutNum=%u lutSize=%u\n", dataSize, lutNum, lutSize);
-                               ConstEval ce(module);
+                               ConstEvalAig ce(module);
                                for (unsigned i = 0; i < lutNum; ++i) {
                                        uint32_t rootNodeID = parse_xaiger_literal(f);
                                        uint32_t cutLeavesM = parse_xaiger_literal(f);
@@ -251,12 +251,11 @@ void AigerReader::parse_xaiger()
                                        }
                                        RTLIL::Const lut_mask(RTLIL::State::Sx, 1 << input_sig.size());
                                        for (int j = 0; j < (1 << cutLeavesM); ++j) {
-                                               ce.push();
+                                               ce.clear();
                                                ce.set(input_sig, RTLIL::Const{j, static_cast<int>(cutLeavesM)});
                                                RTLIL::SigSpec o(output_sig);
                                                ce.eval(o);
                                                lut_mask[j] = o.as_const()[0];
-                                               ce.pop();
                                        }
                                        RTLIL::Cell *output_cell = module->cell(stringf("\\__%d__$and", rootNodeID));
                                        log_assert(output_cell);

diff --git a/kernel/consteval.h b/kernel/consteval.h
index 154373a8deeef29bb2223ae6029d4ffeb167a31c..59e3ef20f41b60a0b8228044256dadce88f93765 100644 (file)
--- a/kernel/consteval.h
+++ b/kernel/consteval.h
@@ -390,6 +390,163 @@ struct ConstEval
        }
 };
 
+struct ConstEvalAig
+{
+       RTLIL::Module *module;
+       //SigMap assign_map;
+       SigMap values_map;
+       //SigPool stop_signals;
+       SigSet<RTLIL::Cell*> sig2driver;
+       std::set<RTLIL::Cell*> busy;
+       std::vector<SigMap> stack;
+       //RTLIL::State defaultval;
+
+       ConstEvalAig(RTLIL::Module *module /*, RTLIL::State defaultval = RTLIL::State::Sm*/) : module(module) /*, assign_map(module), defaultval(defaultval)*/
+       {
+               CellTypes ct;
+               ct.setup_internals();
+               ct.setup_stdcells();
+
+               for (auto &it : module->cells_) {
+                       if (!ct.cell_known(it.second->type))
+                               continue;
+                       for (auto &it2 : it.second->connections())
+                               if (ct.cell_output(it.second->type, it2.first))
+                                       sig2driver.insert(/*assign_map*/(it2.second), it.second);
+               }
+       }
+
+       void clear()
+       {
+               values_map.clear();
+               //stop_signals.clear();
+       }
+
+       void push()
+       {
+               stack.push_back(values_map);
+       }
+
+       void pop()
+       {
+               values_map.swap(stack.back());
+               stack.pop_back();
+       }
+
+       void set(RTLIL::SigSpec sig, RTLIL::Const value)
+       {
+               //assign_map.apply(sig);
+#ifndef NDEBUG
+               RTLIL::SigSpec current_val = values_map(sig);
+               for (int i = 0; i < GetSize(current_val); i++)
+                       log_assert(current_val[i].wire != NULL || current_val[i] == value.bits[i]);
+#endif
+               values_map.add(sig, RTLIL::SigSpec(value));
+       }
+
+       //void stop(RTLIL::SigSpec sig)
+       //{
+       //      assign_map.apply(sig);
+       //      stop_signals.add(sig);
+       //}
+
+       bool eval(RTLIL::Cell *cell, RTLIL::SigSpec &undef)
+       {
+               RTLIL::SigSpec sig_y = values_map(/*assign_map*/(cell->getPort("\\Y")));
+               if (sig_y.is_fully_const())
+                       return true;
+
+               RTLIL::SigSpec sig_a = cell->getPort("\\A");
+               if (sig_a.size() > 0 && !eval(sig_a, undef, cell))
+                       return false;
+
+               RTLIL::Const eval_ret;
+               if (cell->type == "$_NOT_") {
+                       if (sig_a == RTLIL::S0) eval_ret = RTLIL::S1;
+                       else if (sig_a == RTLIL::S1) eval_ret = RTLIL::S0;
+               }
+               else if (cell->type == "$_AND_") {
+                       if (sig_a == RTLIL::S0) {
+                               eval_ret = RTLIL::S0;
+                               goto eval_end;
+                       }
+
+                       {
+                               RTLIL::SigSpec sig_b = cell->getPort("\\B");
+                               if (sig_b.size() > 0 && !eval(sig_b, undef, cell))
+                                       return false;
+                               if (sig_b == RTLIL::S0) {
+                                       eval_ret = RTLIL::S0;
+                                       goto eval_end;
+                               }
+
+                               if (sig_a != RTLIL::State::S1 || sig_b != RTLIL::State::S1) {
+                                       eval_ret = RTLIL::State::Sx;
+                                       goto eval_end;
+                               }
+
+                               eval_ret = RTLIL::State::S1;
+                       }
+               }
+               else log_abort();
+
+
+eval_end:
+               set(sig_y, eval_ret);
+               return true;
+       }
+
+       bool eval(RTLIL::SigSpec &sig, RTLIL::SigSpec &undef, RTLIL::Cell *busy_cell = NULL)
+       {
+               //assign_map.apply(sig);
+               values_map.apply(sig);
+
+               if (sig.is_fully_const())
+                       return true;
+
+               //if (stop_signals.check_any(sig)) {
+               //      undef = stop_signals.extract(sig);
+               //      return false;
+               //}
+
+               if (busy_cell) {
+                       if (busy.count(busy_cell) > 0) {
+                               undef = sig;
+                               return false;
+                       }
+                       busy.insert(busy_cell);
+               }
+
+               std::set<RTLIL::Cell*> driver_cells;
+               sig2driver.find(sig, driver_cells);
+               for (auto cell : driver_cells) {
+                       if (!eval(cell, undef)) {
+                               if (busy_cell)
+                                       busy.erase(busy_cell);
+                               return false;
+                       }
+               }
+
+               if (busy_cell)
+                       busy.erase(busy_cell);
+
+               values_map.apply(sig);
+               if (sig.is_fully_const())
+                       return true;
+
+               for (auto &c : sig.chunks())
+                       if (c.wire != NULL)
+                               undef.append(c);
+               return false;
+       }
+
+       bool eval(RTLIL::SigSpec &sig)
+       {
+               RTLIL::SigSpec undef;
+               return eval(sig, undef);
+       }
+};
+
 YOSYS_NAMESPACE_END
 
 #endif