Added $assert support to SMV back-end

diff --git a/backends/smv/smv.cc b/backends/smv/smv.cc
index f4e8ff7246a5b222525a29634ba19684d2ab9560..03959a4f7c3bf372a61ec1265f4c3abbc7508c97 100644 (file)
--- a/backends/smv/smv.cc
+++ b/backends/smv/smv.cc
@@ -42,7 +42,7 @@ struct SmvWorker
 
        pool<Wire*> partial_assignment_wires;
        dict<SigBit, std::pair<const char*, int>> partial_assignment_bits;
-       vector<string> assignments;
+       vector<string> assignments, invarspecs;
 
        const char *cid()
        {
@@ -227,6 +227,16 @@ struct SmvWorker
                {
                        // FIXME: $slice, $concat, $mem
 
+                       if (cell->type.in("$assert"))
+                       {
+                               SigSpec sig_a = cell->getPort("\\A");
+                               SigSpec sig_en = cell->getPort("\\EN");
+
+                               invarspecs.push_back(stringf("!bool(%s) | bool(%s);", rvalue(sig_en), rvalue(sig_a)));
+
+                               continue;
+                       }
+
                        if (cell->type.in("$shl", "$shr", "$sshl", "$sshr", "$shift", "$shiftx"))
                        {
                                SigSpec sig_a = cell->getPort("\\A");
@@ -634,9 +644,16 @@ struct SmvWorker
                        assignments.push_back(stringf("%s := %s;", cid(wire->name), expr.c_str()));
                }
 
-               f << stringf("  ASSIGN\n");
-               for (const string &line : assignments)
-                       f << stringf("    %s\n", line.c_str());
+               if (!assignments.empty()) {
+                       f << stringf("  ASSIGN\n");
+                       for (const string &line : assignments)
+                               f << stringf("    %s\n", line.c_str());
+               }
+
+               if (!invarspecs.empty()) {
+                       for (const string &line : invarspecs)
+                               f << stringf("  INVARSPEC %s\n", line.c_str());
+               }
        }
 };