Added consteval testing to xsthammer and fixed bugs

kernel/celltypes.h

@@ -185,6 +185,14 @@ struct CellTypes
 
 	static RTLIL::Const eval(std::string type, const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len)
 	{
+		if (type == "$sshr" && !signed1)
+			type = "$shr";
+		if (type == "$sshl" && !signed1)
+			type = "$shl";
+
+		if (!signed1 || !signed2)
+			signed1 = false, signed2 = false;
+
 #define HANDLE_CELL_TYPE(_t) if (type == "$" #_t) return const_ ## _t(arg1, arg2, signed1, signed2, result_len);
 		HANDLE_CELL_TYPE(not)
 		HANDLE_CELL_TYPE(and)

passes/sat/sat.cc

@@ -23,6 +23,7 @@
 
 #include "kernel/register.h"
 #include "kernel/celltypes.h"
+#include "kernel/consteval.h"
 #include "kernel/sigtools.h"
 #include "kernel/log.h"
 #include "kernel/satgen.h"
@@ -115,6 +116,8 @@ static bool parse_sigstr(RTLIL::SigSpec &sig, RTLIL::Module *module, std::string
 	return true;
 }
 
+namespace {
+
 struct SatHelper
 {
 	RTLIL::Design *design;
@@ -448,6 +451,85 @@ struct SatHelper
 	}
 };
 
+/* this should only be used for regression testing of ConstEval -- see tests/xsthammer */
+struct BruteForceEquivChecker
+{
+	RTLIL::Module *mod1, *mod2;
+	RTLIL::SigSpec mod1_inputs, mod1_outputs;
+	RTLIL::SigSpec mod2_inputs, mod2_outputs;
+	int counter, errors;
+
+	void run_checker(RTLIL::SigSpec &inputs)
+	{
+		if (inputs.width < mod1_inputs.width) {
+			RTLIL::SigSpec inputs0 = inputs, inputs1 = inputs;
+			inputs0.append(RTLIL::Const(0, 1));
+			inputs1.append(RTLIL::Const(1, 1));
+			run_checker(inputs0);
+			run_checker(inputs1);
+			return;
+		}
+
+		inputs.optimize();
+
+		ConstEval ce1(mod1), ce2(mod2);
+		ce1.set(mod1_inputs, inputs.as_const());
+		ce2.set(mod2_inputs, inputs.as_const());
+
+		RTLIL::SigSpec sig1 = mod1_outputs, undef1;
+		RTLIL::SigSpec sig2 = mod2_outputs, undef2;
+
+		if (!ce1.eval(sig1, undef1))
+			log("Failed ConstEval of module 1 outputs at signal %s (input: %s = %s).\n",
+					log_signal(undef1), log_signal(mod1_inputs), log_signal(inputs));
+		if (!ce2.eval(sig2, undef2))
+			log("Failed ConstEval of module 2 outputs at signal %s (input: %s = %s).\n",
+					log_signal(undef2), log_signal(mod1_inputs), log_signal(inputs));
+
+		if (sig1 != sig2) {
+			log("Found counter-example:\n");
+			log("  Module 1:  %s = %s  =>  %s = %s\n", log_signal(mod1_inputs), log_signal(inputs), log_signal(mod1_outputs), log_signal(sig1));
+			log("  Module 2:  %s = %s  =>  %s = %s\n", log_signal(mod2_inputs), log_signal(inputs), log_signal(mod2_outputs), log_signal(sig2));
+			errors++;
+		}
+
+		counter++;
+	}
+
+	BruteForceEquivChecker(RTLIL::Module *mod1, RTLIL::Module *mod2) :
+			mod1(mod1), mod2(mod2), counter(0), errors(0)
+	{
+		log("Checking for equivialence (brute-force): %s vs %s\n", mod1->name.c_str(), mod2->name.c_str());
+		for (auto &w : mod1->wires)
+		{
+			RTLIL::Wire *wire1 = w.second;
+			if (wire1->port_id == 0)
+				continue;
+
+			if (mod2->wires.count(wire1->name) == 0)
+				log_cmd_error("Port %s in module 1 has no counterpart in module 2!\n", wire1->name.c_str());
+
+			RTLIL::Wire *wire2 = mod2->wires.at(wire1->name);
+			if (wire1->width != wire2->width || wire1->port_id != wire2->port_id ||
+					wire1->port_input != wire2->port_input || wire1->port_output != wire2->port_output)
+				log_cmd_error("Port %s in module 1 does not match its counterpart in module 2!\n", wire1->name.c_str());
+
+			if (wire1->port_input) {
+				mod1_inputs.append(wire1);
+				mod2_inputs.append(wire2);
+			} else {
+				mod1_outputs.append(wire1);
+				mod2_outputs.append(wire2);
+			}
+		}
+
+		RTLIL::SigSpec inputs;
+		run_checker(inputs);
+	}
+};
+
+} /* namespace */
+
 static void print_proof_failed()
 {
 	log("\n");
@@ -588,6 +670,21 @@ struct SatPass : public Pass {
 				shows.push_back(args[++argidx]);
 				continue;
 			}
+			if (args[argidx] == "-brute_force_equiv_checker" && argidx+2 < args.size()) {
+				/* this should only be used for regression testing of ConstEval -- see tests/xsthammer */
+				std::string mod1_name = RTLIL::escape_id(args[++argidx]);
+				std::string mod2_name = RTLIL::escape_id(args[++argidx]);
+				if (design->modules.count(mod1_name) == 0)
+					log_error("Can't find module `%s'!\n", mod1_name.c_str());
+				if (design->modules.count(mod2_name) == 0)
+					log_error("Can't find module `%s'!\n", mod2_name.c_str());
+				BruteForceEquivChecker checker(design->modules.at(mod1_name), design->modules.at(mod2_name));
+				if (checker.errors > 0)
+					log_cmd_error("Modules are not equivialent!\n");
+				log("Verified %s = %s (using brute-force check on %d cases).\n",
+						mod1_name.c_str(), mod2_name.c_str(), checker.counter);
+				return;
+			}
 			break;
 		}
 		extra_args(args, argidx, design);

