xaiger: cleanup
[yosys.git] / backends / aiger / xaiger.cc
index 9b2bab95ca9e85028375c0ef8709a3b04deca8d8..cd63236e9a9add170182e4760e1ec541692e168d 100644 (file)
@@ -47,6 +47,7 @@ inline static uint32_t bswap32(uint32_t x)
 #include "kernel/yosys.h"
 #include "kernel/sigtools.h"
 #include "kernel/utils.h"
+#include "kernel/timinginfo.h"
 
 USING_YOSYS_NAMESPACE
 PRIVATE_NAMESPACE_BEGIN
@@ -75,14 +76,16 @@ void aiger_encode(std::ostream &f, int x)
 
 struct XAigerWriter
 {
+       Design *design;
        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;
        vector<SigBit> ci_bits, co_bits;
-       dict<SigBit, Cell*> ff_bits;
+       vector<Cell*> ff_list;
        dict<SigBit, float> arrival_times;
 
        vector<pair<int, int>> aig_gates;
@@ -136,7 +139,7 @@ struct XAigerWriter
                return a;
        }
 
-       XAigerWriter(Module *module, bool holes_mode=false) : module(module), sigmap(module)
+       XAigerWriter(Module *module, bool dff_mode) : design(module->design), module(module), sigmap(module)
        {
                pool<SigBit> undriven_bits;
                pool<SigBit> unused_bits;
@@ -156,7 +159,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);
@@ -173,36 +177,47 @@ struct XAigerWriter
                                undriven_bits.insert(bit);
                                unused_bits.insert(bit);
 
-                               bool keep = wire->get_bool_attribute(ID::keep);
+                               bool keep = wire->get_bool_attribute(ID::abc9_keep);
                                if (wire->port_input || keep)
                                        input_bits.insert(bit);
 
