Improvements in assertpmux

diff --git a/examples/smtbmc/.gitignore b/examples/smtbmc/.gitignore
index 88d264c63f3d10b700b8da9301153953a0f90156..ba7a1c9c648ceec1b00d2dae6fef385d172b02a1 100644 (file)
--- a/examples/smtbmc/.gitignore
+++ b/examples/smtbmc/.gitignore
@@ -16,3 +16,5 @@ demo4.yslog
 demo5.smt2
 demo5.vcd
 demo5.yslog
+demo6.smt2
+demo6.yslog

diff --git a/examples/smtbmc/Makefile b/examples/smtbmc/Makefile
index a2d4f444b3d0d85b3ae14b2cc63dd3bbb196feaf..4fb0848f59a4a927104d12a11aa1c00062dbb320 100644 (file)
--- a/examples/smtbmc/Makefile
+++ b/examples/smtbmc/Makefile
@@ -1,5 +1,5 @@
 
-all: demo1 demo2 demo3 demo4
+all: demo1 demo2 demo3 demo4 demo5 demo6
 
 demo1: demo1.smt2
        yosys-smtbmc --dump-vcd demo1.vcd demo1.smt2
@@ -19,6 +19,9 @@ demo4: demo4.smt2
 demo5: demo5.smt2
        yosys-smtbmc -g -t 50 --dump-vcd demo5.vcd demo5.smt2
 
+demo6: demo6.smt2
+       yosys-smtbmc -t 1 demo6.smt2
+
 demo1.smt2: demo1.v
        yosys -ql demo1.yslog -p 'read_verilog -formal demo1.v; prep -top demo1 -nordff; write_smt2 -wires demo1.smt2'
 
@@ -34,12 +37,16 @@ demo4.smt2: demo4.v
 demo5.smt2: demo5.v
        yosys -ql demo5.yslog -p 'read_verilog -formal demo5.v; prep -top demo5 -nordff; write_smt2 -wires demo5.smt2'
 
+demo6.smt2: demo6.v
+       yosys -ql demo6.yslog -p 'read_verilog demo6.v; prep -top demo6 -nordff; assertpmux; opt -keepdc -fast; write_smt2 -wires demo6.smt2'
+
 clean:
        rm -f demo1.yslog demo1.smt2 demo1.vcd
        rm -f demo2.yslog demo2.smt2 demo2.vcd demo2.smtc demo2_tb.v demo2_tb demo2_tb.vcd
        rm -f demo3.yslog demo3.smt2 demo3.vcd
        rm -f demo4.yslog demo4.smt2 demo4.vcd
        rm -f demo5.yslog demo5.smt2 demo5.vcd
+       rm -f demo6.yslog demo6.smt2
 
-.PHONY: demo1 demo2 demo3 demo4 demo5 clean
+.PHONY: demo1 demo2 demo3 demo4 demo5 demo6 clean
 

diff --git a/examples/smtbmc/demo6.v b/examples/smtbmc/demo6.v
new file mode 100644 (file)
index 0000000..62a72e2
--- /dev/null
+++ b/examples/smtbmc/demo6.v
@@ -0,0 +1,14 @@
+// Demo for assertpmux
+
+module demo6 (input A, B, C, D, E, output reg Y);
+       always @* begin
+               Y = 0;
+               if (A != B) begin
+                       (* parallel_case *)
+                       case (C)
+                               A: Y = D;
+                               B: Y = E;
+                       endcase
+               end
+       end
+endmodule

diff --git a/kernel/rtlil.cc b/kernel/rtlil.cc
index 41b4b93f06159c0626e95c28b1df115117b3a602..32efe4f0ddb620f4450a0f38e1561d528d3b071c 100644 (file)
--- a/kernel/rtlil.cc
+++ b/kernel/rtlil.cc
@@ -1975,6 +1975,22 @@ RTLIL::Cell* RTLIL::Module::addDlatchsrGate(RTLIL::IdString name, RTLIL::SigSpec
        return cell;
 }
 
+RTLIL::SigSpec RTLIL::Module::Anyconst(RTLIL::IdString name, int width)
+{
+       RTLIL::SigSpec sig = addWire(NEW_ID, width);
+       Cell *cell = addCell(name, "$anyconst");
+       cell->setParam("\\WIDTH", width);
+       cell->setPort("\\Y", sig);
+       return sig;
+}
+
+RTLIL::SigSpec RTLIL::Module::Initstate(RTLIL::IdString name)
+{
+       RTLIL::SigSpec sig = addWire(NEW_ID);
+       Cell *cell = addCell(name, "$initstate");
+       cell->setPort("\\Y", sig);
+       return sig;
+}
 
 RTLIL::Wire::Wire()
 {

diff --git a/kernel/rtlil.h b/kernel/rtlil.h
index c235585f76a66cd997674a2b8ba921de64928f09..a426e0bdddc678b79fcbe052f2c76f50c0c6d324 100644 (file)
--- a/kernel/rtlil.h
+++ b/kernel/rtlil.h
@@ -1103,6 +1103,9 @@ public:
        RTLIL::SigBit Oai3Gate (RTLIL::IdString name, RTLIL::SigBit sig_a, RTLIL::SigBit sig_b, RTLIL::SigBit sig_c);
        RTLIL::SigBit Aoi4Gate (RTLIL::IdString name, RTLIL::SigBit sig_a, RTLIL::SigBit sig_b, RTLIL::SigBit sig_c, RTLIL::SigBit sig_d);
        RTLIL::SigBit Oai4Gate (RTLIL::IdString name, RTLIL::SigBit sig_a, RTLIL::SigBit sig_b, RTLIL::SigBit sig_c, RTLIL::SigBit sig_d);
+
+       RTLIL::SigSpec Anyconst  (RTLIL::IdString name, int width = 1);
+       RTLIL::SigSpec Initstate (RTLIL::IdString name);
 };
 
 struct RTLIL::Wire : public RTLIL::AttrObject

