diff options
Diffstat (limited to 'passes/sat')
-rw-r--r-- | passes/sat/Makefile.inc | 1 | ||||
-rw-r--r-- | passes/sat/fminit.cc | 197 | ||||
-rw-r--r-- | passes/sat/sat.cc | 3 |
3 files changed, 200 insertions, 1 deletions
diff --git a/passes/sat/Makefile.inc b/passes/sat/Makefile.inc index fc3ac879e..4bb4b0edc 100644 --- a/passes/sat/Makefile.inc +++ b/passes/sat/Makefile.inc @@ -12,4 +12,5 @@ OBJS += passes/sat/supercover.o OBJS += passes/sat/fmcombine.o OBJS += passes/sat/mutate.o OBJS += passes/sat/cutpoint.o +OBJS += passes/sat/fminit.o diff --git a/passes/sat/fminit.cc b/passes/sat/fminit.cc new file mode 100644 index 000000000..f3f00b382 --- /dev/null +++ b/passes/sat/fminit.cc @@ -0,0 +1,197 @@ +/* + * yosys -- Yosys Open SYnthesis Suite + * + * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at> + * + * Permission to use, copy, modify, and/or distribute this software for any + * purpose with or without fee is hereby granted, provided that the above + * copyright notice and this permission notice appear in all copies. + * + * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES + * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF + * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR + * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES + * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN + * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF + * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. + * + */ + +#include "kernel/yosys.h" +#include "kernel/sigtools.h" + +USING_YOSYS_NAMESPACE +PRIVATE_NAMESPACE_BEGIN + +struct FminitPass : public Pass { + FminitPass() : Pass("fminit", "set init values/sequences for formal") { } + void help() YS_OVERRIDE + { + // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| + log("\n"); + log(" fminit [options] <selection>\n"); + log("\n"); + log("This pass creates init constraints (for example for reset sequences) in a formal\n"); + log("model.\n"); + log("\n"); + log(" -seq <signal> <sequence>\n"); + log(" Set sequence using comma-separated list of values, use 'z for\n"); + log(" unconstrained bits. The last value is used for the remainder of the\n"); + log(" trace.\n"); + log("\n"); + log(" -set <signal> <value>\n"); + log(" Add constant value constraint\n"); + log("\n"); + log(" -posedge <signal>\n"); + log(" -negedge <signal>\n"); + log(" Set clock for init sequences\n"); + log("\n"); + } + void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE + { + vector<pair<string, vector<string>>> initdata; + vector<pair<string, string>> setdata; + string clocksignal; + bool clockedge; + + log_header(design, "Executing FMINIT pass.\n"); + + size_t argidx; + for (argidx = 1; argidx < args.size(); argidx++) + { + // if (args[argidx] == "-o" && argidx+1 < args.size()) { + // filename = args[++argidx]; + // continue; + // } + if (args[argidx] == "-seq" && argidx+2 < args.size()) { + string lhs = args[++argidx]; + string rhs = args[++argidx]; + initdata.push_back(make_pair(lhs, split_tokens(rhs, ","))); + continue; + } + if (args[argidx] == "-set" && argidx+2 < args.size()) { + string lhs = args[++argidx]; + string rhs = args[++argidx]; + setdata.push_back(make_pair(lhs, rhs)); + continue; + } + if (args[argidx] == "-posedge" && argidx+1 < args.size()) { + clocksignal = args[++argidx]; + clockedge = true; + continue; + } + if (args[argidx] == "-negedge" && argidx+1 < args.size()) { + clocksignal = args[++argidx]; + clockedge = true; + continue; + } + break; + } + extra_args(args, argidx, design); + + Module *module = nullptr; + + for (auto mod : design->selected_modules()) { + if (module != nullptr) + log_error("'fminit' requires exactly one module to be selected.\n"); + module = mod; + } + + if (module == nullptr) + log_error("'fminit' requires exactly one module to be selected.\n"); + + SigSpec clksig; + if (!clocksignal.empty()) { + if (!SigSpec::parse(clksig, module, clocksignal)) + log_error("Error parsing expression '%s'.\n", clocksignal.c_str()); + } + + for (auto &it : setdata) + { + SigSpec lhs, rhs; + + if (!SigSpec::parse(lhs, module, it.first)) + log_error("Error parsing expression '%s'.\n", it.first.c_str()); + + if (!SigSpec::parse_rhs(lhs, rhs, module, it.second)) + log_error("Error parsing expression '%s'.\n", it.second.c_str()); + + SigSpec final_lhs, final_rhs; + + for (int i = 0; i < GetSize(rhs); i++) + if (rhs[i] != State::Sz) { + final_lhs.append(lhs[i]); + final_rhs.append(rhs[i]); + } + + if (!final_lhs.empty()) { + SigSpec eq = module->Eq(NEW_ID, final_lhs, final_rhs); + module->addAssume(NEW_ID, eq, State::S1); + } + } + + vector<SigSpec> ctrlsig; + vector<SigSpec> ctrlsig_latched; + + for (auto &it : initdata) + { + SigSpec lhs, rhs; + + if (!SigSpec::parse(lhs, module, it.first)) + log_error("Error parsing expression '%s'.\n", it.first.c_str()); + + for (int i = 0; i < GetSize(it.second); i++) + { + if (i >= GetSize(ctrlsig)) + { + SigSpec insig = i > 0 ? ctrlsig.at(i-1) : State::S0; + + Wire *outwire = module->addWire(NEW_ID); + outwire->attributes[ID(init)] = i > 0 ? State::S0 : State::S1; + + if (clksig.empty()) + module->addFf(NEW_ID, insig, outwire); + else + module->addDff(NEW_ID, clksig, insig, outwire, clockedge); + + ctrlsig.push_back(outwire); + ctrlsig_latched.push_back(SigSpec()); + } + + if (i+1 == GetSize(it.second) && ctrlsig_latched[i].empty()) + { + Wire *ffwire = module->addWire(NEW_ID); + ffwire->attributes[ID(init)] = State::S0; + SigSpec outsig = module->Or(NEW_ID, ffwire, ctrlsig[i]); + + if (clksig.empty()) + module->addFf(NEW_ID, outsig, ffwire); + else + module->addDff(NEW_ID, clksig, outsig, ffwire, clockedge); + + ctrlsig_latched[i] = outsig; + } + + SigSpec ctrl = i+1 == GetSize(it.second) ? ctrlsig_latched[i] : ctrlsig[i]; + + SigSpec final_lhs, final_rhs; + + if (!SigSpec::parse_rhs(lhs, rhs, module, it.second[i])) + log_error("Error parsing expression '%s'.\n", it.second[i].c_str()); + + for (int i = 0; i < GetSize(rhs); i++) + if (rhs[i] != State::Sz) { + final_lhs.append(lhs[i]); + final_rhs.append(rhs[i]); + } + + if (!final_lhs.empty()) { + SigSpec eq = module->Eq(NEW_ID, final_lhs, final_rhs); + module->addAssume(NEW_ID, eq, ctrl); + } + } + } + } +} FminitPass; + +PRIVATE_NAMESPACE_END diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc index 430bba1e8..436ac1b01 100644 --- a/passes/sat/sat.cc +++ b/passes/sat/sat.cc @@ -269,7 +269,8 @@ struct SatHelper for (int i = 0; i < lhs.size(); i++) { RTLIL::SigSpec bit = lhs.extract(i, 1); if (rhs[i] == State::Sx || !satgen.initial_state.check_all(bit)) { - removed_bits.append(bit); + if (rhs[i] != State::Sx) + removed_bits.append(bit); lhs.remove(i, 1); rhs.remove(i, 1); i--; |