+                               keep = keep || wire->get_bool_attribute(ID::keep);
                                if (wire->port_output || keep) {
                                        if (bit != wirebit)
                                                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;
 
-               dict<IdString,dict<IdString,std::vector<int>>> arrivals_cache;
                for (auto cell : module->cells()) {
-                       RTLIL::Module* inst_module = module->design->module(cell->type);
                        if (!cell->has_keep_attr()) {
-                               if (cell->type == "$_NOT_")
+                               if (cell->type == ID($_NOT_))
                                {
-                                       SigBit A = sigmap(cell->getPort("\\A").as_bit());
-                                       SigBit Y = sigmap(cell->getPort("\\Y").as_bit());
+                                       SigBit A = sigmap(cell->getPort(ID::A).as_bit());
+                                       SigBit Y = sigmap(cell->getPort(ID::Y).as_bit());
                                        unused_bits.erase(A);
                                        undriven_bits.erase(Y);
                                        not_map[Y] = A;
                                        continue;
                                }
 
-                               if (cell->type == "$_AND_")
+                               if (cell->type == ID($_AND_))
                                {
-                                       SigBit A = sigmap(cell->getPort("\\A").as_bit());
-                                       SigBit B = sigmap(cell->getPort("\\B").as_bit());
-                                       SigBit Y = sigmap(cell->getPort("\\Y").as_bit());
+                                       SigBit A = sigmap(cell->getPort(ID::A).as_bit());
+                                       SigBit B = sigmap(cell->getPort(ID::B).as_bit());
+                                       SigBit Y = sigmap(cell->getPort(ID::Y).as_bit());
                                        unused_bits.erase(A);
                                        unused_bits.erase(B);
                                        undriven_bits.erase(Y);
@@ -210,81 +225,67 @@ struct XAigerWriter
                                        continue;
                                }
 
-                               if (cell->type == "$__ABC9_FF_" &&
-                                               // The presence of an abc9_mergeability attribute indicates
-                                               //   that we do want to pass this flop to ABC
-                                               cell->attributes.count("\\abc9_mergeability"))
+                               if (dff_mode && cell->type.in(ID($_DFF_N_), ID($_DFF_P_)) && !cell->get_bool_attribute(ID::abc9_keep))
                                {
-                                       SigBit D = sigmap(cell->getPort("\\D").as_bit());
-                                       SigBit Q = sigmap(cell->getPort("\\Q").as_bit());
+                                       SigBit D = sigmap(cell->getPort(ID::D).as_bit());
+                                       SigBit Q = sigmap(cell->getPort(ID::Q).as_bit());
                                        unused_bits.erase(D);
                                        undriven_bits.erase(Q);
                                        alias_map[Q] = D;
-                                       auto r YS_ATTRIBUTE(unused) = ff_bits.insert(std::make_pair(D, cell));
-                                       log_assert(r.second);
-                                       if (input_bits.erase(Q))
-                                               log_assert(Q.wire->attributes.count(ID::keep));
+                                       ff_list.emplace_back(cell);
                                        continue;
                                }
 
-                               if (inst_module) {
-                                       bool abc9_flop = false;
-                                       auto it = cell->attributes.find("\\abc9_box_seq");
-                                       if (it != cell->attributes.end()) {
-                                               int abc9_box_seq = it->second.as_int();
-                                               if (GetSize(box_list) <= abc9_box_seq)
-                                                       box_list.resize(abc9_box_seq+1);
-                                               box_list[abc9_box_seq] = cell;
-                                               // Only flop boxes may have arrival times
-                                               //   (all others are combinatorial)
-                                               abc9_flop = inst_module->get_bool_attribute("\\abc9_flop");
-                                               if (!abc9_flop)
-                                                       continue;
-                                       }
+                               if (cell->type.in(ID($specify2), ID($specify3), ID($specrule)))
+                                       continue;
+                       }
 
-                                       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;
+                       RTLIL::Module* inst_module = design->module(cell->type);
+                       if (inst_module && inst_module->get_blackbox_attribute()) {
+                               bool abc9_flop = false;
+
+                               auto it = cell->attributes.find(ID::abc9_box_seq);
+                               if (it != cell->attributes.end()) {
+                                       log_assert(!cell->has_keep_attr());
+                                       log_assert(cell->parameters.empty());
+                                       int abc9_box_seq = it->second.as_int();
+                                       if (GetSize(box_list) <= abc9_box_seq)
+                                               box_list.resize(abc9_box_seq+1);
+                                       box_list[abc9_box_seq] = cell;
+                                       // Only flop boxes may have arrival times
+                                       //   (all others are combinatorial)
+                                       log_assert(cell->parameters.empty());
+                                       abc9_flop = inst_module->get_bool_attribute(ID::abc9_flop);
+                                       if (!abc9_flop)
+                                               continue;
+                               }
 
-                                               auto r = cell_arrivals.insert(conn.first);
-                                               auto &arrivals = r.first->second;
-                                               if (r.second) {
-                                                       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 (!timing.count(inst_module->name))
+                                       timing.setup_module(inst_module);
+                               auto &t = timing.at(inst_module->name).arrival;
+                               for (const auto &conn : cell->connections()) {
+                                       auto port_wire = inst_module->wire(conn.first);
+                                       if (!port_wire->port_output)
+                                               continue;
 
-                                               if (arrivals.empty())
+                                       for (int i = 0; i < GetSize(conn.second); i++) {
+                                               auto d = t.at(TimingInfo::NameBit(conn.first,i), 0);
+                                               if (d == 0)
                                                        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);
+                                                       static std::set<std::tuple<IdString,IdString,int>> seen;
+                                                       if (seen.emplace(inst_module->name, conn.first, i).second) log("%s.%s[%d] abc9_arrival = %d\n",
+                                                                       log_id(cell->type), log_id(conn.first), i, d);
                                                }
 #endif
-                                               for (auto bit : sigmap(conn.second)) {
-                                                       arrival_times[bit] = *jt;
-                                                       if (arrivals.size() > 1)
-                                                               jt++;
-                                               }
+                                               arrival_times[conn.second[i]] = d;
                                        }
-
-                                       if (abc9_flop)
-                                               continue;
                                }
+
+                               if (abc9_flop)
+                                       continue;
                        }
 
                        bool cell_known = inst_module || cell->known();
@@ -319,9 +320,9 @@ struct XAigerWriter
                for (auto cell : box_list) {
                        log_assert(cell);
 
-                       RTLIL::Module* box_module = module->design->module(cell->type);
+                       RTLIL::Module* box_module = design->module(cell->type);
                        log_assert(box_module);
-                       log_assert(box_module->attributes.count("\\abc9_box_id") || box_module->get_bool_attribute("\\abc9_flop"));
+                       log_assert(box_module->has_attribute(ID::abc9_box_id));
 
                        auto r = box_ports.insert(cell->type);
                        if (r.second) {
@@ -331,7 +332,7 @@ struct XAigerWriter
                                for (const auto &port_name : box_module->ports) {
                                        auto w = box_module->wire(port_name);
                                        log_assert(w);
-                                       if (w->get_bool_attribute("\\abc9_carry")) {
+                                       if (w->get_bool_attribute(ID::abc9_carry)) {
                                                if (w->port_input) {
                                                        if (carry_in != IdString())
                                                                log_error("Module '%s' contains more than one 'abc9_carry' input port.\n", log_id(box_module));
@@ -383,33 +384,7 @@ struct XAigerWriter
                                                        alias_map[O] = b;
                                                ci_bits.emplace_back(b);
                                                undriven_bits.erase(O);
-                                               // If PI and CI, then must be a (* keep *) wire
-                                               if (input_bits.erase(O)) {
-                                                       log_assert(output_bits.count(O));
-                                                       log_assert(O.wire->get_bool_attribute(ID::keep));
-                                               }
-                                       }
-                       }
-
-                       // Connect <cell>.abc9_ff.Q (inserted by abc9_map.v) as the last input to the flop box
-                       if (box_module->get_bool_attribute("\\abc9_flop")) {
-                               SigSpec rhs = module->wire(stringf("%s.abc9_ff.Q", cell->name.c_str()));
-                               if (rhs.empty())
-                                       log_error("'%s.abc9_ff.Q' is not a wire present in module '%s'.\n", log_id(cell), log_id(module));
-
-                               for (auto b : rhs) {
-                                       SigBit I = sigmap(b);
-                                       if (b == RTLIL::Sx)
-                                               b = State::S0;
-                                       else if (I != b) {
-                                               if (I == RTLIL::Sx)
-                                                       alias_map[b] = State::S0;
-                                               else
-                                                       alias_map[b] = I;
                                        }
-                                       co_bits.emplace_back(b);
-                                       unused_bits.erase(I);
-                               }
                        }
                }
 
@@ -426,16 +401,14 @@ struct XAigerWriter
                        undriven_bits.erase(bit);
                }
 
-               if (holes_mode) {
-                       struct sort_by_port_id {
-                               bool operator()(const RTLIL::SigBit& a, const RTLIL::SigBit& b) const {
-                                       return a.wire->port_id < b.wire->port_id ||
-                                           (a.wire->port_id == b.wire->port_id && a.offset < b.offset);
-                               }
-                       };
-                       input_bits.sort(sort_by_port_id());
-                       output_bits.sort(sort_by_port_id());
-               }
+               struct sort_by_port_id {
+                       bool operator()(const RTLIL::SigBit& a, const RTLIL::SigBit& b) const {
+                               return a.wire->port_id < b.wire->port_id ||
+                                   (a.wire->port_id == b.wire->port_id && a.offset < b.offset);
+                       }
+               };
+               input_bits.sort(sort_by_port_id());
+               output_bits.sort(sort_by_port_id());
 
                aig_map[State::S0] = 0;
                aig_map[State::S1] = 1;
@@ -446,9 +419,8 @@ struct XAigerWriter
                        aig_map[bit] = 2*aig_m;
                }
 
-               for (const auto &i : ff_bits) {
-                       const Cell *cell = i.second;
-                       const SigBit &q = sigmap(cell->getPort("\\Q"));
+               for (auto cell : ff_list) {
+                       const SigBit &q = sigmap(cell->getPort(ID::Q));
                        aig_m++, aig_i++;
                        log_assert(!aig_map.count(q));
                        aig_map[q] = 2*aig_m;
@@ -472,8 +444,8 @@ struct XAigerWriter
                for (const auto &bit : output_bits) {
                        ordered_outputs[bit] = aig_o++;
                        int aig;
-                       // Unlike bit2aig() which checks aig_map first, for
-                       //   inout/keep bits, since aig_map will point to
+                       // Unlike bit2aig() which checks aig_map first for
+                       //   inout/scc bits, since aig_map will point to
                        //   the PI, first attempt to find the NOT/AND driver
                        //   before resorting to an aig_map lookup (which
                        //   could be another PO)
@@ -494,8 +466,8 @@ struct XAigerWriter
                        aig_outputs.push_back(aig);
                }
 
-               for (auto &i : ff_bits) {
-                       const SigBit &d = i.first;
+               for (auto cell : ff_list) {
+                       const SigBit &d = sigmap(cell->getPort(ID::D));
                        aig_o++;
                        aig_outputs.push_back(aig_map.at(d));
                }
@@ -567,16 +539,16 @@ struct XAigerWriter
                std::stringstream h_buffer;
                auto write_h_buffer = std::bind(write_buffer, std::ref(h_buffer), std::placeholders::_1);
                write_h_buffer(1);
-               log_debug("ciNum = %d\n", GetSize(input_bits) + GetSize(ff_bits) + GetSize(ci_bits));
-               write_h_buffer(input_bits.size() + ff_bits.size() + ci_bits.size());
-               log_debug("coNum = %d\n", GetSize(output_bits) + GetSize(ff_bits) + GetSize(co_bits));
-               write_h_buffer(output_bits.size() + GetSize(ff_bits) + GetSize(co_bits));
-               log_debug("piNum = %d\n", GetSize(input_bits) + GetSize(ff_bits));
-               write_h_buffer(input_bits.size() + ff_bits.size());
-               log_debug("poNum = %d\n", GetSize(output_bits) + GetSize(ff_bits));
-               write_h_buffer(output_bits.size() + ff_bits.size());
+               log_debug("ciNum = %d\n", GetSize(input_bits) + GetSize(ff_list) + GetSize(ci_bits));
+               write_h_buffer(GetSize(input_bits) + GetSize(ff_list) + GetSize(ci_bits));
+               log_debug("coNum = %d\n", GetSize(output_bits) + GetSize(ff_list) + GetSize(co_bits));
+               write_h_buffer(GetSize(output_bits) + GetSize(ff_list) + GetSize(co_bits));
+               log_debug("piNum = %d\n", GetSize(input_bits) + GetSize(ff_list));
+               write_h_buffer(GetSize(input_bits) + GetSize(ff_list));
+               log_debug("poNum = %d\n", GetSize(output_bits) + GetSize(ff_list));
+               write_h_buffer(GetSize(output_bits) + GetSize(ff_list));
                log_debug("boxNum = %d\n", GetSize(box_list));
-               write_h_buffer(box_list.size());
+               write_h_buffer(GetSize(box_list));
 
                auto write_buffer_float = [](std::stringstream &buffer, float f32) {
                        buffer.write(reinterpret_cast<const char*>(&f32), sizeof(f32));
@@ -590,23 +562,20 @@ struct XAigerWriter
                //for (auto bit : output_bits)
                //      write_o_buffer(0);
 
-               if (!box_list.empty() || !ff_bits.empty()) {
+               if (!box_list.empty() || !ff_list.empty()) {
                        dict<IdString, std::tuple<int,int,int>> cell_cache;
 
                        int box_count = 0;
                        for (auto cell : box_list) {
                                log_assert(cell);
+                               log_assert(cell->parameters.empty());
 
-                               RTLIL::Module* box_module = module->design->module(cell->type);
-                               log_assert(box_module);
-
-                               IdString derived_type = box_module->derive(box_module->design, cell->parameters);
-                               box_module = box_module->design->module(derived_type);
-                               log_assert(box_module);
-
-                               auto r = cell_cache.insert(derived_type);
+                               auto r = cell_cache.insert(cell->type);
                                auto &v = r.first->second;
                                if (r.second) {
+                                       RTLIL::Module* box_module = design->module(cell->type);
+                                       log_assert(box_module);
+
                                        int box_inputs = 0, box_outputs = 0;
                                        for (auto port_name : box_module->ports) {
                                                RTLIL::Wire *w = box_module->wire(port_name);
@@ -617,14 +586,9 @@ struct XAigerWriter
                                                        box_outputs += GetSize(w);
                                        }
 
-                                       // For flops only, create an extra 1-bit input that drives a new wire
-                                       //   called "<cell>.abc9_ff.Q" that is used below
-                                       if (box_module->get_bool_attribute("\\abc9_flop"))
-                                               box_inputs++;
-
                                        std::get<0>(v) = box_inputs;
                                        std::get<1>(v) = box_outputs;
-                                       std::get<2>(v) = box_module->attributes.at("\\abc9_box_id").as_int();
+                                       std::get<2>(v) = box_module->attributes.at(ID::abc9_box_id).as_int();
                                }
 
                                write_h_buffer(std::get<0>(v));
@@ -635,36 +599,37 @@ struct XAigerWriter
 
                        std::stringstream r_buffer;
                        auto write_r_buffer = std::bind(write_buffer, std::ref(r_buffer), std::placeholders::_1);
-                       log_debug("flopNum = %d\n", GetSize(ff_bits));
-                       write_r_buffer(ff_bits.size());
+                       log_debug("flopNum = %d\n", GetSize(ff_list));
+                       write_r_buffer(ff_list.size());
 
                        std::stringstream s_buffer;
                        auto write_s_buffer = std::bind(write_buffer, std::ref(s_buffer), std::placeholders::_1);
-                       write_s_buffer(ff_bits.size());
+                       write_s_buffer(ff_list.size());
 
-                       for (const auto &i : ff_bits) {
-                               const Cell *cell = i.second;
+                       dict<SigSpec, int> clk_to_mergeability;
+                       for (const auto cell : ff_list) {
+                               const SigBit &d = sigmap(cell->getPort(ID::D));
+                               const SigBit &q = sigmap(cell->getPort(ID::Q));
 
-                               int mergeability = cell->attributes.at(ID(abc9_mergeability)).as_int();
+                               SigSpec clk_and_pol{sigmap(cell->getPort(ID::C)), cell->type[6] == 'P' ? State::S1 : State::S0};
+                               auto r = clk_to_mergeability.insert(std::make_pair(clk_and_pol, clk_to_mergeability.size()+1));
+                               int mergeability = r.first->second;
                                log_assert(mergeability > 0);
                                write_r_buffer(mergeability);
 
-                               Const init = cell->attributes.at(ID(abc9_init), State::Sx);
-                               log_assert(GetSize(init) == 1);
+                               State init = init_map.at(q, State::Sx);
+                               log_debug("Cell '%s' (type %s) has (* init *) value '%s'.\n", log_id(cell), log_id(cell->type), log_signal(init));
                                if (init == State::S1)
                                        write_s_buffer(1);
                                else if (init == State::S0)
                                        write_s_buffer(0);
                                else {
                                        log_assert(init == State::Sx);
-                                       write_s_buffer(0);
+                                       write_s_buffer(2);
                                }
 
-                               auto it = cell->attributes.find(ID(abc9_arrival));
-                               if (it != cell->attributes.end())
-                                       write_i_buffer(it->second.as_int());
-                               else
-                                       write_i_buffer(0);
+                               // Use arrival time from output of flop box
+                               write_i_buffer(arrival_times.at(d, 0));
                                //write_o_buffer(0);
                        }
 
@@ -680,10 +645,16 @@ struct XAigerWriter
                        f.write(reinterpret_cast<const char*>(&buffer_size_be), sizeof(buffer_size_be));
                        f.write(buffer_str.data(), buffer_str.size());
 
-                       RTLIL::Module *holes_module = module->design->module(stringf("%s$holes", module->name.c_str()));
+                       RTLIL::Design *holes_design;
+                       auto it = saved_designs.find("$abc9_holes");
+                       if (it != saved_designs.end())
+                               holes_design = it->second;
+                       else
+                               holes_design = nullptr;
+                       RTLIL::Module *holes_module = holes_design ? holes_design->module(module->name) : nullptr;
                        if (holes_module) {
                                std::stringstream a_buffer;
-                               XAigerWriter writer(holes_module, true /* holes_mode */);
+                               XAigerWriter writer(holes_module, false /* dff_mode */);
                                writer.write_aiger(a_buffer, false /*ascii_mode*/);
 
                                f << "a";
@@ -713,10 +684,10 @@ struct XAigerWriter
 
                f << stringf("Generated by %s\n", yosys_version_str);
 
-               module->design->scratchpad_set_int("write_xaiger.num_ands", and_map.size());
-               module->design->scratchpad_set_int("write_xaiger.num_wires", aig_map.size());
-               module->design->scratchpad_set_int("write_xaiger.num_inputs", input_bits.size());
-               module->design->scratchpad_set_int("write_xaiger.num_outputs", output_bits.size());
+               design->scratchpad_set_int("write_xaiger.num_ands", and_map.size());
+               design->scratchpad_set_int("write_xaiger.num_wires", aig_map.size());
+               design->scratchpad_set_int("write_xaiger.num_inputs", input_bits.size());
+               design->scratchpad_set_int("write_xaiger.num_outputs", output_bits.size());
        }
 
        void write_map(std::ostream &f)
@@ -726,22 +697,18 @@ struct XAigerWriter
 
                for (auto wire : module->wires())
                {
-                       SigSpec sig = sigmap(wire);
-
                        for (int i = 0; i < GetSize(wire); i++)
                        {
                                RTLIL::SigBit b(wire, i);
                                if (input_bits.count(b)) {
                                        int a = aig_map.at(b);
                                        log_assert((a & 1) == 0);
-                                       input_lines[a] += stringf("input %d %d %s\n", (a >> 1)-1, i, log_id(wire));
+                                       input_lines[a] += stringf("input %d %d %s\n", (a >> 1)-1, wire->start_offset+i, log_id(wire));
                                }
 
                                if (output_bits.count(b)) {
                                        int o = ordered_outputs.at(b);
-                                       int init = 2;
-                                       output_lines[o] += stringf("output %d %d %s %d\n", o - GetSize(co_bits), i, log_id(wire), init);
-                                       continue;
+                                       output_lines[o] += stringf("output %d %d %s\n", o - GetSize(co_bits), wire->start_offset+i, log_id(wire));
                                }
                        }
                }
@@ -771,10 +738,10 @@ struct XAigerBackend : public Backend {
                log("    write_xaiger [options] [filename]\n");
                log("\n");
                log("Write the top module (according to the (* top *) attribute or if only one module\n");
-               log("is currently selected) to an XAIGER file. Any non $_NOT_, $_AND_, $_ABC9_FF_, or");
-               log("non (* abc9_box_id *) cells will be converted into psuedo-inputs and\n");
-               log("pseudo-outputs. Whitebox contents will be taken from the '<module-name>$holes'\n");
-               log("module, if it exists.\n");
+               log("is currently selected) to an XAIGER file. Any non $_NOT_, $_AND_, (optionally\n");
+               log("$_DFF_N_, $_DFF_P_), or non (* abc9_box *) cells will be converted into psuedo-\n");
+               log("inputs and pseudo-outputs. Whitebox contents will be taken from the equivalent\n");
+               log("module in the '$abc9_holes' design, if it exists.\n");
                log("\n");
                log("    -ascii\n");
                log("        write ASCII version of AIGER format\n");
@@ -782,10 +749,13 @@ struct XAigerBackend : public Backend {
                log("    -map <filename>\n");
                log("        write an extra file with port and box symbols\n");
                log("\n");
+               log("    -dff\n");
+               log("        write $_DFF_[NP]_ cells\n");
+               log("\n");
        }
        void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
        {
-               bool ascii_mode = false;
+               bool ascii_mode = false, dff_mode = false;
                std::string map_filename;
 
                log_header(design, "Executing XAIGER backend.\n");
@@ -801,6 +771,10 @@ struct XAigerBackend : public Backend {
                                map_filename = args[++argidx];
                                continue;
                        }
+                       if (args[argidx] == "-dff") {
+                               dff_mode = true;
+                               continue;
+                       }
                        break;
                }
                extra_args(f, filename, args, argidx, !ascii_mode);
@@ -818,7 +792,7 @@ struct XAigerBackend : public Backend {
                if (!top_module->memories.empty())
                        log_error("Found unmapped memories in module %s: unmapped memories are not supported in XAIGER backend!\n", log_id(top_module));
 
-               XAigerWriter writer(top_module);
+               XAigerWriter writer(top_module, dff_mode);
                writer.write_aiger(*f, ascii_mode);
 
                if (!map_filename.empty()) {