From: Eddie Hung <eddie@fpgeh.com>
Date: Mon, 30 Sep 2019 17:59:56 +0000 (-0700)
Subject: Update doc for equiv_opt
X-Git-Tag: working-ls180~1028
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a274b7cc86d4f64541d3d2903b4eeed4616ab1d8;p=yosys.git

Update doc for equiv_opt
---

diff --git a/passes/equiv/equiv_opt.cc b/passes/equiv/equiv_opt.cc
index 9fe3bbd57..4ab5b1a3e 100644
--- a/passes/equiv/equiv_opt.cc
+++ b/passes/equiv/equiv_opt.cc
@@ -32,7 +32,8 @@ struct EquivOptPass:public ScriptPass
 		log("\n");
 		log("    equiv_opt [options] [command]\n");
 		log("\n");
-		log("This command checks circuit equivalence before and after an optimization pass.\n");
+		log("This command uses temporal induction to check circuit equivalence before and\n");
+                log("after an optimization pass.\n");
 		log("\n");
 		log("    -run <from_label>:<to_label>\n");
 		log("        only run the commands between the labels (see below). an empty\n");
@@ -156,7 +157,7 @@ struct EquivOptPass:public ScriptPass
 		if (check_label("prove")) {
 			if (multiclock || help_mode)
 				run("clk2fflogic", "(only with -multiclock)");
-			else
+			if (!multiclock || help_mode)
 				run("async2sync", "(only without -multiclock)");
 			run("equiv_make gold gate equiv");
 			if (help_mode)