tests/xsthammer/run-check.sh

@@ -35,12 +35,15 @@ for mode in nomap techmap; do
 		echo "read_verilog ../../xl_cells.v"
 
 		echo "hierarchy -top ${job}_top"
+		echo "flatten ${job}_xst"
+		echo "flatten ${job}_rtl"
 		echo "flatten ${job}_top"
-		echo "hierarchy -top ${job}_top"
 		echo "opt_clean"
 
+		echo "rename ${job}_xst ${job}_xst_${mode}"
+		echo "rename ${job}_rtl ${job}_rtl_${mode}"
 		echo "rename ${job}_top ${job}_top_${mode}"
-		echo "write_ilang ${job}_top_${mode}.il"
+		echo "dump -outfile ${job}_top_${mode}.il ${job}_xst_${mode} ${job}_rtl_${mode} ${job}_top_${mode}"
 	} > ${job}_top_${mode}.ys
 	../../../../yosys -q ${job}_top_${mode}.ys
 done
@@ -50,6 +53,8 @@ done
 	echo "read_ilang ${job}_top_techmap.il"
 	echo "sat -verify -show a,b,y_rtl,y_xst -prove y_rtl y_xst ${job}_top_nomap"
 	echo "sat -verify -show a,b,y_rtl,y_xst -prove y_rtl y_xst ${job}_top_techmap"
+	echo "sat -brute_force_equiv_checker ${job}_rtl_nomap   ${job}_xst_nomap"
+	echo "sat -brute_force_equiv_checker ${job}_rtl_techmap ${job}_xst_techmap"
 } > ${job}_cmp.ys
 
 if ../../../../yosys -l ${job}.log ${job}_cmp.ys; then