aiger/xaiger: use odd for negedge clk, even for posedge

Since abc9 doesn't like negative mergeability values

diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc
index b8d65de4e0eedb8b327a6634a311722b0aa23622..e2d8e1e7f8d8e65b1cfc7e31dbcf4e4a49a55dcb 100644 (file)
--- a/backends/aiger/xaiger.cc
+++ b/backends/aiger/xaiger.cc
@@ -627,21 +627,25 @@ struct XAigerWriter
                        write_s_buffer(ff_bits.size());
 
                        dict<SigBit, int> clk_to_mergeability;
+                       for (const auto &i : ff_bits) {
+                               const Cell *cell = i.second;
+                               log_assert(cell->type.in(ID($_DFF_N_), ID($_DFF_P_)));
+
+                               SigBit clock = sigmap(cell->getPort(ID::C));
+                               clk_to_mergeability.insert(std::make_pair(clock, clk_to_mergeability.size()*2+1));
+                       }
 
                        for (const auto &i : ff_bits) {
                                const SigBit &d = i.first;
                                const Cell *cell = i.second;
 
-                               log_assert(cell->type.in(ID($_DFF_N_), ID($_DFF_P_)));
-
                                SigBit clock = sigmap(cell->getPort(ID::C));
-                               auto r = clk_to_mergeability.insert(std::make_pair(clock, clk_to_mergeability.size() + 1));
-                               int mergeability = r.first->second;
+                               int mergeability = clk_to_mergeability.at(clock);
                                log_assert(mergeability > 0);
                                if (cell->type == ID($_DFF_N_))
-                                       write_r_buffer(-mergeability);
-                               else if (cell->type == ID($_DFF_P_))
                                        write_r_buffer(mergeability);
+                               else if (cell->type == ID($_DFF_P_))
+                                       write_r_buffer(mergeability+1);
                                else log_abort();
 
                                SigBit Q = sigmap(cell->getPort(ID::Q));

diff --git a/frontends/aiger/aigerparse.cc b/frontends/aiger/aigerparse.cc
index ed3a926c672ed0d386065432b9927ce4ef0001f0..16e94c3944291d9976d73faab9ae268c0da2d974 100644 (file)
--- a/frontends/aiger/aigerparse.cc
+++ b/frontends/aiger/aigerparse.cc
@@ -789,13 +789,12 @@ void AigerReader::post_process()
 
                Cell* ff;
                int clock_index = mergeability[i];
-               if (clock_index < 0) {
+               if (clock_index & 1) {
                        ff = module->addCell(NEW_ID, ID($_DFF_N_));
-                       clock_index = -clock_index;
+                       clock_index--;
                }
-               else if (clock_index > 0)
+               else
                        ff = module->addCell(NEW_ID, ID($_DFF_P_));
-               else log_abort();
                auto r = mergeability_to_clock.insert(clock_index);
                if (r.second)
                        r.first->second = module->addWire(NEW_ID);