btor, smt2, smv: Add a hint on how to deal with funny FF types.

diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index 639c6f12950ad6cb1853ead8c38185736bea5b5d..692452aad5bafae5ccc4c851006256f625ee1317 100644 (file)
--- 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 a185fdd747dad6123f7f4c0c4198e42c16994aad..8be9e05f11e0eafafe3c33a4368176c6aa8fa40a 100644 (file)
--- 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 4e5c6050db61be169b5d7c9105fc7412dd2195e6..e41582fea4af14e03cf4bc5a9b6ec160f9d9bed6 100644 (file)
--- 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));