Merge remote-tracking branch 'origin/eddie/abc9_refactor' into eddie/abc9_required

diff --cc backends/aiger/xaiger.cc
index 268be432a6d050a281f0e6e73924ee75e2e35fb2,c3fc61e3b13232b85ba1bbe228dc7ae0fc8a77ca..c2d076c86341817c891dc629eb13d169430b26ce
--- 1/backends/aiger/xaiger.cc
--- 2/backends/aiger/xaiger.cc
+++ b/backends/aiger/xaiger.cc
@@@ -233,50 -234,32 +234,53 @@@ struct XAigerWrite
                                                        box_list.resize(abc9_box_seq+1);
                                                box_list[abc9_box_seq] = cell;
                                                // Only flop boxes may have arrival times
-                                               if (!inst_module->get_bool_attribute("\\abc9_flop"))
 +                                              //   (all others are combinatorial)
+                                               if (!abc9_flop)
                                                        continue;
                                        }
  
 -                                      auto &cell_arrivals = arrival_cache[cell->type];
 +                                      auto &cell_arrivals = arrivals_cache[cell->type];
                                        for (const auto &conn : cell->connections()) {
 +                                              auto port_wire = inst_module->wire(conn.first);
 +                                              if (!port_wire->port_output)
 +                                                      continue;
 +
                                                auto r = cell_arrivals.insert(conn.first);
 -                                              auto &arrival = r.first->second;
 +                                              auto &arrivals = r.first->second;
                                                if (r.second) {
 -                                                      auto port_wire = inst_module->wire(conn.first);
 -                                                      if (port_wire->port_output) {
 -                                                              auto it = port_wire->attributes.find("\\abc9_arrival");
 -                                                              if (it != port_wire->attributes.end()) {
 -                                                                      if (it->second.flags != 0)
 -                                                                              log_error("Attribute 'abc9_arrival' on port '%s' of module '%s' is not an integer.\n", log_id(port_wire), log_id(cell->type));
 -                                                                      arrival = it->second.as_int();
 -                                                              }
 -                                                      }
 +                                                      auto it = port_wire->attributes.find("\\abc9_arrival");
 +                                                      if (it == port_wire->attributes.end())
 +                                                              continue;
 +                                                      if (it->second.flags == 0)
 +                                                              arrivals.emplace_back(it->second.as_int());
 +                                                      else
 +                                                              for (const auto &tok : split_tokens(it->second.decode_string()))
 +                                                                      arrivals.push_back(atoi(tok.c_str()));
 +                                              }
 +
 +                                              if (arrivals.empty())
 +                                                      continue;
 +
 +                                              if (GetSize(arrivals) > 1 && GetSize(arrivals) != GetSize(port_wire))
 +                                                      log_error("%s.%s is %d bits wide but abc9_arrival = %s has %d value(s)!\n", log_id(cell->type), log_id(conn.first),
 +                                                                      GetSize(port_wire), log_signal(it->second), GetSize(arrivals));
 +
 +                                              auto jt = arrivals.begin();
 +#ifndef NDEBUG
 +                                              if (ys_debug(1)) {
 +                                                      static std::set<std::pair<IdString,IdString>> seen;
 +                                                      if (seen.emplace(cell->type, conn.first).second) log("%s.%s abc9_arrival = %d\n", log_id(cell->type), log_id(conn.first), *jt);
 +                                              }
 +#endif
 +                                              for (auto bit : sigmap(conn.second)) {
 +                                                      arrival_times[bit] = *jt;
 +                                                      if (arrivals.size() > 1)
 +                                                              jt++;
                                                }
 -                                              if (arrival)
 -                                                      for (auto bit : sigmap(conn.second))
 -                                                              arrival_times[bit] = arrival;
                                        }
+ 
+                                       if (abc9_flop)
+                                               continue;
                                }
                        }