diff options
Diffstat (limited to 'backends/smv')
-rw-r--r-- | backends/smv/smv.cc | 83 |
1 files changed, 72 insertions, 11 deletions
diff --git a/backends/smv/smv.cc b/backends/smv/smv.cc index 1758995d1..86a6c3c72 100644 --- a/backends/smv/smv.cc +++ b/backends/smv/smv.cc @@ -166,7 +166,7 @@ struct SmvWorker f << stringf(" VAR\n"); for (auto wire : module->wires()) - f << stringf(" %s : unsigned word[%d];\n", cid(wire->name), wire->width); + f << stringf(" %s : unsigned word[%d]; -- %s\n", cid(wire->name), wire->width, log_id(wire)); for (auto cell : module->cells()) { @@ -374,8 +374,65 @@ struct SmvWorker continue; } - // FIXME: $_BUF_, $_NOT_, $_AND_, $_NAND_, $_OR_, $_NOR_, - // $_XOR_, $_XNOR_, $_MUX_, $_AOI3_, $_OAI3_, $_AOI4_, $_OAI4_ + if (cell->type.in("$_BUF_", "$_NOT_")) + { + string op = cell->type == "$_NOT_" ? "!" : ""; + assignments.push_back(stringf("%s := %s%s;", lvalue(cell->getPort("\\Y")), op.c_str(), rvalue(cell->getPort("\\A")))); + continue; + } + + if (cell->type.in("$_AND_", "$_NAND_", "$_OR_", "$_NOR_", "$_XOR_", "$_XNOR_")) + { + string op; + + if (cell->type.in("$_AND_", "$_NAND_")) op = "&"; + if (cell->type.in("$_OR_", "$_NOR_")) op = "|"; + if (cell->type.in("$_XOR_")) op = "xor"; + if (cell->type.in("$_XNOR_")) op = "xnor"; + + if (cell->type.in("$_NAND_", "$_NOR_")) + assignments.push_back(stringf("%s := !(%s %s %s);", lvalue(cell->getPort("\\Y")), + rvalue(cell->getPort("\\A")), op.c_str(), rvalue(cell->getPort("\\B")))); + else + assignments.push_back(stringf("%s := %s %s %s;", lvalue(cell->getPort("\\Y")), + rvalue(cell->getPort("\\A")), op.c_str(), rvalue(cell->getPort("\\B")))); + continue; + } + + if (cell->type == "$_MUX_") + { + assignments.push_back(stringf("%s := %s ? %s : %s;", lvalue(cell->getPort("\\Y")), + rvalue(cell->getPort("\\S")), rvalue(cell->getPort("\\B")), rvalue(cell->getPort("\\A")))); + continue; + } + + if (cell->type == "$_AOI3_") + { + assignments.push_back(stringf("%s := !((%s & %s) | %s);", lvalue(cell->getPort("\\Y")), + rvalue(cell->getPort("\\A")), rvalue(cell->getPort("\\B")), rvalue(cell->getPort("\\C")))); + continue; + } + + if (cell->type == "$_OAI3_") + { + assignments.push_back(stringf("%s := !((%s | %s) & %s);", lvalue(cell->getPort("\\Y")), + rvalue(cell->getPort("\\A")), rvalue(cell->getPort("\\B")), rvalue(cell->getPort("\\C")))); + continue; + } + + if (cell->type == "$_AOI4_") + { + assignments.push_back(stringf("%s := !((%s & %s) | (%s & %s));", lvalue(cell->getPort("\\Y")), + rvalue(cell->getPort("\\A")), rvalue(cell->getPort("\\B")), rvalue(cell->getPort("\\C")), rvalue(cell->getPort("\\D")))); + continue; + } + + if (cell->type == "$_OAI4_") + { + assignments.push_back(stringf("%s := !((%s | %s) & (%s | %s));", lvalue(cell->getPort("\\Y")), + rvalue(cell->getPort("\\A")), rvalue(cell->getPort("\\B")), rvalue(cell->getPort("\\C")), rvalue(cell->getPort("\\D")))); + continue; + } if (cell->type[0] == '$') log_error("Found currently unsupported cell type %s (%s.%s).\n", log_id(cell->type), log_id(module), log_id(cell)); @@ -473,7 +530,7 @@ struct SmvBackend : public Backend { while (indent < GetSize(line) && (line[indent] == ' ' || line[indent] == '\t')) indent++; - if (line[indent] == '$') + if (line[indent] == '%') { vector<string> stmt = split_tokens(line); @@ -483,6 +540,7 @@ struct SmvBackend : public Backend { if (GetSize(stmt) == 2 && stmt[0] == "%module") { Module *module = design->module(RTLIL::escape_id(stmt[1])); + modules.erase(module); if (module == nullptr) log_error("Module '%s' not found.\n", stmt[1].c_str()); @@ -504,15 +562,18 @@ struct SmvBackend : public Backend { } } - *f << stringf("-- SMV description generated by %s\n", yosys_version_str); + if (!modules.empty()) + { + *f << stringf("-- SMV description generated by %s\n", yosys_version_str); - for (auto module : modules) { - log("Creating SMV representation of module %s.\n", log_id(module)); - SmvWorker worker(module, verbose, *f); - worker.run(); - } + for (auto module : modules) { + log("Creating SMV representation of module %s.\n", log_id(module)); + SmvWorker worker(module, verbose, *f); + worker.run(); + } - *f << stringf("-- end of yosys output\n"); + *f << stringf("-- end of yosys output\n"); + } if (template_f.is_open()) { std::string line; |