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 &it : module->wires_)
- {
- if (it.second->attributes.count("\\init") == 0)
- continue;
-
- RTLIL::SigSpec lhs = sigmap(it.second);
- RTLIL::SigSpec rhs = it.second->attributes.at("\\init");
- log_assert(lhs.size() == rhs.size());
-
- RTLIL::SigSpec removed_bits;
- for (int i = 0; i < lhs.size(); i++) {
- RTLIL::SigSpec bit = lhs.extract(i, 1);
- if (!satgen.initial_state.check_all(bit)) {
- removed_bits.append(bit);
- lhs.remove(i, 1);
- rhs.remove(i, 1);
- i--;
- }
- }
-
- if (removed_bits.size())
- log_warning("ignoring initial value on non-register: %s\n", log_signal(removed_bits));
-
- if (lhs.size()) {
- log("Import set-constraint from init attribute: %s = %s\n", log_signal(lhs), log_signal(rhs));
- big_lhs.remove2(lhs, &big_rhs);
- big_lhs.append(lhs);
- big_rhs.append(rhs);
- }
- }
-
- for (auto &s : sets_init)
- {
- RTLIL::SigSpec lhs, rhs;
-
- if (!RTLIL::SigSpec::parse_sel(lhs, design, 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.size() != rhs.size())
- 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.size(), s.second.c_str(), log_signal(rhs), rhs.size());
-
- 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);
- log_cmd_error("Found -set-init bits that are not part of the initial_state: %s\n", log_signal(rem));
- }
-
- if (set_init_def) {
- RTLIL::SigSpec rem = satgen.initial_state.export_all();
- std::vector<int> undef_rem = satgen.importUndefSigSpec(rem, 1);
- ez->assume(ez->NOT(ez->expression(ezSAT::OpOr, undef_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.size()));
- }
-
- if (set_init_zero) {
- RTLIL::SigSpec rem = satgen.initial_state.export_all();
- rem.remove(big_lhs);
- big_lhs.append(rem);
- big_rhs.append(RTLIL::SigSpec(RTLIL::State::S0, rem.size()));
- }
-
- if (big_lhs.size() == 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)
+ void setup(int timestep = -1, bool initstate = false)
{
if (timestep > 0)
log ("\nSetting up time step %d:\n", timestep);
else
log ("\nSetting up SAT problem:\n");
+ if (initstate)
+ satgen.setInitState(timestep);
+
if (timestep > max_timestep)
max_timestep = timestep;
log("Import constraint from assume cell: %s when %s.\n", log_signal(assumes_a[i]), log_signal(assumes_en[i]));
ez->assume(satgen.importAssumes(timestep));
}
+
+ if (initstate)
+ {
+ RTLIL::SigSpec big_lhs, big_rhs;
+
+ for (auto &it : module->wires_)
+ {
+ if (it.second->attributes.count("\\init") == 0)
+ continue;
+
+ RTLIL::SigSpec lhs = sigmap(it.second);
+ RTLIL::SigSpec rhs = it.second->attributes.at("\\init");
+ log_assert(lhs.size() == rhs.size());
+
+ RTLIL::SigSpec removed_bits;
+ for (int i = 0; i < lhs.size(); i++) {
+ RTLIL::SigSpec bit = lhs.extract(i, 1);
+ if (!satgen.initial_state.check_all(bit)) {
+ removed_bits.append(bit);
+ lhs.remove(i, 1);
+ rhs.remove(i, 1);
+ i--;
+ }
+ }
+
+ if (removed_bits.size())
+ log_warning("ignoring initial value on non-register: %s\n", log_signal(removed_bits));
+
+ if (lhs.size()) {
+ log("Import set-constraint from init attribute: %s = %s\n", log_signal(lhs), log_signal(rhs));
+ big_lhs.remove2(lhs, &big_rhs);
+ big_lhs.append(lhs);
+ big_rhs.append(rhs);
+ }
+ }
+
+ for (auto &s : sets_init)
+ {
+ RTLIL::SigSpec lhs, rhs;
+
+ if (!RTLIL::SigSpec::parse_sel(lhs, design, 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.size() != rhs.size())
+ 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.size(), s.second.c_str(), log_signal(rhs), rhs.size());
+
+ log("Import init 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);
+ log_cmd_error("Found -set-init bits that are not part of the initial_state: %s\n", log_signal(rem));
+ }
+
+ if (set_init_def) {
+ RTLIL::SigSpec rem = satgen.initial_state.export_all();
+ std::vector<int> undef_rem = satgen.importUndefSigSpec(rem, 1);
+ ez->assume(ez->NOT(ez->expression(ezSAT::OpOr, undef_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.size()));
+ }
+
+ if (set_init_zero) {
+ RTLIL::SigSpec rem = satgen.initial_state.export_all();
+ rem.remove(big_lhs);
+ big_lhs.append(rem);
+ big_rhs.append(RTLIL::SigSpec(RTLIL::State::S0, rem.size()));
+ }
+
+ if (big_lhs.size() == 0) {
+ log("No constraints for initial state found.\n\n");
+ return;
+ }
+
+ log("Final init constraint equation: %s = %s\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, timestep));
+ }
}
int setup_proof(int timestep = -1)
int maxModelWidth = 10;
for (auto &info : modelInfo) {
- maxModelName = std::max(maxModelName, int(info.description.size()));
- maxModelWidth = std::max(maxModelWidth, info.width);
+ maxModelName = max(maxModelName, int(info.description.size()));
+ maxModelWidth = max(maxModelWidth, info.width);
}
log("\n");
"---------------------------------------------------------------------------------------------------";
if (last_timestep == -2) {
log(max_timestep > 0 ? " Time " : " ");
- log("%-*s %10s %10s %*s\n", maxModelName+10, "Signal Name", "Dec", "Hex", maxModelWidth+5, "Bin");
+ log("%-*s %11s %9s %*s\n", maxModelName+5, "Signal Name", "Dec", "Hex", maxModelWidth+3, "Bin");
}
log(max_timestep > 0 ? " ---- " : " ");
- log("%*.*s %10.10s %10.10s %*.*s\n", maxModelName+10, maxModelName+10,
- hline, hline, hline, maxModelWidth+5, maxModelWidth+5, hline);
+ log("%*.*s %11.11s %9.9s %*.*s\n", maxModelName+5, maxModelName+5,
+ hline, hline, hline, maxModelWidth+3, maxModelWidth+3, hline);
last_timestep = info.timestep;
}
log(" ");
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());
+ log("%-*s %11d %9x %*s\n", maxModelName+5, info.description.c_str(), value.as_int(), value.as_int(), maxModelWidth+3, 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());
+ log("%-*s %11s %9s %*s\n", maxModelName+5, info.description.c_str(), "--", "--", maxModelWidth+3, value.as_string().c_str());
}
if (last_timestep == -2)
void dump_model_to_vcd(std::string vcd_file_name)
{
+ rewrite_filename(vcd_file_name);
FILE *f = fopen(vcd_file_name.c_str(), "w");
if (!f)
log_cmd_error("Can't open output file `%s' for writing: %s\n", vcd_file_name.c_str(), strerror(errno));
// VCD has some limits on internal (non-display) identifier names, so make legal ones
std::map<std::string, std::string> vcdnames;
- fprintf(f, "$timescale 1ns\n"); // arbitrary time scale since actual clock period is unknown/unimportant
fprintf(f, "$scope module %s $end\n", module->name.c_str());
for (auto &info : modelInfo)
{
void dump_model_to_json(std::string json_file_name)
{
+ rewrite_filename(json_file_name);
FILE *f = fopen(json_file_name.c_str(), "w");
if (!f)
log_cmd_error("Can't open output file `%s' for writing: %s\n", json_file_name.c_str(), strerror(errno));
wavedata[info.description].first = info.width;
wavedata[info.description].second[info.timestep] = value;
- mintime = std::min(mintime, info.timestep);
- maxtime = std::max(maxtime, info.timestep);
- maxwidth = std::max(maxwidth, info.width);
+ mintime = min(mintime, info.timestep);
+ maxtime = max(maxtime, info.timestep);
+ maxwidth = max(maxwidth, info.width);
}
fprintf(f, "{ \"signal\": [");
struct SatPass : public Pass {
SatPass() : Pass("sat", "solve a SAT problem in the circuit") { }
- virtual void help()
+ void help() YS_OVERRIDE
{
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n");
log(" -show-inputs, -show-outputs, -show-ports\n");
log(" add all module (input/output) ports to the list of shown signals\n");
log("\n");
+ log(" -show-regs, -show-public, -show-all\n");
+ log(" show all registers, show signals with 'public' names, show all signals\n");
+ log("\n");
log(" -ignore_div_by_zero\n");
log(" ignore all solutions that involve a division by zero\n");
log("\n");
log("is passed, a temporal induction proof is performed.\n");
log("\n");
log(" -tempinduct\n");
- log(" Perform a temporal induction proof. In a temporalinduction proof it is\n");
+ log(" Perform a temporal induction proof. In a temporal induction proof it is\n");
log(" proven that the condition holds forever after the number of time steps\n");
log(" specified using -seq.\n");
log("\n");
log("\n");
log(" -prove-x <signal> <value>\n");
log(" Like -prove, but an undef (x) bit in the lhs matches any value on\n");
- log(" the right hand side. Useful for equivialence checking.\n");
+ log(" the right hand side. Useful for equivalence checking.\n");
log("\n");
log(" -prove-asserts\n");
log(" Prove that all asserts in the design hold.\n");
log(" Like -falsify but do not return an error for timeouts.\n");
log("\n");
}
- virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
+ void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
{
std::vector<std::pair<std::string, std::string>> sets, sets_init, prove, prove_x;
std::map<int, std::vector<std::pair<std::string, std::string>>> sets_at;
bool verify = false, fail_on_timeout = false, enable_undef = false, set_def_inputs = false;
bool ignore_div_by_zero = false, set_init_undef = false, set_init_zero = false, max_undef = false;
bool tempinduct = false, prove_asserts = false, show_inputs = false, show_outputs = false;
+ bool show_regs = false, show_public = false, show_all = false;
bool ignore_unknown_cells = false, falsify = false, tempinduct_def = false, set_init_def = false;
bool tempinduct_baseonly = false, tempinduct_inductonly = false, set_assumes = false;
int tempinduct_skip = 0, stepsize = 1;
std::string vcd_file_name, json_file_name, cnf_file_name;
- log_header("Executing SAT pass (solving SAT problems in the circuit).\n");
+ log_header(design, "Executing SAT pass (solving SAT problems in the circuit).\n");
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++) {
continue;
}
if (args[argidx] == "-stepsize" && argidx+1 < args.size()) {
- stepsize = std::max(1, atoi(args[++argidx].c_str()));
+ stepsize = max(1, atoi(args[++argidx].c_str()));
continue;
}
if (args[argidx] == "-ignore_div_by_zero") {
if (args[argidx] == "-tempinduct-def") {
tempinduct = true;
tempinduct_def = true;
+ enable_undef = true;
continue;
}
if (args[argidx] == "-tempinduct-baseonly") {
show_outputs = true;
continue;
}
+ if (args[argidx] == "-show-regs") {
+ show_regs = true;
+ continue;
+ }
+ if (args[argidx] == "-show-public") {
+ show_public = true;
+ continue;
+ }
+ if (args[argidx] == "-show-all") {
+ show_all = true;
+ continue;
+ }
if (args[argidx] == "-ignore_unknown_cells") {
ignore_unknown_cells = true;
continue;
shows.push_back(it.second->name.str());
}
+ if (show_regs) {
+ pool<Wire*> reg_wires;
+ for (auto cell : module->cells()) {
+ if (cell->type == "$dff" || cell->type.substr(0, 6) == "$_DFF_")
+ for (auto bit : cell->getPort("\\Q"))
+ if (bit.wire)
+ reg_wires.insert(bit.wire);
+ }
+ for (auto wire : reg_wires)
+ shows.push_back(wire->name.str());
+ }
+
+ if (show_public) {
+ for (auto wire : module->wires())
+ if (wire->name[0] == '\\')
+ shows.push_back(wire->name.str());
+ }
+
+ if (show_all) {
+ for (auto wire : module->wires())
+ shows.push_back(wire->name.str());
+ }
+
if (tempinduct)
{
if (loopcount > 0 || max_undef)
SatHelper basecase(design, module, enable_undef);
SatHelper inductstep(design, module, enable_undef);
- bool basecase_setup_init = true;
basecase.sets = sets;
basecase.set_assumes = set_assumes;
for (int timestep = 1; timestep <= seq_len; timestep++)
if (!tempinduct_inductonly)
- basecase.setup(timestep);
+ basecase.setup(timestep, timestep == 1);
inductstep.sets = sets;
inductstep.set_assumes = set_assumes;
if (!tempinduct_inductonly)
{
- basecase.setup(seq_len + inductlen);
+ basecase.setup(seq_len + inductlen, seq_len + inductlen == 1);
int property = basecase.setup_proof(seq_len + inductlen);
basecase.generate_model();
- if (basecase_setup_init) {
- basecase.setup_init();
- basecase_setup_init = false;
- }
-
if (inductlen > 1)
basecase.force_unique_state(seq_len + 1, seq_len + inductlen);
{
log("\n[base case %d] Solving problem with %d variables and %d clauses..\n",
inductlen, basecase.ez->numCnfVariables(), basecase.ez->numCnfClauses());
+ log_flush();
if (basecase.solve(basecase.ez->NOT(property))) {
log("SAT temporal induction proof finished - model found for base case: FAIL!\n");
{
if (!cnf_file_name.empty())
{
+ rewrite_filename(cnf_file_name);
FILE *f = fopen(cnf_file_name.c_str(), "w");
if (!f)
log_cmd_error("Can't open output file `%s' for writing: %s\n", cnf_file_name.c_str(), strerror(errno));
log("\n[induction step %d] Solving problem with %d variables and %d clauses..\n",
inductlen, inductstep.ez->numCnfVariables(), inductstep.ez->numCnfClauses());
+ log_flush();
if (!inductstep.solve(inductstep.ez->NOT(property))) {
if (inductstep.gotTimeout)
} else {
std::vector<int> prove_bits;
for (int timestep = 1; timestep <= seq_len; timestep++) {
- sathelper.setup(timestep);
+ sathelper.setup(timestep, timestep == 1);
if (sathelper.prove.size() || sathelper.prove_x.size() || sathelper.prove_asserts)
if (timestep > prove_skip)
prove_bits.push_back(sathelper.setup_proof(timestep));
}
if (sathelper.prove.size() || sathelper.prove_x.size() || sathelper.prove_asserts)
sathelper.ez->assume(sathelper.ez->NOT(sathelper.ez->expression(ezSAT::OpAnd, prove_bits)));
- sathelper.setup_init();
}
sathelper.generate_model();
if (!cnf_file_name.empty())
{
+ rewrite_filename(cnf_file_name);
FILE *f = fopen(cnf_file_name.c_str(), "w");
if (!f)
log_cmd_error("Can't open output file `%s' for writing: %s\n", cnf_file_name.c_str(), strerror(errno));
rerun_solver:
log("\nSolving problem with %d variables and %d clauses..\n",
sathelper.ez->numCnfVariables(), sathelper.ez->numCnfClauses());
+ log_flush();
if (sathelper.solve())
{
projects / yosys.git / blobdiff