xaiger: when -dff use (* init *) for initial state

diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc
index 2e2ca70188bf0e356c36c82e0f11a7329b0200d8..5d15df310ff5362374357ab2fc6654b09fe960b0 100644 (file)
--- a/backends/aiger/xaiger.cc
+++ b/backends/aiger/xaiger.cc
@@ -79,6 +79,7 @@ struct XAigerWriter
        Module *module;
        SigMap sigmap;
 
+       dict<SigBit, State> init_map;
        pool<SigBit> input_bits, output_bits;
        dict<SigBit, SigBit> not_map, alias_map;
        dict<SigBit, pair<SigBit, SigBit>> and_map;
@@ -157,7 +158,8 @@ struct XAigerWriter
                        if (wire->get_bool_attribute(ID::keep))
                                sigmap.add(wire);
 
-               for (auto wire : module->wires())
+               for (auto wire : module->wires()) {
+                       auto it = wire->attributes.find(ID::init);
                        for (int i = 0; i < GetSize(wire); i++)
                        {
                                SigBit wirebit(wire, i);
@@ -184,7 +186,17 @@ struct XAigerWriter
                                                alias_map[wirebit] = bit;
                                        output_bits.insert(wirebit);
                                }
+
+                               if (it != wire->attributes.end()) {
+                                       auto s = it->second[i];
+                                       if (s != State::Sx) {
+                                               auto r = init_map.insert(std::make_pair(bit, it->second[i]));
+                                               if (!r.second && r.first->second != it->second[i])
+                                                       log_error("Bit '%s' has a conflicting (* init *) value.\n", log_signal(bit));
+                                       }
+                               }
                        }
+               }
 
                TimingInfo timing;
 
@@ -632,8 +644,8 @@ struct XAigerWriter
                                        write_r_buffer(mergeability);
                                else log_abort();
 
-                               Const init = cell->attributes.at(ID::abc9_init);
-                               log_assert(GetSize(init) == 1);
+                               SigBit Q = sigmap(cell->getPort(ID::Q));
+                               State init = init_map.at(Q, State::Sx);
                                if (init == State::S1)
                                        write_s_buffer(1);
                                else if (init == State::S0)