From 8a815ac74169f62a90511b9b4bda99ceaf5ae774 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sat, 7 Dec 2013 17:28:51 +0100 Subject: [PATCH] Added "sat" undef support and "sat -set-init" options --- kernel/satgen.h | 37 +++++---- passes/sat/sat.cc | 186 ++++++++++++++++++++++++++++++++++++---------- 2 files changed, 170 insertions(+), 53 deletions(-) diff --git a/kernel/satgen.h b/kernel/satgen.h index c2aa4fc2b..35e15aa6c 100644 --- a/kernel/satgen.h +++ b/kernel/satgen.h @@ -98,18 +98,21 @@ struct SatGen return importSigSpecWorker(sig, pf, true, false); } - int signals_eq(RTLIL::SigSpec lhs, RTLIL::SigSpec rhs, int timestep = -1) + int signals_eq(RTLIL::SigSpec lhs, RTLIL::SigSpec rhs, int timestep_lhs = -1, int timestep_rhs = -1) { + if (timestep_rhs < 0) + timestep_rhs = timestep_lhs; + assert(lhs.width == rhs.width); - std::vector vec_lhs = importSigSpec(lhs, timestep); - std::vector vec_rhs = importSigSpec(rhs, timestep); + std::vector vec_lhs = importSigSpec(lhs, timestep_lhs); + std::vector vec_rhs = importSigSpec(rhs, timestep_rhs); if (!model_undef) return ez->vec_eq(vec_lhs, vec_rhs); - std::vector undef_lhs = importUndefSigSpec(lhs, timestep); - std::vector undef_rhs = importUndefSigSpec(rhs, timestep); + std::vector undef_lhs = importUndefSigSpec(lhs, timestep_lhs); + std::vector undef_rhs = importUndefSigSpec(rhs, timestep_rhs); std::vector eq_bits; for (int i = 0; i < lhs.width; i++) @@ -674,18 +677,26 @@ struct SatGen if (timestep > 0 && (cell->type == "$dff" || cell->type == "$_DFF_N_" || cell->type == "$_DFF_P_")) { - if (timestep == 1) { + if (timestep == 1) + { initial_state.add((*sigmap)(cell->connections.at("\\Q"))); - } else { + } + else + { std::vector d = importDefSigSpec(cell->connections.at("\\D"), timestep-1); std::vector q = importDefSigSpec(cell->connections.at("\\Q"), timestep); - ez->assume(ez->vec_eq(d, q)); - } - if (model_undef) { - log("FIXME: No SAT undef model cell type %s!\n", RTLIL::id2cstr(cell->type)); - std::vector undef_y = importUndefSigSpec(cell->connections.at("\\Y"), timestep); - ez->assume(ez->NOT(ez->expression(ezSAT::OpOr, undef_y))); + std::vector qq = model_undef ? ez->vec_var(q.size()) : q; + ez->assume(ez->vec_eq(d, qq)); + + if (model_undef) + { + std::vector undef_d = importUndefSigSpec(cell->connections.at("\\D"), timestep-1); + std::vector undef_q = importUndefSigSpec(cell->connections.at("\\Q"), timestep); + + ez->assume(ez->vec_eq(undef_d, undef_q)); + undefGating(q, qq, undef_q); + } } return true; } diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc index b39ffb23a..bb82c3081 100644 --- a/passes/sat/sat.cc +++ b/passes/sat/sat.cc @@ -44,12 +44,12 @@ struct SatHelper SatGen satgen; // additional constraints - std::vector> sets, prove; + std::vector> sets, prove, sets_init; std::map>> sets_at; std::map> unsets_at; // undef constraints - bool enable_undef; + bool enable_undef, set_init_undef; std::vector sets_def, sets_undef, sets_all_undef; std::map> sets_def_at, sets_undef_at, sets_all_undef_at; @@ -60,15 +60,78 @@ struct SatHelper int max_timestep, timeout; bool gotTimeout; - SatHelper(RTLIL::Design *design, RTLIL::Module *module) : + SatHelper(RTLIL::Design *design, RTLIL::Module *module, bool enable_undef) : design(design), module(module), sigmap(module), ct(design), satgen(&ez, design, &sigmap) { - enable_undef = false; + this->enable_undef = enable_undef; + satgen.model_undef = enable_undef; + set_init_undef = false; max_timestep = -1; timeout = 0; gotTimeout = false; } + void check_undef_enabled(const RTLIL::SigSpec &sig) + { + if (enable_undef) + return; + + std::vector sigbits = sig.to_sigbit_vector(); + for (size_t i = 0; i < sigbits.size(); i++) + if (sigbits[i].wire == NULL && sigbits[i].data == RTLIL::State::Sx) + log_cmd_error("Bit %d of %s is undef but option -enable_undef is missing!\n", int(i), log_signal(sig)); + } + + void setup_init() + { + log ("\nSetting up initial state:\n"); + + RTLIL::SigSpec big_lhs, big_rhs; + + for (auto &s : sets_init) + { + RTLIL::SigSpec lhs, rhs; + + if (!RTLIL::SigSpec::parse(lhs, module, s.first)) + log_cmd_error("Failed to parse lhs set expression `%s'.\n", s.first.c_str()); + if (!RTLIL::SigSpec::parse_rhs(lhs, rhs, module, s.second)) + log_cmd_error("Failed to parse rhs set expression `%s'.\n", s.second.c_str()); + show_signal_pool.add(sigmap(lhs)); + show_signal_pool.add(sigmap(rhs)); + + if (lhs.width != rhs.width) + log_cmd_error("Set expression with different lhs and rhs sizes: %s (%s, %d bits) vs. %s (%s, %d bits)\n", + s.first.c_str(), log_signal(lhs), lhs.width, s.second.c_str(), log_signal(rhs), rhs.width); + + log("Import set-constraint: %s = %s\n", log_signal(lhs), log_signal(rhs)); + big_lhs.remove2(lhs, &big_rhs); + big_lhs.append(lhs); + big_rhs.append(rhs); + } + + if (!satgen.initial_state.check_all(big_lhs)) { + RTLIL::SigSpec rem = satgen.initial_state.remove(big_lhs); + rem.optimize(); + log_cmd_error("Found -set-init bits that are not part of the initial_state: %s\n", log_signal(rem)); + } + + if (set_init_undef) { + RTLIL::SigSpec rem = satgen.initial_state.export_all(); + rem.remove(big_lhs); + big_lhs.append(rem); + big_rhs.append(RTLIL::SigSpec(RTLIL::State::Sx, rem.width)); + } + + if (big_lhs.width == 0) { + log("No constraints for initial state found.\n\n"); + return; + } + + log("Final constraint equation: %s = %s\n\n", log_signal(big_lhs), log_signal(big_rhs)); + check_undef_enabled(big_lhs), check_undef_enabled(big_rhs); + ez.assume(satgen.signals_eq(big_lhs, big_rhs, 1)); + } + void setup(int timestep = -1) { if (timestep > 0) @@ -136,10 +199,8 @@ struct SatHelper } log("Final constraint equation: %s = %s\n", log_signal(big_lhs), log_signal(big_rhs)); - - std::vector lhs_vec = satgen.importSigSpec(big_lhs, timestep); - std::vector rhs_vec = satgen.importSigSpec(big_rhs, timestep); - ez.assume(ez.vec_eq(lhs_vec, rhs_vec)); + check_undef_enabled(big_lhs), check_undef_enabled(big_rhs); + ez.assume(satgen.signals_eq(big_lhs, big_rhs, timestep)); int import_cell_counter = 0; for (auto &c : module->cells) @@ -184,24 +245,19 @@ struct SatHelper } log("Final proof equation: %s = %s\n", log_signal(big_lhs), log_signal(big_rhs)); - - std::vector lhs_vec = satgen.importSigSpec(big_lhs, timestep); - std::vector rhs_vec = satgen.importSigSpec(big_rhs, timestep); - return ez.vec_eq(lhs_vec, rhs_vec); + check_undef_enabled(big_lhs), check_undef_enabled(big_rhs); + return satgen.signals_eq(big_lhs, big_rhs, timestep); } void force_unique_state(int timestep_from, int timestep_to) { RTLIL::SigSpec state_signals = satgen.initial_state.export_all(); for (int i = timestep_from; i < timestep_to; i++) - ez.assume(ez.vec_ne(satgen.importSigSpec(state_signals, i), satgen.importSigSpec(state_signals, timestep_to))); + ez.assume(ez.NOT(satgen.signals_eq(state_signals, state_signals, i, timestep_to))); } bool solve(const std::vector &assumptions) { - // undef is work in progress - log_assert(enable_undef == false); - log_assert(gotTimeout == false); ez.setSolverTimeout(timeout); bool success = ez.solve(modelExpressions, modelValues, assumptions); @@ -212,9 +268,6 @@ struct SatHelper bool solve(int a = 0, int b = 0, int c = 0, int d = 0, int e = 0, int f = 0) { - // undef is work in progress - log_assert(enable_undef == false); - log_assert(gotTimeout == false); ez.setSolverTimeout(timeout); bool success = ez.solve(modelExpressions, modelValues, a, b, c, d, e, f); @@ -293,39 +346,60 @@ struct SatHelper modelSig.sort_and_unify(); // log("Model signals: %s\n", log_signal(modelSig)); + std::vector modelUndefExpressions; + for (auto &c : modelSig.chunks) - if (c.wire != NULL) { + if (c.wire != NULL) + { ModelBlockInfo info; RTLIL::SigSpec chunksig = c; info.width = chunksig.width; info.description = log_signal(chunksig); - for (int timestep = -1; timestep <= max_timestep; timestep++) { + for (int timestep = -1; timestep <= max_timestep; timestep++) + { if ((timestep == -1 && max_timestep > 0) || timestep == 0) continue; - std::vector vec = satgen.importSigSpec(chunksig, timestep); + info.timestep = timestep; info.offset = modelExpressions.size(); - modelExpressions.insert(modelExpressions.end(), vec.begin(), vec.end()); modelInfo.insert(info); + + std::vector vec = satgen.importSigSpec(chunksig, timestep); + modelExpressions.insert(modelExpressions.end(), vec.begin(), vec.end()); + + if (enable_undef) { + std::vector undef_vec = satgen.importUndefSigSpec(chunksig, timestep); + modelUndefExpressions.insert(modelUndefExpressions.end(), undef_vec.begin(), undef_vec.end()); + } } } - // Add zero step signals as collected by satgen - + // Add initial state signals as collected by satgen + // modelSig = satgen.initial_state.export_all(); for (auto &c : modelSig.chunks) - if (c.wire != NULL) { + if (c.wire != NULL) + { ModelBlockInfo info; RTLIL::SigSpec chunksig = c; + info.timestep = 0; info.offset = modelExpressions.size(); info.width = chunksig.width; info.description = log_signal(chunksig); + modelInfo.insert(info); + std::vector vec = satgen.importSigSpec(chunksig, 1); modelExpressions.insert(modelExpressions.end(), vec.begin(), vec.end()); - modelInfo.insert(info); + + if (enable_undef) { + std::vector undef_vec = satgen.importUndefSigSpec(chunksig, 1); + modelUndefExpressions.insert(modelUndefExpressions.end(), undef_vec.begin(), undef_vec.end()); + } } + + modelExpressions.insert(modelExpressions.end(), modelUndefExpressions.begin(), modelUndefExpressions.end()); } void print_model() @@ -344,10 +418,12 @@ struct SatHelper for (auto &info : modelInfo) { RTLIL::Const value; + bool found_undef = false; + for (int i = 0; i < info.width; i++) { value.bits.push_back(modelValues.at(info.offset+i) ? RTLIL::State::S1 : RTLIL::State::S0); - if (modelValues.size() == 2*modelExpressions.size() && modelValues.at(modelExpressions.size()+info.offset+i)) - value.bits.back() = RTLIL::State::Sx; + if (enable_undef && modelValues.at(modelExpressions.size()/2 + info.offset + i)) + value.bits.back() = RTLIL::State::Sx, found_undef = true; } if (info.timestep != last_timestep) { @@ -372,7 +448,7 @@ struct SatHelper } else log(" "); - if (info.width <= 32) + if (info.width <= 32 && !found_undef) log("%-*s %10d %10x %*s\n", maxModelName+10, info.description.c_str(), value.as_int(), value.as_int(), maxModelWidth+5, value.as_string().c_str()); else log("%-*s %10s %10s %*s\n", maxModelName+10, info.description.c_str(), "--", "--", maxModelWidth+5, value.as_string().c_str()); @@ -385,8 +461,15 @@ struct SatHelper void invalidate_model() { std::vector clause; - for (size_t i = 0; i < modelExpressions.size(); i++) - clause.push_back(modelValues.at(i) ? ez.NOT(modelExpressions.at(i)) : modelExpressions.at(i)); + if (enable_undef) { + for (size_t i = 0; i < modelExpressions.size()/2; i++) { + int bit = modelExpressions.at(i), bit_undef = modelExpressions.at(modelExpressions.size()/2 + i); + bool val = modelValues.at(i), val_undef = modelValues.at(modelExpressions.size()/2 + i); + clause.push_back(val_undef ? ez.NOT(bit_undef) : val ? ez.NOT(bit) : bit); + } + } else + for (size_t i = 0; i < modelExpressions.size(); i++) + clause.push_back(modelValues.at(i) ? ez.NOT(modelExpressions.at(i)) : modelExpressions.at(i)); ez.assume(ez.expression(ezSAT::OpOr, clause)); } }; @@ -492,6 +575,12 @@ struct SatPass : public Pass { log(" add undef contraints in the given timestep.\n"); log("\n"); #endif + log(" -set-init \n"); + log(" set the initial value for the register driving the signal to the value\n"); + log("\n"); + log(" -set-init-undef\n"); + log(" set all initial states (not set using -set-init) to undef\n"); + log("\n"); log("The following additional options can be used to set up a proof. If also -seq\n"); log("is passed, a temporal induction proof is performed.\n"); log("\n"); @@ -515,12 +604,12 @@ struct SatPass : public Pass { } virtual void execute(std::vector args, RTLIL::Design *design) { - std::vector> sets, prove; + std::vector> sets, sets_init, prove; std::map>> sets_at; std::map> unsets_at, sets_def_at, sets_undef_at, sets_all_undef_at; std::vector shows, sets_def, sets_undef, sets_all_undef; int loopcount = 0, seq_len = 0, maxsteps = 0, timeout = 0; - bool verify = false, fail_on_timeout = false, enable_undef = false, ignore_div_by_zero = false; + bool verify = false, fail_on_timeout = false, enable_undef = false, ignore_div_by_zero = false, set_init_undef = false; log_header("Executing SAT pass (solving SAT problems in the circuit).\n"); @@ -620,6 +709,17 @@ struct SatPass : public Pass { enable_undef = true; continue; } + if (args[argidx] == "-set-init" && argidx+2 < args.size()) { + std::string lhs = args[++argidx]; + std::string rhs = args[++argidx]; + sets_init.push_back(std::pair(lhs, rhs)); + continue; + } + if (args[argidx] == "-set-init-undef") { + set_init_undef = true; + enable_undef = true; + continue; + } if (args[argidx] == "-show" && argidx+1 < args.size()) { shows.push_back(args[++argidx]); continue; @@ -647,8 +747,8 @@ struct SatPass : public Pass { if (loopcount > 0) log_cmd_error("The options -max and -all are not supported for temporal induction proofs!\n"); - SatHelper basecase(design, module); - SatHelper inductstep(design, module); + SatHelper basecase(design, module, enable_undef); + SatHelper inductstep(design, module, enable_undef); basecase.sets = sets; basecase.prove = prove; @@ -656,29 +756,32 @@ struct SatPass : public Pass { basecase.unsets_at = unsets_at; basecase.shows = shows; basecase.timeout = timeout; - basecase.enable_undef = enable_undef; basecase.sets_def = sets_def; basecase.sets_undef = sets_undef; basecase.sets_all_undef = sets_all_undef; basecase.sets_def_at = sets_def_at; basecase.sets_undef_at = sets_undef_at; basecase.sets_all_undef_at = sets_all_undef_at; + basecase.sets_init = sets_init; + basecase.set_init_undef = set_init_undef; basecase.satgen.ignore_div_by_zero = ignore_div_by_zero; for (int timestep = 1; timestep <= seq_len; timestep++) basecase.setup(timestep); + basecase.setup_init(); inductstep.sets = sets; inductstep.prove = prove; inductstep.shows = shows; inductstep.timeout = timeout; - inductstep.enable_undef = enable_undef; inductstep.sets_def = sets_def; inductstep.sets_undef = sets_undef; inductstep.sets_all_undef = sets_all_undef; inductstep.sets_def_at = sets_def_at; inductstep.sets_undef_at = sets_undef_at; inductstep.sets_all_undef_at = sets_all_undef_at; + inductstep.sets_init = sets_init; + inductstep.set_init_undef = set_init_undef; inductstep.satgen.ignore_div_by_zero = ignore_div_by_zero; inductstep.setup(1); @@ -755,20 +858,22 @@ struct SatPass : public Pass { if (maxsteps > 0) log_cmd_error("The options -maxsteps is only supported for temporal induction proofs!\n"); - SatHelper sathelper(design, module); + SatHelper sathelper(design, module, enable_undef); + sathelper.sets = sets; sathelper.prove = prove; sathelper.sets_at = sets_at; sathelper.unsets_at = unsets_at; sathelper.shows = shows; sathelper.timeout = timeout; - sathelper.enable_undef = enable_undef; sathelper.sets_def = sets_def; sathelper.sets_undef = sets_undef; sathelper.sets_all_undef = sets_all_undef; sathelper.sets_def_at = sets_def_at; sathelper.sets_undef_at = sets_undef_at; sathelper.sets_all_undef_at = sets_all_undef_at; + sathelper.sets_init = sets_init; + sathelper.set_init_undef = set_init_undef; sathelper.satgen.ignore_div_by_zero = ignore_div_by_zero; if (seq_len == 0) { @@ -778,6 +883,7 @@ struct SatPass : public Pass { } else { for (int timestep = 1; timestep <= seq_len; timestep++) sathelper.setup(timestep); + sathelper.setup_init(); } sathelper.generate_model(); -- 2.30.2