From 46fbe9d26299a7b6197463b3056d778f525658fb Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Fri, 7 Jun 2013 13:59:13 +0200 Subject: [PATCH] Added SAT generator and simple sat_solve command --- frontends/verilog/const2ast.cc | 5 +- frontends/verilog/parser.y | 2 + kernel/satgen.h | 137 +++++++++++++++++++ passes/sat/Makefile.inc | 3 + passes/sat/example.v | 12 ++ passes/sat/example.ys | 3 + passes/sat/sat_solve.cc | 241 +++++++++++++++++++++++++++++++++ 7 files changed, 400 insertions(+), 3 deletions(-) create mode 100644 kernel/satgen.h create mode 100644 passes/sat/Makefile.inc create mode 100644 passes/sat/example.v create mode 100644 passes/sat/example.ys create mode 100644 passes/sat/sat_solve.cc diff --git a/frontends/verilog/const2ast.cc b/frontends/verilog/const2ast.cc index e5beaeade..3a88fc046 100644 --- a/frontends/verilog/const2ast.cc +++ b/frontends/verilog/const2ast.cc @@ -186,12 +186,11 @@ AstNode *VERILOG_FRONTEND::const2ast(std::string code, char case_type) my_strtobin(data, endptr+2, len_in_bits, 16, case_type); break; default: - goto error; + return NULL; } return AstNode::mkconst_bits(data, is_signed); } -error: - log_error("Value conversion failed: `%s'\n", code.c_str()); + return NULL; } diff --git a/frontends/verilog/parser.y b/frontends/verilog/parser.y index 22af178e8..ea39e83d4 100644 --- a/frontends/verilog/parser.y +++ b/frontends/verilog/parser.y @@ -912,6 +912,8 @@ basic_expr: } | TOK_CONST { $$ = const2ast(*$1, case_type_stack.size() == 0 ? 0 : case_type_stack.back()); + if ($$ == NULL) + log_error("Value conversion failed: `%s'\n", $1->c_str()); delete $1; } | TOK_STRING { diff --git a/kernel/satgen.h b/kernel/satgen.h new file mode 100644 index 000000000..500c3f105 --- /dev/null +++ b/kernel/satgen.h @@ -0,0 +1,137 @@ +/* + * yosys -- Yosys Open SYnthesis Suite + * + * Copyright (C) 2012 Clifford Wolf + * + * 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. + * + */ + +#ifndef SATGEN_H +#define SATGEN_H + +#include "kernel/rtlil.h" +#include "kernel/sigtools.h" +#include "kernel/celltypes.h" + +#ifdef YOSYS_ENABLE_MINISAT +# include "libs/ezsat/ezminisat.h" +typedef ezMiniSAT ezDefaultSAT; +#else +# include "libs/ezsat/ezsat.h" +typedef ezSAT ezDefaultSAT; +#endif + +struct SatGen +{ + ezSAT *ez; + RTLIL::Design *design; + SigMap *sigmap; + std::string prefix; + + SatGen(ezSAT *ez, RTLIL::Design *design, SigMap *sigmap, std::string prefix = std::string()) : + ez(ez), design(design), sigmap(sigmap), prefix(prefix) + { + } + + void setContext(RTLIL::Design *design, SigMap *sigmap, std::string prefix = std::string()) + { + this->design = design; + this->sigmap = sigmap; + this->prefix = prefix; + } + + virtual ~SatGen() + { + } + + virtual std::vector importSigSpec(RTLIL::SigSpec &sig) + { + RTLIL::SigSpec s = sig; + sigmap->apply(s); + s.expand(); + + std::vector vec; + vec.reserve(s.chunks.size()); + + for (auto &c : s.chunks) + if (c.wire == NULL) + vec.push_back(c.data.as_bool() ? ez->TRUE : ez->FALSE); + else + vec.push_back(ez->literal(prefix + stringf(c.wire->width == 1 ? + "%s" : "%s [%d]", RTLIL::id2cstr(c.wire->name), c.offset))); + return vec; + } + + // ** cell types to be done: ** + // cell_types.insert("$pos"); + // cell_types.insert("$neg"); + // cell_types.insert("$xnor"); + // cell_types.insert("$reduce_and"); + // cell_types.insert("$reduce_or"); + // cell_types.insert("$reduce_xor"); + // cell_types.insert("$reduce_xnor"); + // cell_types.insert("$reduce_bool"); + // cell_types.insert("$shl"); + // cell_types.insert("$shr"); + // cell_types.insert("$sshl"); + // cell_types.insert("$sshr"); + // cell_types.insert("$lt"); + // cell_types.insert("$le"); + // cell_types.insert("$eq"); + // cell_types.insert("$ne"); + // cell_types.insert("$ge"); + // cell_types.insert("$gt"); + // cell_types.insert("$add"); + // cell_types.insert("$sub"); + // cell_types.insert("$mul"); + // cell_types.insert("$div"); + // cell_types.insert("$mod"); + // cell_types.insert("$pow"); + // cell_types.insert("$logic_not"); + // cell_types.insert("$logic_and"); + // cell_types.insert("$logic_or"); + // cell_types.insert("$pmux"); + // cell_types.insert("$safe_pmux"); + + virtual void importCell(RTLIL::Cell *cell) + { + if (cell->type == "$_AND_" || cell->type == "$_OR_" || cell->type == "$_XOR_" || + cell->type == "$and" || cell->type == "$or" || cell->type == "$xor") { + std::vector a = importSigSpec(cell->connections.at("\\A")); + std::vector b = importSigSpec(cell->connections.at("\\B")); + std::vector y = importSigSpec(cell->connections.at("\\Y")); + if (cell->type == "$and" || cell->type == "$_AND_") + ez->assume(ez->vec_eq(ez->vec_and(a, b), y)); + if (cell->type == "$or" || cell->type == "$_OR_") + ez->assume(ez->vec_eq(ez->vec_or(a, b), y)); + if (cell->type == "$xor" || cell->type == "$_XOR") + ez->assume(ez->vec_eq(ez->vec_xor(a, b), y)); + } else + if (cell->type == "$_INV_" || cell->type == "$not") { + std::vector a = importSigSpec(cell->connections.at("\\A")); + std::vector y = importSigSpec(cell->connections.at("\\Y")); + ez->assume(ez->vec_eq(ez->vec_not(a), y)); + } else + if (cell->type == "$_MUX_" || cell->type == "$mux") { + std::vector a = importSigSpec(cell->connections.at("\\A")); + std::vector b = importSigSpec(cell->connections.at("\\B")); + std::vector s = importSigSpec(cell->connections.at("\\S")); + std::vector y = importSigSpec(cell->connections.at("\\Y")); + ez->assume(ez->vec_eq(ez->vec_ite(s, b, a), y)); + } else + log_error("Can't handle cell type %s in SAT generator yet.\n", RTLIL::id2cstr(cell->type)); + } +}; + +#endif diff --git a/passes/sat/Makefile.inc b/passes/sat/Makefile.inc new file mode 100644 index 000000000..873f97468 --- /dev/null +++ b/passes/sat/Makefile.inc @@ -0,0 +1,3 @@ + +OBJS += passes/sat/sat_solve.o + diff --git a/passes/sat/example.v b/passes/sat/example.v new file mode 100644 index 000000000..45011f70d --- /dev/null +++ b/passes/sat/example.v @@ -0,0 +1,12 @@ + +module example(a, y); + +input [15:0] a; +output y; + +wire gt = a > 12345; +wire lt = a < 12345; +assign y = !gt && !lt; + +endmodule + diff --git a/passes/sat/example.ys b/passes/sat/example.ys new file mode 100644 index 000000000..b7798ab2e --- /dev/null +++ b/passes/sat/example.ys @@ -0,0 +1,3 @@ +read_verilog example.v +techmap; opt +sat_solve -show a -set y 1'b1 diff --git a/passes/sat/sat_solve.cc b/passes/sat/sat_solve.cc new file mode 100644 index 000000000..1644eaaa1 --- /dev/null +++ b/passes/sat/sat_solve.cc @@ -0,0 +1,241 @@ +/* + * yosys -- Yosys Open SYnthesis Suite + * + * Copyright (C) 2012 Clifford Wolf + * + * 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/register.h" +#include "kernel/celltypes.h" +#include "kernel/sigtools.h" +#include "kernel/log.h" +#include "kernel/satgen.h" +#include "frontends/verilog/verilog_frontend.h" +#include +#include +#include + +static void split(std::vector &tokens, const std::string &text, char sep) +{ + size_t start = 0, end = 0; + while ((end = text.find(sep, start)) != std::string::npos) { + tokens.push_back(text.substr(start, end - start)); + start = end + 1; + } + tokens.push_back(text.substr(start)); +} + +bool parse_sigstr(RTLIL::SigSpec &sig, RTLIL::Module *module, std::string str) +{ + std::vector tokens; + split(tokens, str, ','); + + sig = RTLIL::SigSpec(); + for (auto &tok : tokens) + { + std::string netname = tok; + std::string indices; + + if (netname.size() == 0) + continue; + + if ('0' <= netname[0] && netname[0] <= '9') { + AST::AstNode *ast = VERILOG_FRONTEND::const2ast(netname); + if (ast == NULL) + return false; + sig.append(RTLIL::Const(ast->bits)); + delete ast; + continue; + } + + if (netname[0] != '$' && netname[0] != '\\') + netname = "\\" + netname; + + if (module->wires.count(netname) == 0) { + size_t indices_pos = netname.size()-1; + if (indices_pos > 2 && netname[indices_pos] == ']') + { + indices_pos--; + while (indices_pos > 0 && ('0' <= netname[indices_pos] && netname[indices_pos] <= '9')) indices_pos--; + if (indices_pos > 0 && netname[indices_pos] == ':') { + indices_pos--; + while (indices_pos > 0 && ('0' <= netname[indices_pos] && netname[indices_pos] <= '9')) indices_pos--; + } + if (indices_pos > 0 && netname[indices_pos] == '[') { + indices = netname.substr(indices_pos); + netname = netname.substr(0, indices_pos); + } + } + } + + if (module->wires.count(netname) == 0) + return false; + + RTLIL::Wire *wire = module->wires.at(netname); + if (!indices.empty()) { + std::vector index_tokens; + split(index_tokens, indices.substr(1, indices.size()-2), ':'); + if (index_tokens.size() == 1) + sig.append(RTLIL::SigSpec(wire, 1, atoi(index_tokens.at(0).c_str()))); + else { + int a = atoi(index_tokens.at(0).c_str()); + int b = atoi(index_tokens.at(1).c_str()); + if (a > b) { + int tmp = a; + a = b, b = tmp; + } + sig.append(RTLIL::SigSpec(wire, b-a+1, a)); + } + } else + sig.append(wire); + } + + return true; +} + +struct SatSolvePass : public Pass { + SatSolvePass() : Pass("sat_solve", "solve a SAT problem in the circuit") { } + virtual void help() + { + // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| + log("\n"); + log(" sat_solve [options] [selection]\n"); + log("\n"); + log("This command solves a SAT problem defined over the currently selected circuit\n"); + log("and additional constraints passed as parameters.\n"); + log("\n"); + log(" -set \n"); + log(" set the specified signal to the specified value.\n"); + log("\n"); + log(" -show n"); + log(" show the model for the specified signal. if no -show option\n"); + log(" is passed then all selected signals will be shown.\n"); + log("\n"); + } + virtual void execute(std::vector args, RTLIL::Design *design) + { + std::vector> sets; + std::vector shows; + + log_header("Executing SAT_SOLVE pass (detecting logic loops).\n"); + + size_t argidx; + for (argidx = 1; argidx < args.size(); argidx++) { + if (args[argidx] == "-set" && argidx+2 < args.size()) { + std::string lhs = args[++argidx].c_str(); + std::string rhs = args[++argidx].c_str(); + sets.push_back(std::pair(lhs, rhs)); + continue; + } + if (args[argidx] == "-show" && argidx+1 < args.size()) { + shows.push_back(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_SOLVE pass! (selected: %s and %s)\n", + RTLIL::id2cstr(module->name), RTLIL::id2cstr(mod_it.first)); + module = mod_it.second; + } + if (module == NULL) + log_cmd_error("Can't perform SAT_SOLVE on an empty selection!\n"); + + ezDefaultSAT ez; + SigMap sigmap(module); + SatGen satgen(&ez, design, &sigmap); + + for (auto &s : sets) + { + RTLIL::SigSpec lhs, rhs; + + if (!parse_sigstr(lhs, module, s.first)) + log_cmd_error("Failed to parse lhs set expression `%s'.\n", s.first.c_str()); + if (!parse_sigstr(rhs, module, s.second)) + log_cmd_error("Failed to parse rhs set expression `%s'.\n", s.second.c_str()); + + 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 constraint: %s = %s\n", log_signal(lhs), log_signal(rhs)); + + std::vector lhs_vec = satgen.importSigSpec(lhs); + std::vector rhs_vec = satgen.importSigSpec(rhs); + ez.assume(ez.vec_eq(lhs_vec, rhs_vec)); + } + + 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)); + satgen.importCell(c.second); + import_cell_counter++; + } + log("Imported %d cells.\n", import_cell_counter); + + std::vector modelExpressions; + std::vector modelValues; + std::vector modelNames; + int maxModelName = 0; + + if (shows.size() == 0) { + for (auto &w : module->wires) + if (design->selected(module, w.second)) { + RTLIL::Wire *wire = w.second; + for (int i = 0; i < wire->width; i++) { + RTLIL::SigSpec sig = RTLIL::SigSpec(wire, 1, i); + std::vector vec = satgen.importSigSpec(sig); + log_assert(vec.size() == 1); + modelExpressions.push_back(vec[0]); + modelNames.push_back(log_signal(sig)); + maxModelName = std::max(maxModelName, int(modelNames.back().size())); + } + } + } else { + for (auto &s : shows) { + RTLIL::SigSpec sig; + if (!parse_sigstr(sig, module, s)) + log_cmd_error("Failed to parse show expression `%s'.\n", s.c_str()); + sig.expand(); + log("Import show expression: %s\n", log_signal(sig)); + for (auto &c : sig.chunks) { + RTLIL::SigSpec chunksig = c; + std::vector vec = satgen.importSigSpec(chunksig); + log_assert(vec.size() == 1); + modelExpressions.push_back(vec[0]); + modelNames.push_back(log_signal(chunksig)); + maxModelName = std::max(maxModelName, int(modelNames.back().size())); + } + } + } + + log("Solving problem with %d variables and %d clauses..\n", ez.numCnfVariables(), int(ez.cnf().size())); + if (ez.solve(modelExpressions, modelValues)) + { + log("SAT solving finished - model found:\n"); + for (size_t i = 0; i < modelNames.size(); i++) + log(" %-*s %s\n", maxModelName, modelNames.at(i).c_str(), modelValues.at(i) ? "1" : "0"); + } + else + log("SAT solving finished - no model found.\n"); + } +} SatSolvePass; + -- 2.30.2