equiv: Suggest running async2sync or clk2fflogic where appropriate.

See #2713.

diff --git a/passes/equiv/equiv_induct.cc b/passes/equiv/equiv_induct.cc
index 37aec50cd42d8f7ba89b5b461d04539c93887af7..5f14416da1c864574d8fb4ad5cfb8ce291c51523 100644 (file)
--- a/passes/equiv/equiv_induct.cc
+++ b/passes/equiv/equiv_induct.cc
@@ -55,7 +55,10 @@ struct EquivInductWorker
 
                for (auto cell : cells) {
                        if (!satgen.importCell(cell, step) && !cell_warn_cache.count(cell)) {
-                               log_warning("No SAT model available for cell %s (%s).\n", log_id(cell), log_id(cell->type));
+                               if (RTLIL::builtin_ff_cell_types().count(cell->type))
+                                       log_warning("No SAT model available for async FF cell %s (%s).  Consider running `async2sync` or `clk2fflogic` first.\n", log_id(cell), log_id(cell->type));
+                               else
+                                       log_warning("No SAT model available for cell %s (%s).\n", log_id(cell), log_id(cell->type));
                                cell_warn_cache.insert(cell);
                        }
                        if (cell->type == ID($equiv)) {

diff --git a/passes/equiv/equiv_simple.cc b/passes/equiv/equiv_simple.cc
index 408c5a7934f6f1897a1f15f9dcc737d5e92142d6..8d9e870da4460fc06554bf06075a8961bc7aa29a 100644 (file)
--- a/passes/equiv/equiv_simple.cc
+++ b/passes/equiv/equiv_simple.cc
@@ -184,8 +184,12 @@ struct EquivSimpleWorker
 
                        for (auto cell : problem_cells) {
                                auto key = pair<Cell*, int>(cell, step+1);
-                               if (!imported_cells_cache.count(key) && !satgen.importCell(cell, step+1))
-                                       log_cmd_error("No SAT model available for cell %s (%s).\n", log_id(cell), log_id(cell->type));
+                               if (!imported_cells_cache.count(key) && !satgen.importCell(cell, step+1)) {
+                                       if (RTLIL::builtin_ff_cell_types().count(cell->type))
+                                               log_cmd_error("No SAT model available for async FF cell %s (%s).  Consider running `async2sync` or `clk2fflogic` first.\n", log_id(cell), log_id(cell->type));
+                                       else
+                                               log_cmd_error("No SAT model available for cell %s (%s).\n", log_id(cell), log_id(cell->type));
+                               }
                                imported_cells_cache.insert(key);
                        }