Added "-dump_fail_to_vcd" argument to SAT solver

passes/sat/sat.cc

@@ -30,6 +30,8 @@
 #include <stdlib.h>
 #include <stdio.h>
 #include <algorithm>
+#include <errno.h>
+#include <string.h>
 
 namespace {
 
@@ -631,6 +633,109 @@ struct SatHelper
 			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)
+			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};
+		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");
+		fprintf(f, "$version\n");
+		fprintf(f, "    Generated by %s\n", yosys_version_str); 
+		fprintf(f, "$end\n");
+		fprintf(f, "$comment\n");
+		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
+		std::map<std::string, std::string> vcdnames;
+		
+		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())
+				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
+			std::string legal_desc = info.description.c_str();
+			for (auto &c : legal_desc) {
+				if(c == '$')
+					c = '_';
+				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
+			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)
+		{
+			RTLIL::Const value;
+
+			for (int i = 0; i < info.width; i++) {
+				value.bits.push_back(modelValues.at(info.offset+i) ? RTLIL::State::S1 : RTLIL::State::S0);
+				if (enable_undef && modelValues.at(modelExpressions.size()/2 + info.offset + i))
+					value.bits.back() = RTLIL::State::Sx;
+			}
+			
+			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)
+				fprintf(f, "%c%s\n", bitvals[value.bits[0]], vcdnames[info.description].c_str());
+			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]]);
+				fprintf(f, " %s\n", vcdnames[info.description].c_str());
+			}
+		}
+
+		if (last_timestep == -2)
+			log("  no model variables selected for display.\n");
+		
+		fclose(f);
+	}
+
 	void invalidate_model(bool max_undef)
 	{
 		std::vector<int> clause;
@@ -822,6 +927,8 @@ struct SatPass : public Pass {
 		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;
+		bool dump_fail_to_vcd = false;
+		std::string vcd_file_name = "";
 
 		log_header("Executing SAT pass (solving SAT problems in the circuit).\n");
 
@@ -995,6 +1102,11 @@ struct SatPass : public Pass {
 				ignore_unknown_cells = true;
 				continue;
 			}
+			if (args[argidx] == "-dump_fail_to_vcd" && argidx+1 < args.size()) {
+				dump_fail_to_vcd = true;
+				vcd_file_name = args[++argidx];
+				continue;
+			}
 			break;
 		}
 		extra_args(args, argidx, design);
@@ -1107,6 +1219,8 @@ struct SatPass : public Pass {
 					log("SAT temporal induction proof finished - model found for base case: FAIL!\n");
 					print_proof_failed();
 					basecase.print_model();
+					if(dump_fail_to_vcd)
+						basecase.dump_model_to_vcd(vcd_file_name);
 					goto tip_failed;
 				}