Merge branch 'master' of github.com:YosysHQ/yosys into claire/eqystuff

5 files changed, 25 insertions, 5 deletions

diff --git a/passes/cmds/stat.cc b/passes/cmds/stat.cc
index a998ab8e7..10e98952e 100644
--- a/passes/cmds/stat.cc
+++ b/passes/cmds/stat.cc
@@ -452,7 +452,7 @@ struct StatPass : public Pass {
 
 		if (json_mode) {
 			log("\n");
-			log("   },\n");
+			log(top_mod == nullptr ? "   }\n" : "   },\n");
 		}
 
 		if (top_mod != nullptr)
@@ -466,7 +466,7 @@ struct StatPass : public Pass {
 
 			statdata_t data = hierarchy_worker(mod_stat, top_mod->name, 0, /*quiet=*/json_mode);
 
-			if (json_mode) 
+			if (json_mode)
 				data.log_data_json("design", true);
 			else if (GetSize(mod_stat) > 1) {
 				log("\n");
diff --git a/passes/cmds/tee.cc b/passes/cmds/tee.cc
index 7a1f4a36b..39ed4a7a8 100644
--- a/passes/cmds/tee.cc
+++ b/passes/cmds/tee.cc
@@ -45,6 +45,9 @@ struct TeePass : public Pass {
 		log("    -a logfile\n");
 		log("        Write output to this file, append if exists.\n");
 		log("\n");
+		log("    -s scratchpad\n");
+		log("        Write output to this scratchpad value, truncate if it exists.\n");
+		log("\n");
 		log("    +INT, -INT\n");
 		log("        Add/subtract INT from the -v setting for this command.\n");
 		log("\n");
@@ -53,9 +56,11 @@ struct TeePass : public Pass {
 	{
 		std::vector<FILE*> backup_log_files, files_to_close;
 		std::vector<std::ostream*> backup_log_streams;
+		std::vector<std::string> backup_log_scratchpads;
 		int backup_log_verbose_level = log_verbose_level;
 		backup_log_streams = log_streams;
 		backup_log_files = log_files;
+		backup_log_scratchpads = log_scratchpads;
 
 		size_t argidx;
 		for (argidx = 1; argidx < args.size(); argidx++)
@@ -78,6 +83,12 @@ struct TeePass : public Pass {
 				files_to_close.push_back(f);
 				continue;
 			}
+			if (args[argidx] == "-s" && argidx+1 < args.size()) {
+				auto name = args[++argidx];
+				design->scratchpad[name] = "";
+				log_scratchpads.push_back(name);
+				continue;
+			}
 			if (GetSize(args[argidx]) >= 2 && (args[argidx][0] == '-' || args[argidx][0] == '+') && args[argidx][1] >= '0' && args[argidx][1] <= '9') {
 				log_verbose_level += atoi(args[argidx].c_str());
 				continue;
@@ -93,6 +104,7 @@ struct TeePass : public Pass {
 				fclose(cf);
 			log_files = backup_log_files;
 			log_streams = backup_log_streams;
+			log_scratchpads = backup_log_scratchpads;
 			throw;
 		}
 
@@ -102,6 +114,7 @@ struct TeePass : public Pass {
 		log_verbose_level = backup_log_verbose_level;
 		log_files = backup_log_files;
 		log_streams = backup_log_streams;
+		log_scratchpads = backup_log_scratchpads;
 	}
 } TeePass;
 
diff --git a/passes/sat/formalff.cc b/passes/sat/formalff.cc
index b2a91b155..e36379096 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;
 
diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc
index 4580f194e..42d3e188a 100644
--- a/passes/sat/qbfsat.cc
+++ b/passes/sat/qbfsat.cc
@@ -416,6 +416,8 @@ QbfSolveOptions parse_args(const std::vector<std::string> &args) {
 					opt.solver = opt.Solver::Yices;
 				else if (args[opt.argidx+1] == "cvc4")
 					opt.solver = opt.Solver::CVC4;
+				else if (args[opt.argidx+1] == "cvc5")
+					opt.solver = opt.Solver::CVC5;
 				else
 					log_cmd_error("Unknown solver \"%s\".\n", args[opt.argidx+1].c_str());
 				opt.argidx++;
@@ -542,8 +544,8 @@ struct QbfSatPass : public Pass {
 		log("        hope that the solver supports optimizing quantified bitvector problems.\n");
 		log("\n");
 		log("    -solver <solver>\n");
-		log("        Use a particular solver. Choose one of: \"z3\", \"yices\", and \"cvc4\".\n");
-		log("        (default: yices)\n");
+		log("        Use a particular solver. Choose one of: \"z3\", \"yices\", \"cvc4\"\n");
+		log("        and \"cvc5\". (default: yices)\n");
 		log("\n");
 		log("    -solver-option <name> <value>\n");
 		log("        Set the specified solver option in the SMT-LIBv2 problem file.\n");
diff --git a/passes/sat/qbfsat.h b/passes/sat/qbfsat.h
index c96c6f818..8fb6093bc 100644
--- a/passes/sat/qbfsat.h
+++ b/passes/sat/qbfsat.h
@@ -29,7 +29,7 @@ struct QbfSolveOptions {
 	bool specialize = false, specialize_from_file = false, write_solution = false, nocleanup = false;
 	bool dump_final_smt2 = false, assume_outputs = false, assume_neg = false, nooptimize = false;
 	bool nobisection = false, sat = false, unsat = false, show_smtbmc = false;
-	enum Solver{Z3, Yices, CVC4} solver = Yices;
+	enum Solver{Z3, Yices, CVC4, CVC5} solver = Yices;
 	enum OptimizationLevel{O0, O1, O2} oflag = O0;
 	dict<std::string, std::string> solver_options;
 	int timeout = 0;
@@ -45,6 +45,8 @@ struct QbfSolveOptions {
 			return "yices";
 		else if (solver == Solver::CVC4)
 			return "cvc4";
+		else if (solver == Solver::CVC5)
+			return "cvc5";
 
 		log_cmd_error("unknown solver specified.\n");
 		return "";