mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-13 04:28:18 +00:00
Code Activity

Improvements and fixes in SAT code

Browse source
This commit is contained in:
Clifford Wolf 2013-06-10 16:09:29 +02:00
parent 15ff4cc63b
commit 7d790febb0
2 changed files with 36 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

27
kernel/satgen.h
View file

@ -74,22 +74,22 @@ struct SatGen
return vec; return vec;
} }
void extendSignalWidth(std::vector<int> &vec_a, std::vector<int> &vec_b, RTLIL::Cell *cell) void extendSignalWidth(std::vector<int> &vec_a, std::vector<int> &vec_b, RTLIL::Cell *cell, size_t y_width = 0)
{ {
bool is_signed_a = false, is_signed_b = false; bool is_signed_a = false, is_signed_b = false;
if (cell->parameters.count("\\A_SIGNED") > 0) if (cell->parameters.count("\\A_SIGNED") > 0)
is_signed_a = cell->parameters["\\A_SIGNED"].as_bool(); is_signed_a = cell->parameters["\\A_SIGNED"].as_bool();
if (cell->parameters.count("\\B_SIGNED") > 0) if (cell->parameters.count("\\B_SIGNED") > 0)
is_signed_b = cell->parameters["\\B_SIGNED"].as_bool(); is_signed_b = cell->parameters["\\B_SIGNED"].as_bool();
while (vec_a.size() < vec_b.size()) while (vec_a.size() < vec_b.size() || vec_a.size() < y_width)
vec_a.push_back(is_signed_a && vec_a.size() > 0 ? vec_a.back() : ez->FALSE); vec_a.push_back(is_signed_a && vec_a.size() > 0 ? vec_a.back() : ez->FALSE);
while (vec_b.size() < vec_a.size()) while (vec_b.size() < vec_a.size() || vec_b.size() < y_width)
vec_b.push_back(is_signed_b && vec_b.size() > 0 ? vec_b.back() : ez->FALSE); vec_b.push_back(is_signed_b && vec_b.size() > 0 ? vec_b.back() : ez->FALSE);
} }
void extendSignalWidth(std::vector<int> &vec_a, std::vector<int> &vec_b, std::vector<int> &vec_y, RTLIL::Cell *cell) void extendSignalWidth(std::vector<int> &vec_a, std::vector<int> &vec_b, std::vector<int> &vec_y, RTLIL::Cell *cell)
{ {
extendSignalWidth(vec_a, vec_b, cell); extendSignalWidth(vec_a, vec_b, cell, vec_y.size());
while (vec_y.size() < vec_a.size()) while (vec_y.size() < vec_a.size())
vec_y.push_back(ez->literal()); vec_y.push_back(ez->literal());
} }
@ -239,6 +239,23 @@ struct SatGen
return true; return true;
} }
if (cell->type == "$mul") {
std::vector<int> a = importSigSpec(cell->connections.at("\\A"), timestep);
std::vector<int> b = importSigSpec(cell->connections.at("\\B"), timestep);
std::vector<int> y = importSigSpec(cell->connections.at("\\Y"), timestep);
extendSignalWidth(a, b, y, cell);
std::vector<int> tmp(a.size(), ez->FALSE);
for (int i = 0; i < int(a.size()); i++)
{
std::vector<int> shifted_a(a.size(), ez->FALSE);
for (int j = i; j < int(a.size()); j++)
shifted_a.at(j) = a.at(j-i);
tmp = ez->vec_ite(b.at(i), ez->vec_add(tmp, shifted_a), tmp);
}
ez->assume(ez->vec_eq(tmp, y));
return true;
}
if (timestep > 0 && (cell->type == "$dff" || cell->type == "$_DFF_N_" || cell->type == "$_DFF_P_")) { 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"))); initial_state.add((*sigmap)(cell->connections.at("\\Q")));
@ -250,7 +267,7 @@ struct SatGen
return true; return true;
} }
// Unsupported internal cell types: $mul $div $mod $pow // Unsupported internal cell types: $div $mod $pow
// .. and all sequential cells except $dff and $_DFF_[NP]_ // .. and all sequential cells except $dff and $_DFF_[NP]_
return false; return false;
} }

18
passes/sat/sat.cc
View file

@ -41,6 +41,11 @@ static void split(std::vector<std::string> &tokens, const std::string &text, cha
tokens.push_back(text.substr(start)); tokens.push_back(text.substr(start));
} }
static int get_dummy_line_num()
{
return 0;
}
static bool parse_sigstr(RTLIL::SigSpec &sig, RTLIL::Module *module, std::string str) static bool parse_sigstr(RTLIL::SigSpec &sig, RTLIL::Module *module, std::string str)
{ {
std::vector<std::string> tokens; std::vector<std::string> tokens;
@ -56,6 +61,7 @@ static bool parse_sigstr(RTLIL::SigSpec &sig, RTLIL::Module *module, std::string
continue; continue;
if ('0' <= netname[0] && netname[0] <= '9') { if ('0' <= netname[0] && netname[0] <= '9') {
AST::get_line_num = get_dummy_line_num;
AST::AstNode *ast = VERILOG_FRONTEND::const2ast(netname); AST::AstNode *ast = VERILOG_FRONTEND::const2ast(netname);
if (ast == NULL) if (ast == NULL)
return false; return false;
@ -320,7 +326,7 @@ struct SatHelper
continue; continue;
if (d->type.substr(0, 6) == "$_DFF_" && p.first == "\\C") if (d->type.substr(0, 6) == "$_DFF_" && p.first == "\\C")
continue; continue;
queued_signals.add(handled_signals.remove(p.second)); queued_signals.add(handled_signals.remove(sigmap(p.second)));
} }
} }
} }
@ -712,6 +718,8 @@ struct SatPass : public Pass {
sathelper.ez.printDIMACS(stdout, true); sathelper.ez.printDIMACS(stdout, true);
#endif #endif
bool did_rerun = false;
rerun_solver: rerun_solver:
log("\nSolving problem with %d variables and %d clauses..\n", log("\nSolving problem with %d variables and %d clauses..\n",
sathelper.ez.numCnfVariables(), sathelper.ez.numCnfClauses()); sathelper.ez.numCnfVariables(), sathelper.ez.numCnfClauses());
@ -733,16 +741,18 @@ struct SatPass : public Pass {
} }
if (loopcount != 0) { if (loopcount != 0) {
loopcount--; loopcount--, did_rerun = true;
sathelper.invalidate_model(); sathelper.invalidate_model();
goto rerun_solver; goto rerun_solver;
} }
} }
else else
{ {
if (prove.size() == 0) { if (did_rerun)
log("SAT solving finished - no more models found.\n");
else if (prove.size() == 0)
log("SAT solving finished - no model found.\n"); log("SAT solving finished - no model found.\n");
} else { else {
log("SAT proof finished - no model found: SUCCESS!\n"); log("SAT proof finished - no model found: SUCCESS!\n");
print_qed(); print_qed();
} }