From 967529abb1dc13a3bf220f2a7ec6ad12dd8ce7ce Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Fri, 9 Dec 2022 15:22:21 +0100 Subject: [PATCH] formalff: Proper error messages on async inputs for the -clk2ff mode --- passes/sat/formalff.cc | 3 +++ 1 file changed, 3 insertions(+) diff --git a/passes/sat/formalff.cc b/passes/sat/formalff.cc index 209486a37..962e350a1 100644 --- a/passes/sat/formalff.cc +++ b/passes/sat/formalff.cc @@ -479,6 +479,9 @@ struct FormalFfPass : public Pass { if (ff.sig_clk.is_fully_const()) log_error("Const CLK on %s (%s) from module %s, run async2sync first.\n", log_id(cell), log_id(cell->type), log_id(module)); + if (ff.has_aload || ff.has_arst || ff.has_sr) + log_error("Async inputs on %s (%s) from module %s, run async2sync first.\n", + log_id(cell), log_id(cell->type), log_id(module)); auto clk_wire = ff.sig_clk.is_wire() ? ff.sig_clk.as_wire() : nullptr;