diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index 1aae421f0..a7a510d7d 100644
--- a/passes/sat/sat.cc
+++ b/passes/sat/sat.cc
@@ -671,7 +671,7 @@ struct SatHelper
 		fprintf(f, "    %s\n", stime);
 		fprintf(f, "$end\n");
 		fprintf(f, "$version\n");
-		fprintf(f, "    Generated by %s\n", yosys_version_str); 
+		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",
@@ -750,6 +750,81 @@ struct SatHelper
 		fclose(f);
 	}
 
+	void dump_model_to_json(std::string json_file_name)
+	{
+		FILE *f = fopen(json_file_name.c_str(), "w");
+		if (!f)
+			log_cmd_error("Can't open output file `%s' for writing: %s\n", json_file_name.c_str(), strerror(errno));
+
+		log("Dumping SAT model to WaveJSON file '%s'.\n", json_file_name.c_str());
+
+		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, "// Generated by %s\n", yosys_version_str);
+
+		int mintime = 1, maxtime = 0, maxwidth = 0;;
+		dict<string, pair<int, dict<int, Const>>> wavedata;
+
+		for (auto &info : modelInfo)
+		{
+			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;
+			}
+
+			wavedata[info.description].first = info.width;
+			wavedata[info.description].second[info.timestep] = value;
+			mintime = std::min(mintime, info.timestep);
+			maxtime = std::max(maxtime, info.timestep);
+			maxwidth = std::max(maxwidth, info.width);
+		}
+
+		fprintf(f, "{ signal: [\n");
+		for (auto &wd : wavedata) {
+			vector<string> data;
+			string name = wd.first.c_str();
+			while (name.substr(0, 1) == "\\")
+				name = name.substr(1);
+			fprintf(f, "    { name: '%s', wave: '", name.c_str());
+			for (int i = mintime; i <= maxtime; i++) {
+				if (wd.second.second.count(i)) {
+					string this_data = wd.second.second[i].as_string();
+					char ch = '=';
+					if (wd.second.first == 1)
+						ch = this_data[0];
+					if (!data.empty() && data.back() == this_data) {
+						fprintf(f, ".");
+					} else {
+						data.push_back(this_data);
+						fprintf(f, "%c", ch);
+					}
+				} else {
+					data.push_back("");
+					fprintf(f, "4");
+				}
+			}
+			if (wd.second.first != 1) {
+				fprintf(f, "', data: [");
+				for (int i = 0; i < GetSize(data); i++)
+					 fprintf(f, "%s'%s'", i ? ", " : "", data[i].c_str());
+				fprintf(f, "] },\n");
+			} else {
+				fprintf(f, "' },\n");
+			}
+		}
+		fprintf(f, "  ],\n");
+		fprintf(f, "  config: {\n");
+		fprintf(f, "    hscale: %.2f,\n", maxwidth / 4.0);
+		fprintf(f, "  },\n");
+		fprintf(f, "}\n");
+		fclose(f);
+	}
+
 	void invalidate_model(bool max_undef)
 	{
 		std::vector<int> clause;
@@ -890,6 +965,9 @@ 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_json <json-file-name>\n");
+		log("        dump SAT model (counter example in proof) to a WaveJSON 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");
@@ -952,7 +1030,7 @@ 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;
-		std::string vcd_file_name, cnf_file_name;
+		std::string vcd_file_name, json_file_name, cnf_file_name;
 
 		log_header("Executing SAT pass (solving SAT problems in the circuit).\n");
 
@@ -1143,6 +1221,10 @@ struct SatPass : public Pass {
 				vcd_file_name = args[++argidx];
 				continue;
 			}
+			if (args[argidx] == "-dump_json" && argidx+1 < args.size()) {
+				json_file_name = args[++argidx];
+				continue;
+			}
 			if (args[argidx] == "-dump_cnf" && argidx+1 < args.size()) {
 				cnf_file_name = args[++argidx];
 				continue;
@@ -1159,7 +1241,7 @@ struct SatPass : public Pass {
 							RTLIL::id2cstr(module->name), RTLIL::id2cstr(mod_it.first));
 				module = mod_it.second;
 			}
-		if (module == NULL) 
+		if (module == NULL)
 			log_cmd_error("Can't perform SAT on an empty selection!\n");
 
 		if (!prove.size() && !prove_x.size() && !prove_asserts && tempinduct)
@@ -1267,6 +1349,8 @@ struct SatPass : public Pass {
 					basecase.print_model();
 					if(!vcd_file_name.empty())
 						basecase.dump_model_to_vcd(vcd_file_name);
+					if(!json_file_name.empty())
+						basecase.dump_model_to_json(json_file_name);
 					goto tip_failed;
 				}
 
@@ -1326,6 +1410,8 @@ struct SatPass : public Pass {
 			log("\nReached maximum number of time steps -> proof failed.\n");
 			if(!vcd_file_name.empty())
 				inductstep.dump_model_to_vcd(vcd_file_name);
+			if(!json_file_name.empty())
+				inductstep.dump_model_to_json(json_file_name);
 			print_proof_failed();
 
 		tip_failed:
@@ -1424,6 +1510,8 @@ struct SatPass : public Pass {
 
 				if(!vcd_file_name.empty())
 					sathelper.dump_model_to_vcd(vcd_file_name);
+				if(!json_file_name.empty())
+					sathelper.dump_model_to_json(json_file_name);
 
 				if (loopcount != 0) {
 					loopcount--, rerun_counter++;
@@ -1487,5 +1575,5 @@ struct SatPass : public Pass {
 		}
 	}
 } SatPass;
- 
+
 PRIVATE_NAMESPACE_END