Added $assert support to SMV back-end

1 files changed, 21 insertions, 4 deletions

diff --git a/backends/smv/smv.cc b/backends/smv/smv.cc
index f4e8ff72..03959a4f 100644
--- 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());
+		}
 	}
 };