write_xaiger: add support and test for (* keep *) on wires

diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc
index 0c08645d06ff50c7739a193c64cbb5e77d5f9268..2a0f5c7e4efc3f518492de8dfe040b76ddafaf60 100644 (file)
--- a/backends/aiger/xaiger.cc
+++ b/backends/aiger/xaiger.cc
@@ -156,7 +156,6 @@ struct XAigerWriter
                        if (wire->get_bool_attribute(ID::keep))
                                sigmap.add(wire);
 
-
                for (auto wire : module->wires())
                        for (int i = 0; i < GetSize(wire); i++)
                        {
@@ -174,10 +173,11 @@ struct XAigerWriter
                                undriven_bits.insert(bit);
                                unused_bits.insert(bit);
 
-                               if (wire->port_input)
+                               bool keep = wire->get_bool_attribute(ID::keep);
+                               if (wire->port_input || keep)
                                        input_bits.insert(bit);
 
-                               if (wire->port_output) {
+                               if (wire->port_output || keep) {
                                        if (bit != wirebit)
                                                alias_map[wirebit] = bit;
                                        output_bits.insert(wirebit);
@@ -209,9 +209,9 @@ struct XAigerWriter
                        }
 
                        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"))
+                                       // The presence of an abc9_mergeability attribute indicates
+                                       //   that we do want to pass this flop to ABC
+                                       cell->attributes.count("\\abc9_mergeability"))
                        {
                                SigBit D = sigmap(cell->getPort("\\D").as_bit());
                                SigBit Q = sigmap(cell->getPort("\\Q").as_bit());
@@ -430,7 +430,17 @@ struct XAigerWriter
 
                for (const auto &bit : output_bits) {
                        ordered_outputs[bit] = aig_o++;
-                       aig_outputs.push_back(bit2aig(bit));
+                       int aig;
+                       if (input_bits.count(bit)) {
+                               auto it = aig_map.find(bit);
+                               int input_aig = it->second;
+                               aig_map.erase(it);
+                               aig = bit2aig(bit);
+                               aig_map.at(bit) = input_aig;
+                       }
+                       else
+                               aig = bit2aig(bit);
+                       aig_outputs.push_back(aig);
                }
 
                for (auto &i : ff_bits) {

diff --git a/tests/techmap/abc9.ys b/tests/techmap/abc9.ys
index 20f263da83d6ca5526864e318d30ab481850ab73..46b6f08d2e712a41c7e7f0d289d58932420e8548 100644 (file)
--- a/tests/techmap/abc9.ys
+++ b/tests/techmap/abc9.ys
@@ -38,3 +38,16 @@ abc9 -lut 4
 design -load gold
 scratchpad -copy abc9.script.flow3 abc9.script
 abc9 -lut 4
+
+design -reset
+read_verilog <<EOT
+module top(input a, b, output o);
+(* keep *) wire w = a & b;
+assign o = ~w;
+endmodule
+EOT
+
+simplemap
+equiv_opt -assert abc9 -lut 4
+design -load postopt
+select -assert-count 2 t:$lut