diff --git a/passes/sat/assertpmux.cc b/passes/sat/assertpmux.cc
index 3c8928db5cedf8efa42a44a9b9e9f8592ea482c4..63a907671b0638c9955c891cdf0a06dbcf86a9f9 100644 (file)
--- a/passes/sat/assertpmux.cc
+++ b/passes/sat/assertpmux.cc
@@ -18,40 +18,166 @@
  */
 
 #include "kernel/yosys.h"
+#include "kernel/sigtools.h"
 
 USING_YOSYS_NAMESPACE
 PRIVATE_NAMESPACE_BEGIN
 
-void assertpmux_worker(Cell *pmux, bool flag_noinit)
+struct AssertpmuxWorker
 {
-       Module *module = pmux->module;
+       Module *module;
+       SigMap sigmap;
 
-       log("Adding assert for $pmux cell %s.%s.\n", log_id(module), log_id(pmux));
+       bool flag_noinit;
+       bool flag_always;
 
-       int swidth = pmux->getParam("\\S_WIDTH").as_int();
-       int cntbits = ceil_log2(swidth+1);
+       // get<0> ... mux cell
+       // get<1> ... mux port index
+       // get<2> ... mux bit index
+       dict<SigBit, pool<tuple<Cell*, int, int>>> sigbit_muxusers;
 
-       SigSpec sel = pmux->getPort("\\S");
-       SigSpec cnt(State::S0, cntbits);
+       dict<SigBit, SigBit> sigbit_actsignals;
+       dict<SigSpec, SigBit> sigspec_actsignals;
+       dict<tuple<Cell*, int>, SigBit> muxport_actsignal;
 
-       for (int i = 0; i < swidth; i++)
-               cnt = module->Add(NEW_ID, cnt, sel[i]);
+       AssertpmuxWorker(Module *module, bool flag_noinit, bool flag_always) :
+                       module(module), sigmap(module), flag_noinit(flag_noinit), flag_always(flag_always)
+       {
+               for (auto wire : module->wires())
+               {
+                       if (wire->port_output)
+                               for (auto bit : sigmap(wire))
+                                       sigbit_actsignals[bit] = State::S1;
+               }
+
+               for (auto cell : module->cells())
+               {
+                       if (cell->type.in("$mux", "$pmux"))
+                       {
+                               int width = cell->getParam("\\WIDTH").as_int();
+                               int numports = cell->type == "$mux" ? 2 : cell->getParam("\\S_WIDTH").as_int() + 1;
+
+                               SigSpec sig_a = sigmap(cell->getPort("\\A"));
+                               SigSpec sig_b = sigmap(cell->getPort("\\B"));
+                               SigSpec sig_s = sigmap(cell->getPort("\\S"));
+
+                               for (int i = 0; i < numports; i++) {
+                                       SigSpec bits = i == 0 ? sig_a : sig_b.extract(width*(i-1), width);
+                                       for (int k = 0; k < width; k++) {
+                                               tuple<Cell*, int, int> muxuser(cell, i, k);
+                                               sigbit_muxusers[bits[k]].insert(muxuser);
+                                       }
+                               }
+                       }
+                       else
+                       {
+                               for (auto &conn : cell->connections()) {
+                                       if (!cell->known() || cell->input(conn.first))
+                                               for (auto bit : sigmap(conn.second))
+                                                       sigbit_actsignals[bit] = State::S1;
+                               }
+                       }
+               }
+       }
+
+       SigBit get_bit_activation(SigBit bit)
+       {
+               sigmap.apply(bit);
+
+               if (sigbit_actsignals.count(bit) == 0)
+               {
+                       SigSpec output;
+
+                       for (auto muxuser : sigbit_muxusers.at(bit))
+                       {
+                               Cell *cell = std::get<0>(muxuser);
+                               int portidx = std::get<1>(muxuser);
+                               int bitidx = std::get<2>(muxuser);
+
+                               tuple<Cell*, int> muxport(cell, portidx);
+
+                               if (muxport_actsignal.count(muxport) == 0) {
+                                       if (portidx == 0)
+                                               muxport_actsignal[muxport] = module->LogicNot(NEW_ID, cell->getPort("\\S"));
+                                       else
+                                               muxport_actsignal[muxport] = cell->getPort("\\S")[portidx-1];
+                               }
+
+                               output.append(module->LogicAnd(NEW_ID, muxport_actsignal.at(muxport), get_bit_activation(cell->getPort("\\Y")[bitidx])));
+                       }
+
+                       output.sort_and_unify();
+
+                       if (GetSize(output) == 0)
+                               output = State::S0;
+                       else if (GetSize(output) > 1)
+                               output = module->ReduceOr(NEW_ID, output);
+
+                       sigbit_actsignals[bit] = output.as_bit();
+               }
+
+               return sigbit_actsignals.at(bit);
+       }
+
+       SigBit get_activation(SigSpec sig)
+       {
+               sigmap.apply(sig);
+               sig.sort_and_unify();
+
+               if (sigspec_actsignals.count(sig) == 0)
+               {
+                       SigSpec output;
+
+                       for (auto bit : sig)
+                               output.append(get_bit_activation(bit));
 
-       SigSpec assert_a = module->Le(NEW_ID, cnt, SigSpec(1, cntbits));
-       SigSpec assert_en = State::S1;
+                       output.sort_and_unify();
 
-       if (flag_noinit) {
-               Cell *initstate_cell = module->addCell(NEW_ID, "$initstate");
-               SigSpec initstate_sig = module->addWire(NEW_ID);
-               initstate_cell->setPort("\\Y", initstate_sig);
-               assert_en = module->LogicNot(NEW_ID, initstate_sig);
+                       if (GetSize(output) == 0)
+                               output = State::S0;
+                       else if (GetSize(output) > 1)
+                               output = module->ReduceOr(NEW_ID, output);
+
+                       sigspec_actsignals[sig] = output.as_bit();
+               }
+
+               return sigspec_actsignals.at(sig);
        }
 
-       Cell *assert_cell = module->addAssert(NEW_ID, assert_a, assert_en);
+       void run(Cell *pmux)
+       {
+               log("Adding assert for $pmux cell %s.%s.\n", log_id(module), log_id(pmux));
+
+               int swidth = pmux->getParam("\\S_WIDTH").as_int();
+               int cntbits = ceil_log2(swidth+1);
+
+               SigSpec sel = pmux->getPort("\\S");
+               SigSpec cnt(State::S0, cntbits);
 
-       if (pmux->attributes.count("\\src") != 0)
-               assert_cell->attributes["\\src"] = pmux->attributes.at("\\src");
-}
+               for (int i = 0; i < swidth; i++)
+                       cnt = module->Add(NEW_ID, cnt, sel[i]);
+
+               SigSpec assert_a = module->Le(NEW_ID, cnt, SigSpec(1, cntbits));
+               SigSpec assert_en;
+
+               if (flag_noinit)
+                       assert_en.append(module->LogicNot(NEW_ID, module->Initstate(NEW_ID)));
+
+               if (!flag_always)
+                       assert_en.append(get_activation(pmux->getPort("\\Y")));
+
+               if (GetSize(assert_en) == 0)
+                       assert_en = State::S1;
+
+               if (GetSize(assert_en) == 2)
+                       assert_en = module->LogicAnd(NEW_ID, assert_en[0], assert_en[1]);
+
+               Cell *assert_cell = module->addAssert(NEW_ID, assert_a, assert_en);
+
+               if (pmux->attributes.count("\\src") != 0)
+                       assert_cell->attributes["\\src"] = pmux->attributes.at("\\src");
+       }
+};
 
 struct AssertpmuxPass : public Pass {
        AssertpmuxPass() : Pass("assertpmux", "convert internal signals to module ports") { }
@@ -67,10 +193,16 @@ struct AssertpmuxPass : public Pass {
                log("    -noinit\n");
                log("        do not enforce the pmux condition during the init state\n");
                log("\n");
+               log("    -always\n");
+               log("        usually the $pmux condition is only checked when the $pmux output\n");
+               log("        is used be the mux tree it drives. this option will deactivate this\n");
+               log("        additional constrained and check the $pmux condition always.\n");
+               log("\n");
        }
        virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
        {
                bool flag_noinit = false;
+               bool flag_always = false;
 
                log_header(design, "Executing ASSERTPMUX pass (add asserts for $pmux cells).\n");
 
@@ -81,12 +213,17 @@ struct AssertpmuxPass : public Pass {
                                flag_noinit = true;
                                continue;
                        }
+                       if (args[argidx] == "-always") {
+                               flag_always = true;
+                               continue;
+                       }
                        break;
                }
                extra_args(args, argidx, design);
 
                for (auto module : design->selected_modules())
                {
+                       AssertpmuxWorker worker(module, flag_noinit, flag_always);
                        vector<Cell*> pmux_cells;
 
                        for (auto cell : module->selected_cells())
@@ -94,7 +231,7 @@ struct AssertpmuxPass : public Pass {
                                        pmux_cells.push_back(cell);
 
                        for (auto cell : pmux_cells)
-                               assertpmux_worker(cell, flag_noinit);
+                               worker.run(cell);
                }
 
        }