riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Improvements in assertpmux

This commit is contained in:
Clifford Wolf 2016-09-07 12:42:16 +02:00
parent e2570ffb87
commit cb7dbf4070
6 changed files with 202 additions and 23 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
examples/smtbmc/.gitignore vendored
View File

@ -16,3 +16,5 @@ demo4.yslog
demo5.smt2
demo5.vcd
demo5.yslog
demo6.smt2
demo6.yslog

11
examples/smtbmc/Makefile
View File

@ -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

14
examples/smtbmc/demo6.v Normal file
View File

@ -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

16
kernel/rtlil.cc
View File

@ -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()
{

3
kernel/rtlil.h
View File

@ -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

179
passes/sat/assertpmux.cc
View File

@ -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;
}
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<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;
}
}
}
}
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<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));
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<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);
}
}