From: Clifford Wolf <clifford@clifford.at>
Date: Sat, 9 Nov 2013 10:38:17 +0000 (+0100)
Subject: Added verification of SAT model to "eval -vloghammer_report" command
X-Git-Tag: yosys-0.2.0~377
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=18f9477e95aa57ce1659de1991117f881fa359bd;p=yosys.git

Added verification of SAT model to "eval -vloghammer_report" command
---

diff --git a/kernel/satgen.h b/kernel/satgen.h
index 6bd633603..3c63f9168 100644
--- a/kernel/satgen.h
+++ b/kernel/satgen.h
@@ -53,17 +53,16 @@ struct SatGen
 		this->prefix = prefix;
 	}
 
-	std::vector<int> importSigSpec(RTLIL::SigSpec &sig, int timestep = -1)
+	std::vector<int> importSigSpec(RTLIL::SigSpec sig, int timestep = -1)
 	{
 		assert(timestep < 0 || timestep > 0);
-		RTLIL::SigSpec s = sig;
-		sigmap->apply(s);
-		s.expand();
+		sigmap->apply(sig);
+		sig.expand();
 
 		std::vector<int> vec;
-		vec.reserve(s.chunks.size());
+		vec.reserve(sig.chunks.size());
 
-		for (auto &c : s.chunks)
+		for (auto &c : sig.chunks)
 			if (c.wire == NULL) {
 				vec.push_back(c.data.as_bool() ? ez->TRUE : ez->FALSE);
 			} else {
diff --git a/passes/sat/eval.cc b/passes/sat/eval.cc
index d805b3c84..54cb60d21 100644
--- a/passes/sat/eval.cc
+++ b/passes/sat/eval.cc
@@ -24,6 +24,7 @@
 #include "kernel/celltypes.h"
 #include "kernel/consteval.h"
 #include "kernel/sigtools.h"
+#include "kernel/satgen.h"
 #include "kernel/log.h"
 #include <stdlib.h>
 #include <stdio.h>
@@ -141,6 +142,43 @@ struct VlogHammerReporter
 		return list;
 	}
 
+	void sat_check(RTLIL::Module *module, RTLIL::SigSpec recorded_set_vars, RTLIL::Const recorded_set_vals, RTLIL::SigSpec expected_y)
+	{
+		log("Verifying SAT model..\n");
+
+		ezDefaultSAT ez;
+		SigMap sigmap(module);
+		SatGen satgen(&ez, design, &sigmap);
+
+		for (auto &c : module->cells)
+			if (!satgen.importCell(c.second))
+				log_error("Failed to import cell %s (type %s) to SAT database.\n", RTLIL::id2cstr(c.first), RTLIL::id2cstr(c.second->type));
+
+		std::vector<int> rec_var_vec = satgen.importSigSpec(recorded_set_vars);
+		std::vector<int> rec_val_vec = satgen.importSigSpec(recorded_set_vals);
+		ez.assume(ez.vec_eq(rec_var_vec, rec_val_vec));
+
+		std::vector<int> y_vec = satgen.importSigSpec(module->wires.at("\\y"));
+		std::vector<bool> y_values;
+
+		log("  Created SAT problem with %d variables and %d clauses.\n",
+				ez.numCnfVariables(), ez.numCnfClauses());
+
+		if (!ez.solve(y_vec, y_values))
+			log_error("Failed to find solution to SAT problem.\n");
+
+		expected_y.expand();
+		assert(expected_y.chunks.size() == y_vec.size());
+		for (size_t i = 0; i < y_vec.size(); i++) {
+			RTLIL::State bit = expected_y.chunks.at(i).data.bits.at(0);
+			if ((bit == RTLIL::State::S0 || bit == RTLIL::State::S1) && ((bit == RTLIL::State::S1) != y_values.at(i)))
+				log_error("Found error in SAT model: y[%d] = %d, should be %d.\n",
+						int(i), int(y_values.at(i)), int(bit == RTLIL::State::S1));
+		}
+
+		log("  SAT model verified.\n");
+	}
+
 	void run()
 	{
 		for (int idx = 0; idx < int(patterns.size()); idx++)
@@ -151,6 +189,8 @@ struct VlogHammerReporter
 
 			for (int mod = 0; mod < int(modules.size()); mod++)
 			{
+				RTLIL::SigSpec recorded_set_vars;
+				RTLIL::Const recorded_set_vals;
 				RTLIL::Module *module = modules[mod];
 				std::string module_name = module_names[mod].c_str();
 				ConstEval ce(module);
@@ -160,6 +200,8 @@ struct VlogHammerReporter
 					RTLIL::Wire *wire = module->wires.at(inputs[i]);
 					for (int j = input_widths[i]-1; j >= 0; j--) {
 						ce.set(RTLIL::SigSpec(wire, 1, j), bits.back());
+						recorded_set_vars.append(RTLIL::SigSpec(wire, 1, j));
+						recorded_set_vals.bits.push_back(bits.back());
 						bits.pop_back();
 					}
 					if (module == modules.front()) {
@@ -188,6 +230,7 @@ struct VlogHammerReporter
 				if (module_name == "rtl") {
 					rtl_sig = sig;
 					rtl_sig.expand();
+					sat_check(module, recorded_set_vars, recorded_set_vals, sig);
 				} else if (rtl_sig.width > 0) {
 					sig.expand();
 					if (rtl_sig.width != sig.width)