From: Bogdan Vukobratovic <bogdan.vukobratovic@gmail.com>
Date: Thu, 27 Jun 2019 20:06:23 +0000 (+0200)
Subject: Add help for "-sat" option inside opt_rmdff. "opt" can pass "-sat" too
X-Git-Tag: working-ls180~1239^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3225bfb98403271bbe8a56418ccd027b42eabda1;p=yosys.git

Add help for "-sat" option inside opt_rmdff. "opt" can pass "-sat" too
---

diff --git a/passes/opt/opt.cc b/passes/opt/opt.cc
index a4aca2fee..e9a43e0f3 100644
--- a/passes/opt/opt.cc
+++ b/passes/opt/opt.cc
@@ -44,7 +44,7 @@ struct OptPass : public Pass {
 		log("        opt_muxtree\n");
 		log("        opt_reduce [-fine] [-full]\n");
 		log("        opt_merge [-share_all]\n");
-		log("        opt_rmdff [-keepdc]\n");
+		log("        opt_rmdff [-keepdc] [-sat]\n");
 		log("        opt_clean [-purge]\n");
 		log("        opt_expr [-mux_undef] [-mux_bool] [-undriven] [-clkinv] [-fine] [-full] [-keepdc]\n");
 		log("    while <changed design>\n");
@@ -54,7 +54,7 @@ struct OptPass : public Pass {
 		log("    do\n");
 		log("        opt_expr [-mux_undef] [-mux_bool] [-undriven] [-clkinv] [-fine] [-full] [-keepdc]\n");
 		log("        opt_merge [-share_all]\n");
-		log("        opt_rmdff [-keepdc]\n");
+		log("        opt_rmdff [-keepdc] [-sat]\n");
 		log("        opt_clean [-purge]\n");
 		log("    while <changed design in opt_rmdff>\n");
 		log("\n");
@@ -112,6 +112,10 @@ struct OptPass : public Pass {
 				opt_rmdff_args += " -keepdc";
 				continue;
 			}
+			if (args[argidx] == "-sat") {
+				opt_rmdff_args += " -sat";
+				continue;
+			}
 			if (args[argidx] == "-share_all") {
 				opt_merge_args += " -share_all";
 				continue;
diff --git a/passes/opt/opt_rmdff.cc b/passes/opt/opt_rmdff.cc
index 17e0d7cd4..be6ac2d30 100644
--- a/passes/opt/opt_rmdff.cc
+++ b/passes/opt/opt_rmdff.cc
@@ -549,6 +549,10 @@ struct OptRmdffPass : public Pass {
 		log("This pass identifies flip-flops with constant inputs and replaces them with\n");
 		log("a constant driver.\n");
 		log("\n");
+		log("    -sat\n");
+		log("        additionally invoke SAT solver to detect and remove flip-flops (with \n");
+		log("        non-constant inputs) that can also be replaced with a constant driver\n");
+		log("\n");
 	}
 	void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
 	{