From: Clifford Wolf Date: Thu, 13 Jun 2013 17:51:13 +0000 (+0200) Subject: Added consteval testing to xsthammer and fixed bugs X-Git-Tag: yosys-0.2.0~572 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=30db70b1baaad1f299234b419ac2dc581eee1e14;p=yosys.git Added consteval testing to xsthammer and fixed bugs --- diff --git a/kernel/celltypes.h b/kernel/celltypes.h index cc84251c3..cd72192af 100644 --- 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 60be79d62..b192ac01b 100644 --- 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 b2d9193ae..709eff816 100644 --- 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