Progress in SMV back-end

diff --git a/backends/smv/smv.cc b/backends/smv/smv.cc
index 1758995d12228aea9e78e21e2157f5f342af56d8..86a6c3c72322c44e82d474970fec17a5fa9af151 100644 (file)
--- 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;