Merge pull request #1433 from YosysHQ/eddie/equiv_opt_async2sync

async2sync to be called by equiv_opt only when -async2sync given

passes/equiv/equiv_opt.cc

@@ -50,6 +50,9 @@ struct EquivOptPass:public ScriptPass
 		log("    -multiclock\n");
 		log("        run clk2fflogic before equivalence checking.\n");
 		log("\n");
+		log("    -async2sync\n");
+		log("        run async2sync before equivalence checking.\n");
+		log("\n");
 		log("    -undef\n");
 		log("        enable modelling of undef states during equiv_induct.\n");
 		log("\n");
@@ -59,7 +62,7 @@ struct EquivOptPass:public ScriptPass
 	}
 
 	std::string command, techmap_opts;
-	bool assert, undef, multiclock;
+	bool assert, undef, multiclock, async2sync;
 
 	void clear_flags() YS_OVERRIDE
 	{
@@ -68,6 +71,7 @@ struct EquivOptPass:public ScriptPass
 		assert = false;
 		undef = false;
 		multiclock = false;
+		async2sync = false;
 	}
 
 	void execute(std::vector < std::string > args, RTLIL::Design * design) YS_OVERRIDE
@@ -101,6 +105,10 @@ struct EquivOptPass:public ScriptPass
 				multiclock = true;
 				continue;
 			}
+			if (args[argidx] == "-async2sync") {
+				async2sync = true;
+				continue;
+			}
 			break;
 		}
 
@@ -120,6 +128,9 @@ struct EquivOptPass:public ScriptPass
 		if (!design->full_selection())
 			log_cmd_error("This command only operates on fully selected designs!\n");
 
+		if (async2sync && multiclock)
+			log_cmd_error("The '-async2sync' and '-multiclock' options are mutually exclusive!\n");
+
 		log_header(design, "Executing EQUIV_OPT pass.\n");
 		log_push();
 
@@ -157,8 +168,8 @@ struct EquivOptPass:public ScriptPass
 		if (check_label("prove")) {
 			if (multiclock || help_mode)
 				run("clk2fflogic", "(only with -multiclock)");
-			if (!multiclock || help_mode)
+			if (async2sync || help_mode)
-				run("async2sync", "(only without -multiclock)");
+				run("async2sync", " (only with -async2sync)");
 			run("equiv_make gold gate equiv");
 			if (help_mode)
 				run("equiv_induct [-undef] equiv");

tests/ice40/latches.ys

@@ -1,14 +1,11 @@
 read_verilog latches.v
-design -save read
 
 proc
-async2sync # converts latches to a 'sync' variant clocked by a 'super'-clock
 flatten
-synth_ice40
+# Can't run any sort of equivalence check because latches are blown to LUTs
-equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # equivalency check
+#equiv_opt -async2sync -assert -map +/ice40/cells_sim.v synth_ice40 # equivalency check
-design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
 
-design -load read
+#design -load preopt
 synth_ice40
 cd top
 select -assert-count 4 t:SB_LUT4

tests/xilinx/latches.ys

@@ -2,9 +2,7 @@ read_verilog latches.v
 
 proc
 flatten
-equiv_opt -assert -run :prove -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
+equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
-async2sync
-equiv_opt -assert -run prove: -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
 
 design -load preopt
 synth_xilinx