From cb7dbf4070a7ca3658b7e473cb54f2eafb6c9ae3 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 7 Sep 2016 12:42:16 +0200 Subject: [PATCH] Improvements in assertpmux --- examples/smtbmc/.gitignore | 2 + examples/smtbmc/Makefile | 11 ++- examples/smtbmc/demo6.v | 14 +++ kernel/rtlil.cc | 16 ++++ kernel/rtlil.h | 3 + passes/sat/assertpmux.cc | 179 ++++++++++++++++++++++++++++++++----- 6 files changed, 202 insertions(+), 23 deletions(-) create mode 100644 examples/smtbmc/demo6.v diff --git a/examples/smtbmc/.gitignore b/examples/smtbmc/.gitignore index 88d264c63..ba7a1c9c6 100644 --- 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 a2d4f444b..4fb0848f5 100644 --- 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 index 000000000..62a72e2a8 --- /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 41b4b93f0..32efe4f0d 100644 --- 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 c235585f7..a426e0bdd 100644 --- 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 3c8928db5..63a907671 100644 --- 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_muxusers; - SigSpec sel = pmux->getPort("\\S"); - SigSpec cnt(State::S0, cntbits); + dict sigbit_actsignals; + dict sigspec_actsignals; + dict, 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; + } - SigSpec assert_a = module->Le(NEW_ID, cnt, SigSpec(1, cntbits)); - SigSpec assert_en = 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; - 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); + 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 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; + } + } + } } - Cell *assert_cell = module->addAssert(NEW_ID, assert_a, assert_en); + SigBit get_bit_activation(SigBit bit) + { + sigmap.apply(bit); - if (pmux->attributes.count("\\src") != 0) - assert_cell->attributes["\\src"] = pmux->attributes.at("\\src"); -} + 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 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)); + + output.sort_and_unify(); + + 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); + } + + 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); + + 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 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 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); } }