+ 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");
+ }
+