From 979347999f72591b5536e58110cfd491edccc937 Mon Sep 17 00:00:00 2001
From: =?utf8?q?Marcelina=20Ko=C5=9Bcielnicka?= <mwk@0x04.net>
Date: Tue, 23 Feb 2021 12:06:21 +0100
Subject: [PATCH] btor, smt2, smv: Add a hint on how to deal with funny FF
 types.

---
 backends/btor/btor.cc | 15 ++++++++++++++-
 backends/smt2/smt2.cc | 12 ++++++++++++
 backends/smv/smv.cc   | 18 ++++++++++++++++--
 3 files changed, 42 insertions(+), 3 deletions(-)

diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index 639c6f129..692452aad 100644
--- a/backends/btor/btor.cc
+++ b/backends/btor/btor.cc
@@ -860,7 +860,20 @@ struct BtorWorker
 			goto okay;
 		}
 
-		log_error("Unsupported cell type: %s (%s)\n", log_id(cell->type), log_id(cell));
+		if (cell->type.in(ID($dffe), ID($sdff), ID($sdffe), ID($sdffce)) || cell->type.str().substr(0, 6) == "$_SDFF" || (cell->type.str().substr(0, 6) == "$_DFFE" && cell->type.str().size() == 10)) {
+			log_error("Unsupported cell type %s for cell %s.%s -- please run `dffunmap` before `write_btor`.\n",
+					log_id(cell->type), log_id(module), log_id(cell));
+		}
+		if (cell->type.in(ID($adff), ID($adffe), ID($dffsr), ID($dffsre)) || cell->type.str().substr(0, 5) == "$_DFF") {
+			log_error("Unsupported cell type %s for cell %s.%s -- please run `async2sync; dffunmap` or `clk2fflogic` before `write_btor`.\n",
+					log_id(cell->type), log_id(module), log_id(cell));
+		}
+		if (cell->type.in(ID($sr), ID($dlatch), ID($adlatch), ID($dlatchsr)) || cell->type.str().substr(0, 8) == "$_DLATCH" || cell->type.str().substr(0, 5) == "$_SR_") {
+			log_error("Unsupported cell type %s for cell %s.%s -- please run `clk2fflogic` before `write_btor`.\n",
+					log_id(cell->type), log_id(module), log_id(cell));
+		}
+		log_error("Unsupported cell type %s for cell %s.%s.\n",
+				log_id(cell->type), log_id(module), log_id(cell));
 
 	okay:
 		btorf_pop(log_id(cell));
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index a185fdd74..8be9e05f1 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -855,6 +855,18 @@ struct Smt2Worker
 			return;
 		}
 
+		if (cell->type.in(ID($dffe), ID($sdff), ID($sdffe), ID($sdffce)) || cell->type.str().substr(0, 6) == "$_SDFF" || (cell->type.str().substr(0, 6) == "$_DFFE" && cell->type.str().size() == 10)) {
+			log_error("Unsupported cell type %s for cell %s.%s -- please run `dffunmap` before `write_smt2`.\n",
+					log_id(cell->type), log_id(module), log_id(cell));
+		}
+		if (cell->type.in(ID($adff), ID($adffe), ID($dffsr), ID($dffsre)) || cell->type.str().substr(0, 5) == "$_DFF") {
+			log_error("Unsupported cell type %s for cell %s.%s -- please run `async2sync; dffunmap` or `clk2fflogic` before `write_smt2`.\n",
+					log_id(cell->type), log_id(module), log_id(cell));
+		}
+		if (cell->type.in(ID($sr), ID($dlatch), ID($adlatch), ID($dlatchsr)) || cell->type.str().substr(0, 8) == "$_DLATCH" || cell->type.str().substr(0, 5) == "$_SR_") {
+			log_error("Unsupported cell type %s for cell %s.%s -- please run `clk2fflogic` before `write_smt2`.\n",
+					log_id(cell->type), log_id(module), log_id(cell));
+		}
 		log_error("Unsupported cell type %s for cell %s.%s.\n",
 				log_id(cell->type), log_id(module), log_id(cell));
 	}
diff --git a/backends/smv/smv.cc b/backends/smv/smv.cc
index 4e5c6050d..e41582fea 100644
--- a/backends/smv/smv.cc
+++ b/backends/smv/smv.cc
@@ -573,8 +573,22 @@ struct SmvWorker
 				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));
+			if (cell->type[0] == '$') {
+				if (cell->type.in(ID($dffe), ID($sdff), ID($sdffe), ID($sdffce)) || cell->type.str().substr(0, 6) == "$_SDFF" || (cell->type.str().substr(0, 6) == "$_DFFE" && cell->type.str().size() == 10)) {
+					log_error("Unsupported cell type %s for cell %s.%s -- please run `dffunmap` before `write_smv`.\n",
+							log_id(cell->type), log_id(module), log_id(cell));
+				}
+				if (cell->type.in(ID($adff), ID($adffe), ID($dffsr), ID($dffsre)) || cell->type.str().substr(0, 5) == "$_DFF") {
+					log_error("Unsupported cell type %s for cell %s.%s -- please run `async2sync; dffunmap` or `clk2fflogic` before `write_smv`.\n",
+							log_id(cell->type), log_id(module), log_id(cell));
+				}
+				if (cell->type.in(ID($sr), ID($dlatch), ID($adlatch), ID($dlatchsr)) || cell->type.str().substr(0, 8) == "$_DLATCH" || cell->type.str().substr(0, 5) == "$_SR_") {
+					log_error("Unsupported cell type %s for cell %s.%s -- please run `clk2fflogic` before `write_smv`.\n",
+							log_id(cell->type), log_id(module), log_id(cell));
+				}
+				log_error("Unsupported cell type %s for cell %s.%s.\n",
+						log_id(cell->type), log_id(module), log_id(cell));
+			}
 
 //			f << stringf("    %s : %s;\n", cid(cell->name), cid(cell->type));
 
-- 
2.30.2