* 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
#include <stdlib.h>
#include <stdio.h>
#include <algorithm>
+#include <errno.h>
+#include <string.h>
-namespace {
+USING_YOSYS_NAMESPACE
+PRIVATE_NAMESPACE_BEGIN
struct SatHelper
{
RTLIL::Design *design;
RTLIL::Module *module;
- ezDefaultSAT ez;
SigMap sigmap;
CellTypes ct;
+
+ ezSatPtr ez;
SatGen satgen;
// additional constraints
std::vector<std::pair<std::string, std::string>> sets, prove, prove_x, sets_init;
std::map<int, std::vector<std::pair<std::string, std::string>>> sets_at;
std::map<int, std::vector<std::string>> unsets_at;
- bool prove_asserts;
+ bool prove_asserts, set_assumes;
// undef constraints
- bool enable_undef, set_init_undef, ignore_unknown_cells;
+ bool enable_undef, set_init_def, set_init_undef, set_init_zero, ignore_unknown_cells;
std::vector<std::string> sets_def, sets_any_undef, sets_all_undef;
std::map<int, std::vector<std::string>> sets_def_at, sets_any_undef_at, sets_all_undef_at;
bool gotTimeout;
SatHelper(RTLIL::Design *design, RTLIL::Module *module, bool enable_undef) :
- design(design), module(module), sigmap(module), ct(design), satgen(&ez, &sigmap)
+ design(design), module(module), sigmap(module), ct(design), satgen(ez.get(), &sigmap)
{
this->enable_undef = enable_undef;
satgen.model_undef = enable_undef;
+ set_init_def = false;
set_init_undef = false;
+ set_init_zero = false;
ignore_unknown_cells = false;
max_timestep = -1;
timeout = 0;
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.width == rhs.width);
-
- 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(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)
+ 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;
{
RTLIL::SigSpec lhs, rhs;
- if (!RTLIL::SigSpec::parse(lhs, module, s.first))
+ 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.width != rhs.width)
+ 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.width, s.second.c_str(), log_signal(rhs), rhs.width);
+ 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);
{
RTLIL::SigSpec lhs, rhs;
- if (!RTLIL::SigSpec::parse(lhs, module, s.first))
+ 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.width != rhs.width)
+ 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.width, s.second.c_str(), log_signal(rhs), rhs.width);
+ s.first.c_str(), log_signal(lhs), lhs.size(), s.second.c_str(), log_signal(rhs), rhs.size());
- log("Import set-constraint for timestep: %s = %s\n", log_signal(lhs), log_signal(rhs));
+ log("Import set-constraint for this timestep: %s = %s\n", log_signal(lhs), log_signal(rhs));
big_lhs.remove2(lhs, &big_rhs);
big_lhs.append(lhs);
big_rhs.append(rhs);
{
RTLIL::SigSpec lhs;
- if (!RTLIL::SigSpec::parse(lhs, module, s))
+ if (!RTLIL::SigSpec::parse_sel(lhs, design, module, s))
log_cmd_error("Failed to parse lhs set expression `%s'.\n", s.c_str());
show_signal_pool.add(sigmap(lhs));
- log("Import unset-constraint for timestep: %s\n", log_signal(lhs));
+ log("Import unset-constraint for this timestep: %s\n", log_signal(lhs));
big_lhs.remove2(lhs, &big_rhs);
}
log("Final 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));
+ ez->assume(satgen.signals_eq(big_lhs, big_rhs, timestep));
// 0 = sets_def
// 1 = sets_any_undef
for (auto &s : sets_def) {
RTLIL::SigSpec sig;
- if (!RTLIL::SigSpec::parse(sig, module, s))
+ if (!RTLIL::SigSpec::parse_sel(sig, design, module, s))
log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
sets_def_undef[0].insert(sig);
}
for (auto &s : sets_any_undef) {
RTLIL::SigSpec sig;
- if (!RTLIL::SigSpec::parse(sig, module, s))
+ if (!RTLIL::SigSpec::parse_sel(sig, design, module, s))
log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
sets_def_undef[1].insert(sig);
}
for (auto &s : sets_all_undef) {
RTLIL::SigSpec sig;
- if (!RTLIL::SigSpec::parse(sig, module, s))
+ if (!RTLIL::SigSpec::parse_sel(sig, design, module, s))
log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
sets_def_undef[2].insert(sig);
}
for (auto &s : sets_def_at[timestep]) {
RTLIL::SigSpec sig;
- if (!RTLIL::SigSpec::parse(sig, module, s))
+ if (!RTLIL::SigSpec::parse_sel(sig, design, module, s))
log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
sets_def_undef[0].insert(sig);
sets_def_undef[1].erase(sig);
for (auto &s : sets_any_undef_at[timestep]) {
RTLIL::SigSpec sig;
- if (!RTLIL::SigSpec::parse(sig, module, s))
+ if (!RTLIL::SigSpec::parse_sel(sig, design, module, s))
log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
sets_def_undef[0].erase(sig);
sets_def_undef[1].insert(sig);
for (auto &s : sets_all_undef_at[timestep]) {
RTLIL::SigSpec sig;
- if (!RTLIL::SigSpec::parse(sig, module, s))
+ if (!RTLIL::SigSpec::parse_sel(sig, design, module, s))
log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
sets_def_undef[0].erase(sig);
sets_def_undef[1].erase(sig);
for (int t = 0; t < 3; t++)
for (auto &sig : sets_def_undef[t]) {
- log("Import %s constraint for timestep: %s\n", t == 0 ? "def" : t == 1 ? "any_undef" : "all_undef", log_signal(sig));
+ log("Import %s constraint for this timestep: %s\n", t == 0 ? "def" : t == 1 ? "any_undef" : "all_undef", log_signal(sig));
std::vector<int> undef_sig = satgen.importUndefSigSpec(sig, timestep);
if (t == 0)
- ez.assume(ez.NOT(ez.expression(ezSAT::OpOr, undef_sig)));
+ ez->assume(ez->NOT(ez->expression(ezSAT::OpOr, undef_sig)));
if (t == 1)
- ez.assume(ez.expression(ezSAT::OpOr, undef_sig));
+ ez->assume(ez->expression(ezSAT::OpOr, undef_sig));
if (t == 2)
- ez.assume(ez.expression(ezSAT::OpAnd, undef_sig));
+ ez->assume(ez->expression(ezSAT::OpAnd, undef_sig));
}
int import_cell_counter = 0;
- for (auto &c : module->cells)
- if (design->selected(module, c.second)) {
- // log("Import cell: %s\n", RTLIL::id2cstr(c.first));
- if (satgen.importCell(c.second, timestep)) {
- for (auto &p : c.second->connections)
- if (ct.cell_output(c.second->type, p.first))
- show_drivers.insert(sigmap(p.second), c.second);
+ for (auto cell : module->cells())
+ if (design->selected(module, cell)) {
+ // log("Import cell: %s\n", RTLIL::id2cstr(cell->name));
+ if (satgen.importCell(cell, timestep)) {
+ for (auto &p : cell->connections())
+ if (ct.cell_output(cell->type, p.first))
+ show_drivers.insert(sigmap(p.second), cell);
import_cell_counter++;
} else if (ignore_unknown_cells)
- log("Warning: Failed to import cell %s (type %s) to SAT database.\n", RTLIL::id2cstr(c.first), RTLIL::id2cstr(c.second->type));
+ log_warning("Failed to import cell %s (type %s) to SAT database.\n", RTLIL::id2cstr(cell->name), RTLIL::id2cstr(cell->type));
else
- log_error("Failed to import cell %s (type %s) to SAT database.\n", RTLIL::id2cstr(c.first), RTLIL::id2cstr(c.second->type));
+ log_error("Failed to import cell %s (type %s) to SAT database.\n", RTLIL::id2cstr(cell->name), RTLIL::id2cstr(cell->type));
}
log("Imported %d cells to SAT database.\n", import_cell_counter);
+
+ if (set_assumes) {
+ RTLIL::SigSpec assumes_a, assumes_en;
+ satgen.getAssumes(assumes_a, assumes_en, timestep);
+ for (int i = 0; i < GetSize(assumes_a); i++)
+ 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)
{
- assert(prove.size() || prove_x.size() || prove_asserts);
+ log_assert(prove.size() || prove_x.size() || prove_asserts);
RTLIL::SigSpec big_lhs, big_rhs;
std::vector<int> prove_bits;
{
RTLIL::SigSpec lhs, rhs;
- if (!RTLIL::SigSpec::parse(lhs, module, s.first))
+ if (!RTLIL::SigSpec::parse_sel(lhs, design, module, s.first))
log_cmd_error("Failed to parse lhs proof expression `%s'.\n", s.first.c_str());
if (!RTLIL::SigSpec::parse_rhs(lhs, rhs, module, s.second))
log_cmd_error("Failed to parse rhs proof expression `%s'.\n", s.second.c_str());
show_signal_pool.add(sigmap(lhs));
show_signal_pool.add(sigmap(rhs));
- if (lhs.width != rhs.width)
+ if (lhs.size() != rhs.size())
log_cmd_error("Proof 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);
+ s.first.c_str(), log_signal(lhs), lhs.size(), s.second.c_str(), log_signal(rhs), rhs.size());
log("Import proof-constraint: %s = %s\n", log_signal(lhs), log_signal(rhs));
big_lhs.remove2(lhs, &big_rhs);
{
RTLIL::SigSpec lhs, rhs;
- if (!RTLIL::SigSpec::parse(lhs, module, s.first))
+ if (!RTLIL::SigSpec::parse_sel(lhs, design, module, s.first))
log_cmd_error("Failed to parse lhs proof-x expression `%s'.\n", s.first.c_str());
if (!RTLIL::SigSpec::parse_rhs(lhs, rhs, module, s.second))
log_cmd_error("Failed to parse rhs proof-x expression `%s'.\n", s.second.c_str());
show_signal_pool.add(sigmap(lhs));
show_signal_pool.add(sigmap(rhs));
- if (lhs.width != rhs.width)
+ if (lhs.size() != rhs.size())
log_cmd_error("Proof-x 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);
+ s.first.c_str(), log_signal(lhs), lhs.size(), s.second.c_str(), log_signal(rhs), rhs.size());
log("Import proof-x-constraint: %s = %s\n", log_signal(lhs), log_signal(rhs));
big_lhs.remove2(lhs, &big_rhs);
std::vector<int> undef_rhs = satgen.importUndefSigSpec(big_rhs, timestep);
for (size_t i = 0; i < value_lhs.size(); i++)
- prove_bits.push_back(ez.OR(undef_lhs.at(i), ez.AND(ez.NOT(undef_rhs.at(i)), ez.NOT(ez.XOR(value_lhs.at(i), value_rhs.at(i))))));
+ prove_bits.push_back(ez->OR(undef_lhs.at(i), ez->AND(ez->NOT(undef_rhs.at(i)), ez->NOT(ez->XOR(value_lhs.at(i), value_rhs.at(i))))));
}
if (prove_asserts) {
RTLIL::SigSpec asserts_a, asserts_en;
satgen.getAsserts(asserts_a, asserts_en, timestep);
- asserts_a.expand();
- asserts_en.expand();
- for (size_t i = 0; i < asserts_a.chunks.size(); i++)
- log("Import proof for assert: %s when %s.\n", log_signal(asserts_a.chunks[i]), log_signal(asserts_en.chunks[i]));
+ for (int i = 0; i < GetSize(asserts_a); i++)
+ log("Import proof for assert: %s when %s.\n", log_signal(asserts_a[i]), log_signal(asserts_en[i]));
prove_bits.push_back(satgen.importAsserts(timestep));
}
- return ez.expression(ezSAT::OpAnd, prove_bits);
+ return ez->expression(ezSAT::OpAnd, prove_bits);
}
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.NOT(satgen.signals_eq(state_signals, state_signals, i, timestep_to)));
+ ez->assume(ez->NOT(satgen.signals_eq(state_signals, state_signals, i, timestep_to)));
}
bool solve(const std::vector<int> &assumptions)
{
log_assert(gotTimeout == false);
- ez.setSolverTimeout(timeout);
- bool success = ez.solve(modelExpressions, modelValues, assumptions);
- if (ez.getSolverTimoutStatus())
+ ez->setSolverTimeout(timeout);
+ bool success = ez->solve(modelExpressions, modelValues, assumptions);
+ if (ez->getSolverTimoutStatus())
gotTimeout = true;
return success;
}
bool solve(int a = 0, int b = 0, int c = 0, int d = 0, int e = 0, int f = 0)
{
log_assert(gotTimeout == false);
- ez.setSolverTimeout(timeout);
- bool success = ez.solve(modelExpressions, modelValues, a, b, c, d, e, f);
- if (ez.getSolverTimoutStatus())
+ ez->setSolverTimeout(timeout);
+ bool success = ez->solve(modelExpressions, modelValues, a, b, c, d, e, f);
+ if (ez->getSolverTimoutStatus())
gotTimeout = true;
return success;
}
maybe_undef.push_back(modelExpressions.at(modelExpressions.size()/2 + i));
backupValues.swap(modelValues);
- if (!solve(ez.expression(ezSAT::OpAnd, must_undef), ez.expression(ezSAT::OpOr, maybe_undef)))
+ if (!solve(ez->expression(ezSAT::OpAnd, must_undef), ez->expression(ezSAT::OpOr, maybe_undef)))
break;
}
final_signals.add(sig);
} else {
for (auto &d : drivers)
- for (auto &p : d->connections) {
+ for (auto &p : d->connections()) {
if (d->type == "$dff" && p.first == "\\CLK")
continue;
if (d->type.substr(0, 6) == "$_DFF_" && p.first == "\\C")
{
for (auto &s : shows) {
RTLIL::SigSpec sig;
- if (!RTLIL::SigSpec::parse(sig, module, s))
+ if (!RTLIL::SigSpec::parse_sel(sig, design, module, s))
log_cmd_error("Failed to parse show expression `%s'.\n", s.c_str());
log("Import show expression: %s\n", log_signal(sig));
modelSig.append(sig);
std::vector<int> modelUndefExpressions;
- for (auto &c : modelSig.chunks)
+ for (auto &c : modelSig.chunks())
if (c.wire != NULL)
{
ModelBlockInfo info;
RTLIL::SigSpec chunksig = c;
- info.width = chunksig.width;
+ info.width = chunksig.size();
info.description = log_signal(chunksig);
for (int timestep = -1; timestep <= max_timestep; timestep++)
// Add initial state signals as collected by satgen
//
modelSig = satgen.initial_state.export_all();
- for (auto &c : modelSig.chunks)
+ for (auto &c : modelSig.chunks())
if (c.wire != NULL)
{
ModelBlockInfo info;
info.timestep = 0;
info.offset = modelExpressions.size();
- info.width = chunksig.width;
+ info.width = chunksig.size();
info.description = log_signal(chunksig);
modelInfo.insert(info);
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)
+ log(" no model variables selected for display.\n");
+ }
+
+ 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));
+
+ log("Dumping SAT model to VCD file %s\n", vcd_file_name.c_str());
+
+ time_t timestamp;
+ struct tm* now;
+ char stime[128] = {};
+ time(×tamp);
+ now = localtime(×tamp);
+ strftime(stime, sizeof(stime), "%c", now);
+
+ std::string module_fname = "unknown";
+ auto apos = module->attributes.find("\\src");
+ if(apos != module->attributes.end())
+ module_fname = module->attributes["\\src"].decode_string();
+
+ fprintf(f, "$date\n");
+ fprintf(f, " %s\n", stime);
+ fprintf(f, "$end\n");
+ fprintf(f, "$version\n");
+ fprintf(f, " Generated by %s\n", yosys_version_str);
+ fprintf(f, "$end\n");
+ fprintf(f, "$comment\n");
+ fprintf(f, " Generated from SAT problem in module %s (declared at %s)\n",
+ module->name.c_str(), module_fname.c_str());
+ fprintf(f, "$end\n");
+
+ // VCD has some limits on internal (non-display) identifier names, so make legal ones
+ std::map<std::string, std::string> vcdnames;
+
+ fprintf(f, "$scope module %s $end\n", module->name.c_str());
+ for (auto &info : modelInfo)
+ {
+ if (vcdnames.find(info.description) != vcdnames.end())
+ continue;
+
+ char namebuf[16];
+ snprintf(namebuf, sizeof(namebuf), "v%d", static_cast<int>(vcdnames.size()));
+ vcdnames[info.description] = namebuf;
+
+ // Even display identifiers can't use some special characters
+ std::string legal_desc = info.description.c_str();
+ for (auto &c : legal_desc) {
+ if(c == '$')
+ c = '_';
+ if(c == ':')
+ c = '_';
+ }
+
+ fprintf(f, "$var wire %d %s %s $end\n", info.width, namebuf, legal_desc.c_str());
+
+ // Need to look at first *two* cycles!
+ // We need to put a name on all variables but those without an initialization clause
+ // have no value at timestep 0
+ if(info.timestep > 1)
+ break;
+ }
+ fprintf(f, "$upscope $end\n");
+ fprintf(f, "$enddefinitions $end\n");
+ fprintf(f, "$dumpvars\n");
+
+ static const char bitvals[] = "01xzxx";
+
+ int last_timestep = -2;
+ for (auto &info : modelInfo)
+ {
+ RTLIL::Const value;
+
+ for (int i = 0; i < info.width; i++) {
+ value.bits.push_back(modelValues.at(info.offset+i) ? RTLIL::State::S1 : RTLIL::State::S0);
+ if (enable_undef && modelValues.at(modelExpressions.size()/2 + info.offset + i))
+ value.bits.back() = RTLIL::State::Sx;
+ }
+
+ if (info.timestep != last_timestep) {
+ if(last_timestep == 0)
+ fprintf(f, "$end\n");
+ else
+ fprintf(f, "#%d\n", info.timestep);
+ last_timestep = info.timestep;
+ }
+
+ if(info.width == 1) {
+ fprintf(f, "%c%s\n", bitvals[value.bits[0]], vcdnames[info.description].c_str());
+ } else {
+ fprintf(f, "b");
+ for(int k=info.width-1; k >= 0; k --) //need to flip bit ordering for VCD
+ fprintf(f, "%c", bitvals[value.bits[k]]);
+ fprintf(f, " %s\n", vcdnames[info.description].c_str());
+ }
}
if (last_timestep == -2)
log(" no model variables selected for display.\n");
+
+ fclose(f);
+ }
+
+ 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));
+
+ log("Dumping SAT model to WaveJSON file '%s'.\n", json_file_name.c_str());
+
+ int mintime = 1, maxtime = 0, maxwidth = 0;;
+ dict<string, pair<int, dict<int, Const>>> wavedata;
+
+ for (auto &info : modelInfo)
+ {
+ Const value;
+ for (int i = 0; i < info.width; i++) {
+ value.bits.push_back(modelValues.at(info.offset+i) ? RTLIL::State::S1 : RTLIL::State::S0);
+ if (enable_undef && modelValues.at(modelExpressions.size()/2 + info.offset + i))
+ value.bits.back() = RTLIL::State::Sx;
+ }
+
+ wavedata[info.description].first = info.width;
+ wavedata[info.description].second[info.timestep] = value;
+ mintime = min(mintime, info.timestep);
+ maxtime = max(maxtime, info.timestep);
+ maxwidth = max(maxwidth, info.width);
+ }
+
+ fprintf(f, "{ \"signal\": [");
+ bool fist_wavedata = true;
+ for (auto &wd : wavedata)
+ {
+ fprintf(f, "%s", fist_wavedata ? "\n" : ",\n");
+ fist_wavedata = false;
+
+ vector<string> data;
+ string name = wd.first.c_str();
+ while (name.substr(0, 1) == "\\")
+ name = name.substr(1);
+
+ fprintf(f, " { \"name\": \"%s\", \"wave\": \"", name.c_str());
+ for (int i = mintime; i <= maxtime; i++) {
+ if (wd.second.second.count(i)) {
+ string this_data = wd.second.second[i].as_string();
+ char ch = '=';
+ if (wd.second.first == 1)
+ ch = this_data[0];
+ if (!data.empty() && data.back() == this_data) {
+ fprintf(f, ".");
+ } else {
+ data.push_back(this_data);
+ fprintf(f, "%c", ch);
+ }
+ } else {
+ data.push_back("");
+ fprintf(f, "4");
+ }
+ }
+ if (wd.second.first != 1) {
+ fprintf(f, "\", \"data\": [");
+ for (int i = 0; i < GetSize(data); i++)
+ fprintf(f, "%s\"%s\"", i ? ", " : "", data[i].c_str());
+ fprintf(f, "] }");
+ } else {
+ fprintf(f, "\" }");
+ }
+ }
+ fprintf(f, "\n ],\n");
+ fprintf(f, " \"config\": {\n");
+ fprintf(f, " \"hscale\": %.2f\n", maxwidth / 4.0);
+ fprintf(f, " }\n");
+ fprintf(f, "}\n");
+ fclose(f);
}
void invalidate_model(bool max_undef)
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);
if (!max_undef || !val_undef)
- clause.push_back(val_undef ? ez.NOT(bit_undef) : val ? ez.NOT(bit) : bit);
+ 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));
+ clause.push_back(modelValues.at(i) ? ez->NOT(modelExpressions.at(i)) : modelExpressions.at(i));
+ ez->assume(ez->expression(ezSAT::OpOr, clause));
}
};
-} /* namespace */
-
-static void print_proof_failed()
+void print_proof_failed()
{
log("\n");
log(" ______ ___ ___ _ _ _ _ \n");
log("\n");
}
-static void print_timeout()
+void print_timeout()
{
log("\n");
log(" _____ _ _ _____ ____ _ _____\n");
log("\n");
}
-static void print_qed()
+void print_qed()
{
log("\n");
log(" /$$$$$$ /$$$$$$$$ /$$$$$$$ \n");
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 the model for the specified signal. if no -show option is\n");
log(" passed then a set of signals to be shown is automatically selected.\n");
log("\n");
- log(" -show-inputs, -show-outputs\n");
- log(" add all module input (output) ports to the list of shown signals\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(" set up a sequential problem with <N> time steps. The steps will\n");
log(" be numbered from 1 to N.\n");
log("\n");
+ log(" note: for large <N> it can be significantly faster to use\n");
+ log(" -tempinduct-baseonly -maxsteps <N> instead of -seq <N>.\n");
+ log("\n");
log(" -set-at <N> <signal> <value>\n");
log(" -unset-at <N> <signal>\n");
log(" set or unset the specified signal to the specified value in the\n");
log(" given timestep. this has priority over a -set for the same signal.\n");
log("\n");
+ log(" -set-assumes\n");
+ log(" set all assumptions provided via $assume cells\n");
+ log("\n");
log(" -set-def-at <N> <signal>\n");
log(" -set-any-undef-at <N> <signal>\n");
log(" -set-all-undef-at <N> <signal>\n");
- log(" add undef contraints in the given timestep.\n");
+ log(" add undef constraints in the given timestep.\n");
log("\n");
log(" -set-init <signal> <value>\n");
log(" set the initial value for the register driving the signal to the value\n");
log(" -set-init-undef\n");
log(" set all initial states (not set using -set-init) to undef\n");
log("\n");
+ log(" -set-init-def\n");
+ log(" do not force a value for the initial state but do not allow undef\n");
+ log("\n");
+ log(" -set-init-zero\n");
+ log(" set all initial states (not set using -set-init) to zero\n");
+ log("\n");
+ log(" -dump_vcd <vcd-file-name>\n");
+ log(" dump SAT model (counter example in proof) to VCD file\n");
+ log("\n");
+ log(" -dump_json <json-file-name>\n");
+ log(" dump SAT model (counter example in proof) to a WaveJSON file.\n");
+ log("\n");
+ log(" -dump_cnf <cnf-file-name>\n");
+ log(" dump CNF of SAT problem (in DIMACS format). in temporal induction\n");
+ log(" proofs this is the CNF of the first induction step.\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");
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(" -tempinduct-def\n");
+ log(" Perform a temporal induction proof. Assume an initial state with all\n");
+ log(" registers set to defined values for the induction step.\n");
+ log("\n");
+ log(" -tempinduct-baseonly\n");
+ log(" Run only the basecase half of temporal induction (requires -maxsteps)\n");
+ log("\n");
+ log(" -tempinduct-inductonly\n");
+ log(" Run only the induction half of temporal induction\n");
+ log("\n");
+ log(" -tempinduct-skip <N>\n");
+ log(" Skip the first <N> steps of the induction proof.\n");
+ log("\n");
+ log(" note: this will assume that the base case holds for <N> steps.\n");
+ log(" this must be proven independently with \"-tempinduct-baseonly\n");
+ log(" -maxsteps <N>\". Use -initsteps if you just want to set a\n");
+ log(" minimal induction length.\n");
+ log("\n");
log(" -prove <signal> <value>\n");
log(" Attempt to proof that <signal> is always <value>.\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("\n");
+ log(" -prove-skip <N>\n");
+ log(" Do not enforce the prove-condition for the first <N> time steps.\n");
+ log("\n");
log(" -maxsteps <N>\n");
log(" Set a maximum length for the induction.\n");
log("\n");
+ log(" -initsteps <N>\n");
+ log(" Set initial length for the induction.\n");
+ log(" This will speed up the search of the right induction length\n");
+ log(" for deep induction proofs.\n");
+ log("\n");
+ log(" -stepsize <N>\n");
+ log(" Increase the size of the induction proof in steps of <N>.\n");
+ log(" This will speed up the search of the right induction length\n");
+ log(" for deep induction proofs.\n");
+ log("\n");
log(" -timeout <N>\n");
log(" Maximum number of seconds a single SAT instance may take.\n");
log("\n");
log(" -verify-no-timeout\n");
log(" Like -verify but do not return an error for timeouts.\n");
log("\n");
+ log(" -falsify\n");
+ log(" Return an error and stop the synthesis script if the proof succeeds.\n");
+ log("\n");
+ log(" -falsify-no-timeout\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;
std::map<int, std::vector<std::string>> unsets_at, sets_def_at, sets_any_undef_at, sets_all_undef_at;
std::vector<std::string> shows, sets_def, sets_any_undef, sets_all_undef;
- int loopcount = 0, seq_len = 0, maxsteps = 0, timeout = 0;
+ int loopcount = 0, seq_len = 0, maxsteps = 0, initsteps = 0, timeout = 0, prove_skip = 0;
bool verify = false, fail_on_timeout = false, enable_undef = false, set_def_inputs = false;
- bool ignore_div_by_zero = false, set_init_undef = false, max_undef = 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 ignore_unknown_cells = 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++) {
verify = true;
continue;
}
+ if (args[argidx] == "-falsify") {
+ fail_on_timeout = true;
+ falsify = true;
+ continue;
+ }
+ if (args[argidx] == "-falsify-no-timeout") {
+ falsify = true;
+ continue;
+ }
if (args[argidx] == "-timeout" && argidx+1 < args.size()) {
timeout = atoi(args[++argidx].c_str());
continue;
maxsteps = atoi(args[++argidx].c_str());
continue;
}
+ if (args[argidx] == "-initsteps" && argidx+1 < args.size()) {
+ initsteps = atoi(args[++argidx].c_str());
+ continue;
+ }
+ if (args[argidx] == "-stepsize" && argidx+1 < args.size()) {
+ stepsize = max(1, atoi(args[++argidx].c_str()));
+ continue;
+ }
if (args[argidx] == "-ignore_div_by_zero") {
ignore_div_by_zero = true;
continue;
enable_undef = true;
continue;
}
+ if (args[argidx] == "-set-assumes") {
+ set_assumes = true;
+ continue;
+ }
if (args[argidx] == "-tempinduct") {
tempinduct = true;
continue;
}
+ if (args[argidx] == "-tempinduct-def") {
+ tempinduct = true;
+ tempinduct_def = true;
+ enable_undef = true;
+ continue;
+ }
+ if (args[argidx] == "-tempinduct-baseonly") {
+ tempinduct = true;
+ tempinduct_baseonly = true;
+ continue;
+ }
+ if (args[argidx] == "-tempinduct-inductonly") {
+ tempinduct = true;
+ tempinduct_inductonly = true;
+ continue;
+ }
+ if (args[argidx] == "-tempinduct-skip" && argidx+1 < args.size()) {
+ tempinduct_skip = atoi(args[++argidx].c_str());
+ continue;
+ }
if (args[argidx] == "-prove" && argidx+2 < args.size()) {
std::string lhs = args[++argidx];
std::string rhs = args[++argidx];
prove_asserts = true;
continue;
}
+ if (args[argidx] == "-prove-skip" && argidx+1 < args.size()) {
+ prove_skip = atoi(args[++argidx].c_str());
+ continue;
+ }
if (args[argidx] == "-seq" && argidx+1 < args.size()) {
seq_len = atoi(args[++argidx].c_str());
continue;
enable_undef = true;
continue;
}
+ if (args[argidx] == "-set-init-def") {
+ set_init_def = true;
+ continue;
+ }
+ if (args[argidx] == "-set-init-zero") {
+ set_init_zero = true;
+ continue;
+ }
if (args[argidx] == "-show" && argidx+1 < args.size()) {
shows.push_back(args[++argidx]);
continue;
show_outputs = true;
continue;
}
+ if (args[argidx] == "-show-ports") {
+ show_inputs = true;
+ 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;
}
+ if (args[argidx] == "-dump_vcd" && argidx+1 < args.size()) {
+ vcd_file_name = args[++argidx];
+ continue;
+ }
+ if (args[argidx] == "-dump_json" && argidx+1 < args.size()) {
+ json_file_name = args[++argidx];
+ continue;
+ }
+ if (args[argidx] == "-dump_cnf" && argidx+1 < args.size()) {
+ cnf_file_name = args[++argidx];
+ continue;
+ }
break;
}
extra_args(args, argidx, design);
RTLIL::Module *module = NULL;
- for (auto &mod_it : design->modules)
- if (design->selected(mod_it.second)) {
- if (module)
- log_cmd_error("Only one module must be selected for the SAT pass! (selected: %s and %s)\n",
- RTLIL::id2cstr(module->name), RTLIL::id2cstr(mod_it.first));
- module = mod_it.second;
- }
- if (module == NULL)
+ for (auto mod : design->selected_modules()) {
+ if (module)
+ log_cmd_error("Only one module must be selected for the SAT pass! (selected: %s and %s)\n", log_id(module), log_id(mod));
+ module = mod;
+ }
+ if (module == NULL)
log_cmd_error("Can't perform SAT on an empty selection!\n");
- if (!prove.size() && !prove_x.size() && !prove_asserts && verify)
- log_cmd_error("Got -verify but nothing to prove!\n");
-
if (!prove.size() && !prove_x.size() && !prove_asserts && tempinduct)
log_cmd_error("Got -tempinduct but nothing to prove!\n");
- if (seq_len == 0 && tempinduct)
- log_cmd_error("Got -tempinduct but no -seq argument!\n");
+ if (prove_skip && tempinduct)
+ log_cmd_error("Options -prove-skip and -tempinduct don't work with each other. Use -seq instead of -prove-skip.\n");
+
+ if (prove_skip >= seq_len && prove_skip > 0)
+ log_cmd_error("The value of -prove-skip must be smaller than the one of -seq.\n");
+
+ if (set_init_undef + set_init_zero + set_init_def > 1)
+ log_cmd_error("The options -set-init-undef, -set-init-def, and -set-init-zero are exclusive!\n");
if (set_def_inputs) {
- for (auto &it : module->wires)
+ for (auto &it : module->wires_)
if (it.second->port_input)
- sets_def.push_back(it.second->name);
+ sets_def.push_back(it.second->name.str());
}
if (show_inputs) {
- for (auto &it : module->wires)
+ for (auto &it : module->wires_)
if (it.second->port_input)
- shows.push_back(it.second->name);
+ shows.push_back(it.second->name.str());
}
if (show_outputs) {
- for (auto &it : module->wires)
+ for (auto &it : module->wires_)
if (it.second->port_output)
- shows.push_back(it.second->name);
+ 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)
SatHelper inductstep(design, module, enable_undef);
basecase.sets = sets;
+ basecase.set_assumes = set_assumes;
basecase.prove = prove;
basecase.prove_x = prove_x;
basecase.prove_asserts = prove_asserts;
basecase.sets_any_undef_at = sets_any_undef_at;
basecase.sets_all_undef_at = sets_all_undef_at;
basecase.sets_init = sets_init;
+ basecase.set_init_def = set_init_def;
basecase.set_init_undef = set_init_undef;
+ basecase.set_init_zero = set_init_zero;
basecase.satgen.ignore_div_by_zero = ignore_div_by_zero;
basecase.ignore_unknown_cells = ignore_unknown_cells;
for (int timestep = 1; timestep <= seq_len; timestep++)
- basecase.setup(timestep);
- basecase.setup_init();
+ if (!tempinduct_inductonly)
+ basecase.setup(timestep, timestep == 1);
inductstep.sets = sets;
+ inductstep.set_assumes = set_assumes;
inductstep.prove = prove;
inductstep.prove_x = prove_x;
inductstep.prove_asserts = prove_asserts;
inductstep.satgen.ignore_div_by_zero = ignore_div_by_zero;
inductstep.ignore_unknown_cells = ignore_unknown_cells;
- inductstep.setup(1);
- inductstep.ez.assume(inductstep.setup_proof(1));
+ if (!tempinduct_baseonly) {
+ inductstep.setup(1);
+ inductstep.ez->assume(inductstep.setup_proof(1));
+ }
+
+ if (tempinduct_def) {
+ std::vector<int> undef_state = inductstep.satgen.importUndefSigSpec(inductstep.satgen.initial_state.export_all(), 1);
+ inductstep.ez->assume(inductstep.ez->NOT(inductstep.ez->expression(ezSAT::OpOr, undef_state)));
+ }
for (int inductlen = 1; inductlen <= maxsteps || maxsteps == 0; inductlen++)
{
// phase 1: proving base case
- basecase.setup(seq_len + inductlen);
- int property = basecase.setup_proof(seq_len + inductlen);
- basecase.generate_model();
-
- if (inductlen > 1)
- basecase.force_unique_state(seq_len + 1, seq_len + inductlen);
-
- log("\n[base case] Solving problem with %d variables and %d clauses..\n",
- basecase.ez.numCnfVariables(), basecase.ez.numCnfClauses());
-
- if (basecase.solve(basecase.ez.NOT(property))) {
- log("SAT temporal induction proof finished - model found for base case: FAIL!\n");
- print_proof_failed();
- basecase.print_model();
- goto tip_failed;
+ if (!tempinduct_inductonly)
+ {
+ basecase.setup(seq_len + inductlen, seq_len + inductlen == 1);
+ int property = basecase.setup_proof(seq_len + inductlen);
+ basecase.generate_model();
+
+ if (inductlen > 1)
+ basecase.force_unique_state(seq_len + 1, seq_len + inductlen);
+
+ if (tempinduct_skip < 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");
+ print_proof_failed();
+ basecase.print_model();
+ if(!vcd_file_name.empty())
+ basecase.dump_model_to_vcd(vcd_file_name);
+ if(!json_file_name.empty())
+ basecase.dump_model_to_json(json_file_name);
+ goto tip_failed;
+ }
+
+ if (basecase.gotTimeout)
+ goto timeout;
+
+ log("Base case for induction length %d proven.\n", inductlen);
+ }
+ else
+ {
+ log("\n[base case %d] Skipping prove for this step (-tempinduct-skip %d).",
+ inductlen, tempinduct_skip);
+ log("\n[base case %d] Problem size so far: %d variables and %d clauses.\n",
+ inductlen, basecase.ez->numCnfVariables(), basecase.ez->numCnfClauses());
+ }
+ basecase.ez->assume(property);
}
- if (basecase.gotTimeout)
- goto timeout;
-
- log("Base case for induction length %d proven.\n", inductlen);
- basecase.ez.assume(property);
-
// phase 2: proving induction step
- inductstep.setup(inductlen + 1);
- property = inductstep.setup_proof(inductlen + 1);
- inductstep.generate_model();
-
- if (inductlen > 1)
- inductstep.force_unique_state(1, inductlen + 1);
-
- log("\n[induction step] Solving problem with %d variables and %d clauses..\n",
- inductstep.ez.numCnfVariables(), inductstep.ez.numCnfClauses());
-
- if (!inductstep.solve(inductstep.ez.NOT(property))) {
- if (inductstep.gotTimeout)
- goto timeout;
- log("Induction step proven: SUCCESS!\n");
- print_qed();
- goto tip_success;
+ if (!tempinduct_baseonly)
+ {
+ inductstep.setup(inductlen + 1);
+ int property = inductstep.setup_proof(inductlen + 1);
+ inductstep.generate_model();
+
+ if (inductlen > 1)
+ inductstep.force_unique_state(1, inductlen + 1);
+
+ if (inductlen <= tempinduct_skip || inductlen <= initsteps || inductlen % stepsize != 0)
+ {
+ if (inductlen < tempinduct_skip)
+ log("\n[induction step %d] Skipping prove for this step (-tempinduct-skip %d).",
+ inductlen, tempinduct_skip);
+ if (inductlen < initsteps)
+ log("\n[induction step %d] Skipping prove for this step (-initsteps %d).",
+ inductlen, tempinduct_skip);
+ if (inductlen % stepsize != 0)
+ log("\n[induction step %d] Skipping prove for this step (-stepsize %d).",
+ inductlen, stepsize);
+ log("\n[induction step %d] Problem size so far: %d variables and %d clauses.\n",
+ inductlen, inductstep.ez->numCnfVariables(), inductstep.ez->numCnfClauses());
+ inductstep.ez->assume(property);
+ }
+ else
+ {
+ 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("Dumping CNF to file `%s'.\n", cnf_file_name.c_str());
+ cnf_file_name.clear();
+
+ inductstep.ez->printDIMACS(f, false);
+ fclose(f);
+ }
+
+ 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)
+ goto timeout;
+ log("Induction step proven: SUCCESS!\n");
+ print_qed();
+ goto tip_success;
+ }
+
+ log("Induction step failed. Incrementing induction length.\n");
+ inductstep.ez->assume(property);
+ inductstep.print_model();
+ }
}
+ }
- log("Induction step failed. Incrementing induction length.\n");
- inductstep.ez.assume(property);
-
- inductstep.print_model();
+ if (tempinduct_baseonly) {
+ log("\nReached maximum number of time steps -> proved base case for %d steps: SUCCESS!\n", maxsteps);
+ goto tip_success;
}
log("\nReached maximum number of time steps -> proof failed.\n");
+ if(!vcd_file_name.empty())
+ inductstep.dump_model_to_vcd(vcd_file_name);
+ if(!json_file_name.empty())
+ inductstep.dump_model_to_json(json_file_name);
print_proof_failed();
tip_failed:
log_error("Called with -verify and proof did fail!\n");
}
- tip_success:;
+ if (0)
+ tip_success:
+ if (falsify) {
+ log("\n");
+ log_error("Called with -falsify and proof did succeed!\n");
+ }
}
else
{
SatHelper sathelper(design, module, enable_undef);
sathelper.sets = sets;
+ sathelper.set_assumes = set_assumes;
sathelper.prove = prove;
sathelper.prove_x = prove_x;
sathelper.prove_asserts = prove_asserts;
sathelper.sets_any_undef_at = sets_any_undef_at;
sathelper.sets_all_undef_at = sets_all_undef_at;
sathelper.sets_init = sets_init;
+ sathelper.set_init_def = set_init_def;
sathelper.set_init_undef = set_init_undef;
+ sathelper.set_init_zero = set_init_zero;
sathelper.satgen.ignore_div_by_zero = ignore_div_by_zero;
sathelper.ignore_unknown_cells = ignore_unknown_cells;
if (seq_len == 0) {
sathelper.setup();
if (sathelper.prove.size() || sathelper.prove_x.size() || sathelper.prove_asserts)
- sathelper.ez.assume(sathelper.ez.NOT(sathelper.setup_proof()));
+ sathelper.ez->assume(sathelper.ez->NOT(sathelper.setup_proof()));
} 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)
- prove_bits.push_back(sathelper.setup_proof(timestep));
+ 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.ez->assume(sathelper.ez->NOT(sathelper.ez->expression(ezSAT::OpAnd, prove_bits)));
}
sathelper.generate_model();
-#if 0
- // print CNF for debugging
- sathelper.ez.printDIMACS(stdout, true);
-#endif
+ 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("Dumping CNF to file `%s'.\n", cnf_file_name.c_str());
+ cnf_file_name.clear();
+
+ sathelper.ez->printDIMACS(f, false);
+ fclose(f);
+ }
int rerun_counter = 0;
rerun_solver:
log("\nSolving problem with %d variables and %d clauses..\n",
- sathelper.ez.numCnfVariables(), sathelper.ez.numCnfClauses());
+ sathelper.ez->numCnfVariables(), sathelper.ez->numCnfClauses());
+ log_flush();
if (sathelper.solve())
{
sathelper.print_model();
+ if(!vcd_file_name.empty())
+ sathelper.dump_model_to_vcd(vcd_file_name);
+ if(!json_file_name.empty())
+ sathelper.dump_model_to_json(json_file_name);
+
if (loopcount != 0) {
loopcount--, rerun_counter++;
sathelper.invalidate_model(max_undef);
goto rerun_solver;
}
- if (verify) {
- log("\n");
- log_error("Called with -verify and proof did fail!\n");
+ if (!prove.size() && !prove_x.size() && !prove_asserts) {
+ if (falsify) {
+ log("\n");
+ log_error("Called with -falsify and found a model!\n");
+ }
+ } else {
+ if (verify) {
+ log("\n");
+ log_error("Called with -verify and proof did fail!\n");
+ }
}
}
else
goto timeout;
if (rerun_counter)
log("SAT solving finished - no more models found (after %d distinct solutions).\n", rerun_counter);
- else if (!prove.size() && !prove_x.size() && !prove_asserts)
+ else if (!prove.size() && !prove_x.size() && !prove_asserts) {
log("SAT solving finished - no model found.\n");
- else {
+ if (verify) {
+ log("\n");
+ log_error("Called with -verify and found no model!\n");
+ }
+ } else {
log("SAT proof finished - no model found: SUCCESS!\n");
print_qed();
+ if (falsify) {
+ log("\n");
+ log_error("Called with -falsify and proof did succeed!\n");
+ }
}
}
- if (verify && rerun_counter) {
- log("\n");
- log_error("Called with -verify and proof did fail!\n");
+ if (!prove.size() && !prove_x.size() && !prove_asserts) {
+ if (falsify && rerun_counter) {
+ log("\n");
+ log_error("Called with -falsify and found a model!\n");
+ }
+ } else {
+ if (verify && rerun_counter) {
+ log("\n");
+ log_error("Called with -verify and proof did fail!\n");
+ }
}
}
}
}
} SatPass;
-
+
+PRIVATE_NAMESPACE_END
projects / yosys.git / blobdiff