From b7ea71e6e39dfda903e1060e1b254ce0002fcf0d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Marcelina=20Ko=C5=9Bcielnicka?= <mwk@0x04.net>
Date: Tue, 30 Mar 2021 04:00:45 +0200
Subject: equiv: Suggest running async2sync or clk2fflogic where appropriate.

See #2713.
---
 passes/equiv/equiv_induct.cc | 5 ++++-
 passes/equiv/equiv_simple.cc | 8 ++++++--
 2 files changed, 10 insertions(+), 3 deletions(-)

diff --git a/passes/equiv/equiv_induct.cc b/passes/equiv/equiv_induct.cc
index 37aec50cd..5f14416da 100644
--- 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 408c5a793..8d9e870da 100644
--- 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);
 			}
 
-- 
cgit v1.2.3