Added consteval testing to xsthammer and fixed bugs

diff --git a/kernel/celltypes.h b/kernel/celltypes.h
index cc84251c3b3a573d2b89b49329cd87d92a1b8527..cd72192afc7ecbcb9568e9d50683219cf0073399 100644 (file)
--- a/kernel/celltypes.h
+++ b/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)

diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index 60be79d62c86059f231b7ef48b8bedd302268df8..b192ac01b56750ce9c7c2d48da7d14586bcb6358 100644 (file)
--- a/passes/sat/sat.cc
+++ b/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);

diff --git a/tests/xsthammer/run-check.sh b/tests/xsthammer/run-check.sh
index b2d9193aead5b1756de96ea336f865cbaab32ed5..709eff8169d7a2297cf87c342a6f924fcc15f348 100644 (file)
--- a/tests/xsthammer/run-check.sh
+++ b/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