Added init support to SMV back-end

diff --git a/backends/smv/smv.cc b/backends/smv/smv.cc
index 9db3d3a6edd3e9f9d8b2f95af44320547a676621..9e304daefed335b810441734f90235a6fc940384 100644 (file)
--- a/backends/smv/smv.cc
+++ b/backends/smv/smv.cc
@@ -218,6 +218,9 @@ struct SmvWorker
                                partial_assignment_wires.insert(wire);
 
                        f << stringf("    %s : unsigned word[%d]; -- %s\n", cid(wire->name), wire->width, log_id(wire));
+
+                       if (wire->attributes.count("\\init"))
+                               assignments.push_back(stringf("init(%s) := %s;", lvalue(wire), rvalue(wire->attributes.at("\\init"))));
                }
 
                for (auto cell : module->cells())
@@ -483,7 +486,6 @@ struct SmvWorker
 
                        if (cell->type == "$dff")
                        {
-                               // FIXME: use init property
                                assignments.push_back(stringf("next(%s) := %s;", lvalue(cell->getPort("\\Q")), rvalue(cell->getPort("\\D"))));
                                continue;
                        }