Merge branch 'master' of github.com:cliffordwolf/yosys

1 files changed, 93 insertions, 49 deletions

diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index 2cd15d01c..d18a220d3 100644
--- a/passes/sat/sat.cc
+++ b/passes/sat/sat.cc
@@ -632,27 +632,27 @@ struct SatHelper
 		if (last_timestep == -2)
 			log("  no model variables selected for display.\n");
 	}
-	
+
 	void dump_model_to_vcd(std::string vcd_file_name)
 	{
-		FILE* f = fopen(vcd_file_name.c_str(), "w");
-		if(!f)
+		FILE *f = fopen(vcd_file_name.c_str(), "w");
+		if (!f)
 			log_cmd_error("Can't open output file `%s' for writing: %s\n", vcd_file_name.c_str(), strerror(errno));
-		
+
 		log("Dumping SAT model to VCD file %s\n", vcd_file_name.c_str());
-		
+
 		time_t timestamp;
 		struct tm* now;
-		char stime[128] = {0};
+		char stime[128] = {};
 		time(&timestamp);
 		now = localtime(&timestamp);
 		strftime(stime, sizeof(stime), "%c", now);
-			
+
 		std::string module_fname = "unknown";
 		auto apos = module->attributes.find("\\src");
 		if(apos != module->attributes.end())
 			module_fname = module->attributes["\\src"].decode_string();
-			
+
 		fprintf(f, "$date\n");
 		fprintf(f, "    %s\n", stime);
 		fprintf(f, "$end\n");
@@ -663,21 +663,22 @@ struct SatHelper
 		fprintf(f, "    Generated from SAT problem in module %s (declared at %s)\n",
 			module->name.c_str(), module_fname.c_str());
 		fprintf(f, "$end\n");
-		
-		//VCD has some limits on internal (non-display) identifier names, so make legal ones
+
+		// VCD has some limits on internal (non-display) identifier names, so make legal ones
 		std::map<std::string, std::string> vcdnames;
-		
-		fprintf(f, "$timescale 1ns\n");		//arbitrary time scale since actual clock period is unknown/unimportant
+
+		fprintf(f, "$timescale 1ns\n"); // arbitrary time scale since actual clock period is unknown/unimportant
 		fprintf(f, "$scope module %s $end\n", module->name.c_str());
-		for (auto &info : modelInfo) {
-			if(vcdnames.find(info.description) != vcdnames.end())
+		for (auto &info : modelInfo)
+		{
+			if (vcdnames.find(info.description) != vcdnames.end())
 				continue;
-			
+
 			char namebuf[16];
 			snprintf(namebuf, sizeof(namebuf), "v%d", static_cast<int>(vcdnames.size()));
 			vcdnames[info.description] = namebuf;
-			
-			//Even display identifiers can't use some special characters
+
+			// Even display identifiers can't use some special characters
 			std::string legal_desc = info.description.c_str();
 			for (auto &c : legal_desc) {
 				if(c == '$')
@@ -685,21 +686,21 @@ struct SatHelper
 				if(c == ':')
 					c = '_';
 			}
-			
+
 			fprintf(f, "$var wire %d %s %s $end\n", info.width, namebuf, legal_desc.c_str());
-			
-			//Need to look at first *two* cycles!
-			//We need to put a name on all variables but those without an initialization clause
-			//have no value at timestep 0
+
+			// Need to look at first *two* cycles!
+			// We need to put a name on all variables but those without an initialization clause
+			// have no value at timestep 0
 			if(info.timestep > 1)
 				break;
 		}
 		fprintf(f, "$upscope $end\n");
 		fprintf(f, "$enddefinitions $end\n");
 		fprintf(f, "$dumpvars\n");
-		
+
 		static const char bitvals[] = "01xzxx";
-		
+
 		int last_timestep = -2;
 		for (auto &info : modelInfo)
 		{
@@ -710,19 +711,18 @@ struct SatHelper
 				if (enable_undef && modelValues.at(modelExpressions.size()/2 + info.offset + i))
 					value.bits.back() = RTLIL::State::Sx;
 			}
-			
-			if (info.timestep != last_timestep) {			
+
+			if (info.timestep != last_timestep) {
 				if(last_timestep == 0)
 					fprintf(f, "$end\n");
 				else
 					fprintf(f, "#%d\n", info.timestep);
-				
 				last_timestep = info.timestep;
 			}
-			
-			if(info.width == 1)
+
+			if(info.width == 1) {
 				fprintf(f, "%c%s\n", bitvals[value.bits[0]], vcdnames[info.description].c_str());
-			else {
+			} else {
 				fprintf(f, "b");
 				for(int k=info.width-1; k >= 0; k --)	//need to flip bit ordering for VCD
 					fprintf(f, "%c", bitvals[value.bits[k]]);
@@ -732,7 +732,7 @@ struct SatHelper
 
 		if (last_timestep == -2)
 			log("  no model variables selected for display.\n");
-		
+
 		fclose(f);
 	}
 
@@ -878,6 +878,10 @@ struct SatPass : public Pass {
 		log("    -dump_vcd <vcd-file-name>\n");
 		log("        dump SAT model (counter example in proof) to VCD file\n");
 		log("\n");
+		log("    -dump_cnf <cnf-file-name>\n");
+		log("        dump CNF of SAT problem (in DIMACS format). in temporal induction\n");
+		log("        proofs this is the CNF of the first induction step.\n");
+		log("\n");
 		log("The following additional options can be used to set up a proof. If also -seq\n");
 		log("is passed, a temporal induction proof is performed.\n");
 		log("\n");
@@ -903,6 +907,9 @@ struct SatPass : public Pass {
 		log("    -maxsteps <N>\n");
 		log("        Set a maximum length for the induction.\n");
 		log("\n");
+		log("    -initsteps <N>\n");
+		log("        Set initial length for the induction.\n");
+		log("\n");
 		log("    -timeout <N>\n");
 		log("        Maximum number of seconds a single SAT instance may take.\n");
 		log("\n");
@@ -925,12 +932,12 @@ struct SatPass : public Pass {
 		std::map<int, std::vector<std::pair<std::string, std::string>>> sets_at;
 		std::map<int, std::vector<std::string>> unsets_at, sets_def_at, sets_any_undef_at, sets_all_undef_at;
 		std::vector<std::string> shows, sets_def, sets_any_undef, sets_all_undef;
-		int loopcount = 0, seq_len = 0, maxsteps = 0, timeout = 0;
+		int loopcount = 0, seq_len = 0, maxsteps = 0, initsteps = 0, timeout = 0;
 		bool verify = false, fail_on_timeout = false, enable_undef = false, set_def_inputs = false;
 		bool ignore_div_by_zero = false, set_init_undef = false, set_init_zero = false, max_undef = false;
 		bool tempinduct = false, prove_asserts = false, show_inputs = false, show_outputs = false;
 		bool ignore_unknown_cells = false, falsify = false, tempinduct_def = false, set_init_def = false;
-		std::string vcd_file_name;
+		std::string vcd_file_name, cnf_file_name;
 
 		log_header("Executing SAT pass (solving SAT problems in the circuit).\n");
 
@@ -970,6 +977,10 @@ struct SatPass : public Pass {
 				maxsteps = atoi(args[++argidx].c_str());
 				continue;
 			}
+			if (args[argidx] == "-initsteps" && argidx+1 < args.size()) {
+				initsteps = atoi(args[++argidx].c_str());
+				continue;
+			}
 			if (args[argidx] == "-ignore_div_by_zero") {
 				ignore_div_by_zero = true;
 				continue;
@@ -1108,6 +1119,10 @@ struct SatPass : public Pass {
 				vcd_file_name = args[++argidx];
 				continue;
 			}
+			if (args[argidx] == "-dump_cnf" && argidx+1 < args.size()) {
+				cnf_file_name = args[++argidx];
+				continue;
+			}
 			break;
 		}
 		extra_args(args, argidx, design);
@@ -1240,21 +1255,42 @@ struct SatPass : public Pass {
 				if (inductlen > 1)
 					inductstep.force_unique_state(1, inductlen + 1);
 
-				log("\n[induction step] Solving problem with %d variables and %d clauses..\n",
-						inductstep.ez.numCnfVariables(), inductstep.ez.numCnfClauses());
-
-				if (!inductstep.solve(inductstep.ez.NOT(property))) {
-					if (inductstep.gotTimeout)
-						goto timeout;
-					log("Induction step proven: SUCCESS!\n");
-					print_qed();
-					goto tip_success;
+				if (inductlen < initsteps)
+				{
+					log("\n[induction step] Skipping problem with %d variables and %d clauses (below initsteps).\n",
+							inductstep.ez.numCnfVariables(), inductstep.ez.numCnfClauses());
+					inductstep.ez.assume(property);
 				}
+				else
+				{
+					if (!cnf_file_name.empty())
+					{
+						FILE *f = fopen(cnf_file_name.c_str(), "w");
+						if (!f)
+							log_cmd_error("Can't open output file `%s' for writing: %s\n", cnf_file_name.c_str(), strerror(errno));
 
-				log("Induction step failed. Incrementing induction length.\n");
-				inductstep.ez.assume(property);
+						log("Dumping CNF to file `%s'.\n", cnf_file_name.c_str());
+						cnf_file_name.clear();
 
-				inductstep.print_model();
+						inductstep.ez.printDIMACS(f, false);
+						fclose(f);
+					}
+
+					log("\n[induction step] Solving problem with %d variables and %d clauses..\n",
+							inductstep.ez.numCnfVariables(), inductstep.ez.numCnfClauses());
+
+					if (!inductstep.solve(inductstep.ez.NOT(property))) {
+						if (inductstep.gotTimeout)
+							goto timeout;
+						log("Induction step proven: SUCCESS!\n");
+						print_qed();
+						goto tip_success;
+					}
+
+					log("Induction step failed. Incrementing induction length.\n");
+					inductstep.ez.assume(property);
+					inductstep.print_model();
+				}
 			}
 
 			log("\nReached maximum number of time steps -> proof failed.\n");
@@ -1318,10 +1354,18 @@ struct SatPass : public Pass {
 			}
 			sathelper.generate_model();
 
-#if 0
-			// print CNF for debugging
-			sathelper.ez.printDIMACS(stdout, true);
-#endif
+			if (!cnf_file_name.empty())
+			{
+				FILE *f = fopen(cnf_file_name.c_str(), "w");
+				if (!f)
+					log_cmd_error("Can't open output file `%s' for writing: %s\n", cnf_file_name.c_str(), strerror(errno));
+
+				log("Dumping CNF to file `%s'.\n", cnf_file_name.c_str());
+				cnf_file_name.clear();
+
+				sathelper.ez.printDIMACS(f, false);
+				fclose(f);
+			}
 
 			int rerun_counter = 0;