Added $assert/$assume support to AIGER back-end

diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc
index 9dd3a94c7659d08e98a76068d0a6d2240ade17fc..aefe5cf435e6ea215b91740fba2ed82f4d7387ab 100644 (file)
--- a/backends/aiger/aiger.cc
+++ b/backends/aiger/aiger.cc
@@ -45,11 +45,12 @@ struct AigerWriter
        pool<SigBit> input_bits, output_bits;
        dict<SigBit, SigBit> not_map, ff_map;
        dict<SigBit, pair<SigBit, SigBit>> and_map;
+       vector<pair<SigBit, SigBit>> asserts, assumes;
        pool<SigBit> initstate_bits;
 
        vector<pair<int, int>> aig_gates;
        vector<int> aig_latchin, aig_latchinit, aig_outputs;
-       int aig_m = 0, aig_i = 0, aig_l = 0, aig_o = 0, aig_a = 0;
+       int aig_m = 0, aig_i = 0, aig_l = 0, aig_o = 0, aig_a = 0, aig_b = 0, aig_c = 0;
 
        dict<SigBit, int> aig_map;
        dict<SigBit, int> ordered_outputs;
@@ -146,6 +147,22 @@ struct AigerWriter
                                continue;
                        }
 
+                       if (cell->type == "$assert")
+                       {
+                               SigBit A = sigmap(cell->getPort("\\A").as_bit());
+                               SigBit EN = sigmap(cell->getPort("\\EN").as_bit());
+                               asserts.push_back(make_pair(A, EN));
+                               continue;
+                       }
+
+                       if (cell->type == "$assume")
+                       {
+                               SigBit A = sigmap(cell->getPort("\\A").as_bit());
+                               SigBit EN = sigmap(cell->getPort("\\EN").as_bit());
+                               assumes.push_back(make_pair(A, EN));
+                               continue;
+                       }
+
                        log_error("Unsupported cell type: %s (%s)\n", log_id(cell->type), log_id(cell));
                }
 
@@ -225,6 +242,20 @@ struct AigerWriter
                        ordered_outputs[bit] = aig_o-1;
                        aig_outputs.push_back(bit2aig(bit));
                }
+
+               for (auto it : asserts) {
+                       aig_b++;
+                       int bit_a = bit2aig(it.first);
+                       int bit_en = bit2aig(it.second);
+                       aig_outputs.push_back(mkgate(bit_a^1, bit_en));
+               }
+
+               for (auto it : assumes) {
+                       aig_c++;
+                       int bit_a = bit2aig(it.first);
+                       int bit_en = bit2aig(it.second);
+                       aig_outputs.push_back(mkgate(bit_a^1, bit_en)^1);
+               }
        }
 
        void write_aiger(std::ostream &f, bool ascii_mode, bool miter_mode, bool symbols_mode)
@@ -232,12 +263,18 @@ struct AigerWriter
                log_assert(aig_m == aig_i + aig_l + aig_a);
                log_assert(aig_l == GetSize(aig_latchin));
                log_assert(aig_l == GetSize(aig_latchinit));
-               log_assert(aig_o == GetSize(aig_outputs));
-
-               if (miter_mode)
-                       f << stringf("%s %d %d %d 0 %d %d\n", ascii_mode ? "aag" : "aig", aig_m, aig_i, aig_l,  aig_a, aig_o);
-               else
-                       f << stringf("%s %d %d %d %d %d\n", ascii_mode ? "aag" : "aig", aig_m, aig_i, aig_l, aig_o, aig_a);
+               log_assert((aig_o + aig_b + aig_c) == GetSize(aig_outputs));
+
+               if (miter_mode) {
+                       if (aig_b || aig_c)
+                               log_error("Running AIGER back-end in -miter mode, but design contains $assert and/or $assume cells!\n");
+                       f << stringf("%s %d %d %d 0 %d %d\n", ascii_mode ? "aag" : "aig", aig_m, aig_i, aig_l, aig_a, aig_o);
+               } else {
+                       f << stringf("%s %d %d %d %d %d", ascii_mode ? "aag" : "aig", aig_m, aig_i, aig_l, aig_o, aig_a);
+                       if (aig_b || aig_c)
+                               f << stringf(" %d %d", aig_b, aig_c);
+                       f << stringf("\n");
+               }
 
                if (ascii_mode)
                {
@@ -253,7 +290,7 @@ struct AigerWriter
                                        f << stringf("%d %d %d\n", 2*(aig_i+i)+2, aig_latchin.at(i), 2*(aig_i+i)+2);
                        }
 
-                       for (int i = 0; i < aig_o; i++)
+                       for (int i = 0; i < aig_o + aig_b + aig_c; i++)
                                f << stringf("%d\n", aig_outputs.at(i));
 
                        for (int i = 0; i < aig_a; i++)
@@ -270,7 +307,7 @@ struct AigerWriter
                                        f << stringf("%d %d\n", aig_latchin.at(i), 2*(aig_i+i)+2);
                        }
 
-                       for (int i = 0; i < aig_o; i++)
+                       for (int i = 0; i < aig_o + aig_b + aig_c; i++)
                                f << stringf("%d\n", aig_outputs.at(i));
 
                        for (int i = 0; i < aig_a; i++) {
@@ -418,7 +455,11 @@ struct AigerBackend : public Backend {
                log("    write_aiger [options] [filename]\n");
                log("\n");
                log("Write the current design to an AIGER file. The design must be flattened and\n");
-               log("must not contain any cell types except $_AND_, $_NOT_, and simple FF types.\n");
+               log("must not contain any cell types except $_AND_, $_NOT_, simple FF types,\n");
+               log("$assert and $assume cells, and $initstate cells.\n");
+               log("\n");
+               log("$assert and $assume cells are converted to AIGER bad state properties and\n");
+               log("invariant constraints.\n");
                log("\n");
                log("    -ascii\n");
                log("        write ASCII version of AGIER format\n");

diff --git a/examples/aiger/demo.sh b/examples/aiger/demo.sh
index caaa447619e826c4834efab1c9d191a36d439d51..8728b6722a1bdd6e6e27b1363179075e11f7a02d 100644 (file)
--- a/examples/aiger/demo.sh
+++ b/examples/aiger/demo.sh
@@ -4,11 +4,11 @@ yosys -p '
        read_verilog -formal demo.v
        prep -flatten -nordff -top demo
        write_smt2 -wires demo.smt2
-       miter -assert demo
+       flatten demo; delete -output
        memory_map; opt -full
        techmap; opt -fast
        abc -fast -g AND; opt_clean
-       write_aiger -miter -zinit -map demo.aim demo.aig
+       write_aiger -map demo.aim demo.aig
 '
 super_prove demo.aig > demo.aiw
 yosys-smtbmc --dump-vcd demo.vcd --aig demo demo.smt2

diff --git a/examples/aiger/demo.v b/examples/aiger/demo.v
index bb54ba4ef86530db71df43d2f7e369224881e0b9..b98287424ea2e73e0793cc254f86f1cc10de03d4 100644 (file)
--- a/examples/aiger/demo.v
+++ b/examples/aiger/demo.v
@@ -4,7 +4,7 @@ module demo(input clk, reset, ctrl);
   initial counter[NBITS-2] = 0;
   initial counter[0] = 1;
   always @(posedge clk) begin
-    counter <= reset ? 0 : ctrl ? counter + 1 : counter - 1;
+    counter <= reset ? 1 : ctrl ? counter + 1 : counter - 1;
     assume(counter != 0);
     assume(counter != 1 << (NBITS-1));
     assert(counter != (1 << NBITS)-1);