aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile2
-rw-r--r--backends/firrtl/firrtl.cc63
-rw-r--r--backends/smt2/smtio.py6
-rw-r--r--frontends/ilang/ilang_lexer.l4
-rw-r--r--frontends/verilog/verilog_lexer.l15
-rw-r--r--kernel/rtlil.h17
-rw-r--r--passes/cmds/Makefile.inc1
-rw-r--r--passes/cmds/printattrs.cc90
-rw-r--r--passes/hierarchy/hierarchy.cc4
-rw-r--r--passes/sat/qbfsat.cc71
-rw-r--r--tests/various/printattr.ys14
11 files changed, 238 insertions, 49 deletions
diff --git a/Makefile b/Makefile
index cd6179879..e589b2b67 100644
--- a/Makefile
+++ b/Makefile
@@ -717,7 +717,7 @@ ifneq ($(ABCREV),default)
echo 'REEBE: NOP pbagnvaf ybpny zbqvsvpngvbaf! Frg NOPERI=qrsnhyg va Lbflf Znxrsvyr!' | tr 'A-Za-z' 'N-ZA-Mn-za-m'; false; \
fi
# set a variable so the test fails if git fails to run - when comparing outputs directly, empty string would match empty string
- $(Q) if ! (cd abc && rev="`git rev-parse $(ABCREV)`" && test "`git rev-parse HEAD`" == "$$rev"); then \
+ $(Q) if ! (cd abc 2> /dev/null && rev="`git rev-parse $(ABCREV)`" && test "`git rev-parse HEAD`" == "$$rev"); then \
test $(ABCPULL) -ne 0 || { echo 'REEBE: NOP abg hc gb qngr naq NOPCHYY frg gb 0 va Znxrsvyr!' | tr 'A-Za-z' 'N-ZA-Mn-za-m'; exit 1; }; \
echo "Pulling ABC from $(ABCURL):"; set -x; \
test -d abc || git clone $(ABCURL) abc; \
diff --git a/backends/firrtl/firrtl.cc b/backends/firrtl/firrtl.cc
index f6dae1d8c..a90b0b87a 100644
--- a/backends/firrtl/firrtl.cc
+++ b/backends/firrtl/firrtl.cc
@@ -392,7 +392,34 @@ struct FirrtlWorker
return result;
}
- void run()
+ void emit_extmodule()
+ {
+ std::string moduleFileinfo = getFileinfo(module);
+ f << stringf(" extmodule %s: %s\n", make_id(module->name), moduleFileinfo.c_str());
+ vector<std::string> port_decls;
+
+ for (auto wire : module->wires())
+ {
+ const auto wireName = make_id(wire->name);
+ std::string wireFileinfo = getFileinfo(wire);
+
+ if (wire->port_input && wire->port_output)
+ {
+ log_error("Module port %s.%s is inout!\n", log_id(module), log_id(wire));
+ }
+ port_decls.push_back(stringf(" %s %s: UInt<%d> %s\n", wire->port_input ? "input" : "output",
+ wireName, wire->width, wireFileinfo.c_str()));
+ }
+
+ for (auto &str : port_decls)
+ {
+ f << str;
+ }
+
+ f << stringf("\n");
+ }
+
+ void emit_module()
{
std::string moduleFileinfo = getFileinfo(module);
f << stringf(" module %s: %s\n", make_id(module->name), moduleFileinfo.c_str());
@@ -446,7 +473,7 @@ struct FirrtlWorker
string y_id = make_id(cell->name);
std::string cellFileinfo = getFileinfo(cell);
- if (cell->type.in(ID($not), ID($logic_not), ID($neg), ID($reduce_and), ID($reduce_or), ID($reduce_xor), ID($reduce_bool), ID($reduce_xnor)))
+ if (cell->type.in(ID($not), ID($logic_not), ID($_NOT_), ID($neg), ID($reduce_and), ID($reduce_or), ID($reduce_xor), ID($reduce_bool), ID($reduce_xnor)))
{
string a_expr = make_expr(cell->getPort(ID::A));
wire_decls.push_back(stringf(" wire %s: UInt<%d> %s\n", y_id.c_str(), y_width, cellFileinfo.c_str()));
@@ -462,7 +489,7 @@ struct FirrtlWorker
// Assume the FIRRTL width is a single bit.
firrtl_width = 1;
- if (cell->type == ID($not)) primop = "not";
+ if (cell->type.in(ID($not), ID($_NOT_))) primop = "not";
else if (cell->type == ID($neg)) {
primop = "neg";
firrtl_is_signed = true; // Result of "neg" is signed (an SInt).
@@ -494,7 +521,7 @@ struct FirrtlWorker
continue;
}
- if (cell->type.in(ID($add), ID($sub), ID($mul), ID($div), ID($mod), ID($xor), ID($xnor), ID($and), ID($or), ID($eq), ID($eqx),
+ if (cell->type.in(ID($add), ID($sub), ID($mul), ID($div), ID($mod), ID($xor), ID($_XOR_), ID($xnor), ID($and), ID($_AND_), ID($or), ID($_OR_), ID($eq), ID($eqx),
ID($gt), ID($ge), ID($lt), ID($le), ID($ne), ID($nex), ID($shr), ID($sshr), ID($sshl), ID($shl),
ID($logic_and), ID($logic_or), ID($pow)))
{
@@ -524,7 +551,7 @@ struct FirrtlWorker
// For the arithmetic ops, expand operand widths to result widths befor performing the operation.
// This corresponds (according to iverilog) to what verilog compilers implement.
- if (cell->type.in(ID($add), ID($sub), ID($mul), ID($div), ID($mod), ID($xor), ID($xnor), ID($and), ID($or)))
+ if (cell->type.in(ID($add), ID($sub), ID($mul), ID($div), ID($mod), ID($xor), ID($_XOR_), ID($xnor), ID($and), ID($_AND_), ID($or), ID($_OR_)))
{
if (a_width < y_width) {
a_expr = stringf("pad(%s, %d)", a_expr.c_str(), y_width);
@@ -560,17 +587,17 @@ struct FirrtlWorker
} else if (cell->type == ID($mod)) {
primop = "rem";
firrtl_width = min(a_width, b_width);
- } else if (cell->type == ID($and)) {
+ } else if (cell->type.in(ID($and), ID($_AND_))) {
primop = "and";
always_uint = true;
firrtl_width = max(a_width, b_width);
}
- else if (cell->type == ID($or) ) {
+ else if (cell->type.in(ID($or), ID($_OR_))) {
primop = "or";
always_uint = true;
firrtl_width = max(a_width, b_width);
}
- else if (cell->type == ID($xor)) {
+ else if (cell->type.in(ID($xor), ID($_XOR_))) {
primop = "xor";
always_uint = true;
firrtl_width = max(a_width, b_width);
@@ -694,7 +721,8 @@ struct FirrtlWorker
}
}
- if (!cell->parameters.at(ID::B_SIGNED).as_bool()) {
+ auto it = cell->parameters.find(ID::B_SIGNED);
+ if (it == cell->parameters.end() || !it->second.as_bool()) {
b_expr = "asUInt(" + b_expr + ")";
}
@@ -723,9 +751,10 @@ struct FirrtlWorker
continue;
}
- if (cell->type.in(ID($mux)))
+ if (cell->type.in(ID($mux), ID($_MUX_)))
{
- int width = cell->parameters.at(ID::WIDTH).as_int();
+ auto it = cell->parameters.find(ID::WIDTH);
+ int width = it == cell->parameters.end()? 1 : it->second.as_int();
string a_expr = make_expr(cell->getPort(ID::A));
string b_expr = make_expr(cell->getPort(ID::B));
string s_expr = make_expr(cell->getPort(ID::S));
@@ -1076,6 +1105,18 @@ struct FirrtlWorker
for (auto str : wire_exprs)
f << str;
+
+ f << stringf("\n");
+ }
+
+ void run()
+ {
+ // Blackboxes should be emitted as `extmodule`s in firrtl. Only ports are
+ // emitted in such a case.
+ if (module->get_blackbox_attribute())
+ emit_extmodule();
+ else
+ emit_module();
}
};
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index 69f59df79..62dfe7c11 100644
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -172,7 +172,7 @@ class SmtIo:
self.unroll = False
if self.solver == "yices":
- if self.noincr:
+ if self.noincr or self.forall:
self.popen_vargs = ['yices-smt2'] + self.solver_opts
else:
self.popen_vargs = ['yices-smt2', '--incremental'] + self.solver_opts
@@ -232,12 +232,16 @@ class SmtIo:
if self.logic_uf: self.logic += "UF"
if self.logic_bv: self.logic += "BV"
if self.logic_dt: self.logic = "ALL"
+ if self.solver == "yices" and self.forall: self.logic = "BV"
self.setup_done = True
for stmt in self.info_stmts:
self.write(stmt)
+ if self.forall and self.solver == "yices":
+ self.write("(set-option :yices-ef-max-iters 1000000000)")
+
if self.produce_models:
self.write("(set-option :produce-models true)")
diff --git a/frontends/ilang/ilang_lexer.l b/frontends/ilang/ilang_lexer.l
index 62f53d18e..3362ed641 100644
--- a/frontends/ilang/ilang_lexer.l
+++ b/frontends/ilang/ilang_lexer.l
@@ -91,8 +91,10 @@ USING_YOSYS_NAMESPACE
[0-9]+'[01xzm-]* { rtlil_frontend_ilang_yylval.string = strdup(yytext); return TOK_VALUE; }
-?[0-9]+ {
char *end = nullptr;
+ errno = 0;
long value = strtol(yytext, &end, 10);
- if (end != yytext + strlen(yytext))
+ log_assert(end == yytext + strlen(yytext));
+ if (errno == ERANGE)
return TOK_INVALID; // literal out of range of long
if (value < INT_MIN || value > INT_MAX)
return TOK_INVALID; // literal out of range of int (relevant mostly for LP64 platforms)
diff --git a/frontends/verilog/verilog_lexer.l b/frontends/verilog/verilog_lexer.l
index f6a3ac4db..02fa0031b 100644
--- a/frontends/verilog/verilog_lexer.l
+++ b/frontends/verilog/verilog_lexer.l
@@ -48,16 +48,18 @@ USING_YOSYS_NAMESPACE
using namespace AST;
using namespace VERILOG_FRONTEND;
+#define YYSTYPE FRONTEND_VERILOG_YYSTYPE
+#define YYLTYPE FRONTEND_VERILOG_YYLTYPE
+
YOSYS_NAMESPACE_BEGIN
namespace VERILOG_FRONTEND {
std::vector<std::string> fn_stack;
std::vector<int> ln_stack;
+ YYLTYPE real_location;
+ YYLTYPE old_location;
}
YOSYS_NAMESPACE_END
-#define YYSTYPE FRONTEND_VERILOG_YYSTYPE
-#define YYLTYPE FRONTEND_VERILOG_YYLTYPE
-
#define SV_KEYWORD(_tok) \
if (sv_mode) return _tok; \
log("Lexer warning: The SystemVerilog keyword `%s' (at %s:%d) is not "\
@@ -73,9 +75,6 @@ YOSYS_NAMESPACE_END
#define YY_INPUT(buf,result,max_size) \
result = readsome(*VERILOG_FRONTEND::lexin, buf, max_size)
-YYLTYPE real_location;
-YYLTYPE old_location;
-
#define YY_USER_ACTION \
old_location = real_location; \
real_location.first_line = real_location.last_line; \
@@ -128,7 +127,9 @@ static bool isUserType(std::string &s)
%x BASED_CONST
%%
- int comment_caller;
+ // Initialise comment_caller to something to avoid a "maybe undefined"
+ // warning from GCC.
+ int comment_caller = INITIAL;
<INITIAL,SYNOPSYS_TRANSLATE_OFF>"`file_push "[^\n]* {
fn_stack.push_back(current_filename);
diff --git a/kernel/rtlil.h b/kernel/rtlil.h
index 898c54a3a..91d6a9f77 100644
--- a/kernel/rtlil.h
+++ b/kernel/rtlil.h
@@ -298,8 +298,8 @@ namespace RTLIL
// The methods below are just convenience functions for better compatibility with std::string.
- bool operator==(const std::string &rhs) const { return str() == rhs; }
- bool operator!=(const std::string &rhs) const { return str() != rhs; }
+ bool operator==(const std::string &rhs) const { return c_str() == rhs; }
+ bool operator!=(const std::string &rhs) const { return c_str() != rhs; }
bool operator==(const char *rhs) const { return strcmp(c_str(), rhs) == 0; }
bool operator!=(const char *rhs) const { return strcmp(c_str(), rhs) != 0; }
@@ -723,7 +723,7 @@ struct RTLIL::SigBit
SigBit(const RTLIL::SigChunk &chunk);
SigBit(const RTLIL::SigChunk &chunk, int index);
SigBit(const RTLIL::SigSpec &sig);
- SigBit(const RTLIL::SigBit &sigbit);
+ SigBit(const RTLIL::SigBit &sigbit) = default;
RTLIL::SigBit &operator =(const RTLIL::SigBit &other) = default;
bool operator <(const RTLIL::SigBit &other) const;
@@ -1136,8 +1136,14 @@ public:
return design->selected_member(name, member->name);
}
- RTLIL::Wire* wire(RTLIL::IdString id) { return wires_.count(id) ? wires_.at(id) : nullptr; }
- RTLIL::Cell* cell(RTLIL::IdString id) { return cells_.count(id) ? cells_.at(id) : nullptr; }
+ RTLIL::Wire* wire(RTLIL::IdString id) {
+ auto it = wires_.find(id);
+ return it == wires_.end() ? nullptr : it->second;
+ }
+ RTLIL::Cell* cell(RTLIL::IdString id) {
+ auto it = cells_.find(id);
+ return it == cells_.end() ? nullptr : it->second;
+ }
RTLIL::ObjRange<RTLIL::Wire*> wires() { return RTLIL::ObjRange<RTLIL::Wire*>(&wires_, &refcount_wires_); }
RTLIL::ObjRange<RTLIL::Cell*> cells() { return RTLIL::ObjRange<RTLIL::Cell*>(&cells_, &refcount_cells_); }
@@ -1496,7 +1502,6 @@ inline RTLIL::SigBit::SigBit(RTLIL::Wire *wire) : wire(wire), offset(0) { log_as
inline RTLIL::SigBit::SigBit(RTLIL::Wire *wire, int offset) : wire(wire), offset(offset) { log_assert(wire != nullptr); }
inline RTLIL::SigBit::SigBit(const RTLIL::SigChunk &chunk) : wire(chunk.wire) { log_assert(chunk.width == 1); if (wire) offset = chunk.offset; else data = chunk.data[0]; }
inline RTLIL::SigBit::SigBit(const RTLIL::SigChunk &chunk, int index) : wire(chunk.wire) { if (wire) offset = chunk.offset + index; else data = chunk.data[index]; }
-inline RTLIL::SigBit::SigBit(const RTLIL::SigBit &sigbit) : wire(sigbit.wire), data(sigbit.data){ if (wire) offset = sigbit.offset; }
inline bool RTLIL::SigBit::operator<(const RTLIL::SigBit &other) const {
if (wire == other.wire)
diff --git a/passes/cmds/Makefile.inc b/passes/cmds/Makefile.inc
index a88980eaf..53bfd40c6 100644
--- a/passes/cmds/Makefile.inc
+++ b/passes/cmds/Makefile.inc
@@ -39,3 +39,4 @@ OBJS += passes/cmds/bugpoint.o
endif
OBJS += passes/cmds/scratchpad.o
OBJS += passes/cmds/logger.o
+OBJS += passes/cmds/printattrs.o
diff --git a/passes/cmds/printattrs.cc b/passes/cmds/printattrs.cc
new file mode 100644
index 000000000..80dbfa259
--- /dev/null
+++ b/passes/cmds/printattrs.cc
@@ -0,0 +1,90 @@
+/*
+ * yosys -- Yosys Open SYnthesis Suite
+ *
+ * Copyright (C) 2020 Alberto Gonzalez <boqwxp@airmail.cc>
+ *
+ * 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"
+
+USING_YOSYS_NAMESPACE
+PRIVATE_NAMESPACE_BEGIN
+
+struct PrintAttrsPass : public Pass {
+ PrintAttrsPass() : Pass("printattrs", "print attributes of selected objects") { }
+ void help() YS_OVERRIDE
+ {
+ // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+ log("\n");
+ log(" printattrs [selection]\n");
+ log("\n");
+ log("Print all attributes of the selected objects.\n");
+ log("\n");
+ log("\n");
+ }
+
+ static std::string get_indent_str(const unsigned int indent) {
+ return stringf("%*s", indent, "");
+ }
+
+ static void log_const(const RTLIL::IdString &s, const RTLIL::Const &x, const unsigned int indent) {
+ if (x.flags == RTLIL::CONST_FLAG_STRING)
+ log("%s(* %s=\"%s\" *)\n", get_indent_str(indent).c_str(), log_id(s), x.decode_string().c_str());
+ else if (x.flags == RTLIL::CONST_FLAG_NONE)
+ log("%s(* %s=%s *)\n", get_indent_str(indent).c_str(), log_id(s), x.as_string().c_str());
+ else
+ log_assert(x.flags == RTLIL::CONST_FLAG_STRING || x.flags == RTLIL::CONST_FLAG_NONE); //intended to fail
+ }
+
+ void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
+ {
+ size_t argidx = 1;
+ extra_args(args, argidx, design);
+
+ unsigned int indent = 0;
+ for (auto mod : design->selected_modules())
+ {
+ if (design->selected_whole_module(mod)) {
+ log("%s%s\n", get_indent_str(indent).c_str(), log_id(mod->name));
+ indent += 2;
+ for (auto &it : mod->attributes)
+ log_const(it.first, it.second, indent);
+ }
+
+ for (auto cell : mod->selected_cells()) {
+ log("%s%s\n", get_indent_str(indent).c_str(), log_id(cell->name));
+ indent += 2;
+ for (auto &it : cell->attributes)
+ log_const(it.first, it.second, indent);
+ indent -= 2;
+ }
+
+ for (auto wire : mod->selected_wires()) {
+ log("%s%s\n", get_indent_str(indent).c_str(), log_id(wire->name));
+ indent += 2;
+ for (auto &it : wire->attributes)
+ log_const(it.first, it.second, indent);
+ indent -= 2;
+ }
+
+ if (design->selected_whole_module(mod))
+ indent -= 2;
+ }
+
+ log("\n");
+ }
+} PrintAttrsPass;
+
+PRIVATE_NAMESPACE_END
diff --git a/passes/hierarchy/hierarchy.cc b/passes/hierarchy/hierarchy.cc
index 95d74d1eb..f99d1509d 100644
--- a/passes/hierarchy/hierarchy.cc
+++ b/passes/hierarchy/hierarchy.cc
@@ -574,9 +574,9 @@ struct HierarchyPass : public Pass {
log("\n");
log("In parametric designs, a module might exists in several variations with\n");
log("different parameter values. This pass looks at all modules in the current\n");
- log("design an re-runs the language frontends for the parametric modules as\n");
+ log("design and re-runs the language frontends for the parametric modules as\n");
log("needed. It also resolves assignments to wired logic data types (wand/wor),\n");
- log("resolves positional module parameters, unroll array instances, and more.\n");
+ log("resolves positional module parameters, unrolls array instances, and more.\n");
log("\n");
log(" -check\n");
log(" also check the design hierarchy. this generates an error when\n");
diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc
index c42760488..712a46cbc 100644
--- a/passes/sat/qbfsat.cc
+++ b/passes/sat/qbfsat.cc
@@ -41,6 +41,7 @@ struct QbfSolveOptions {
bool specialize, specialize_from_file, write_solution, nocleanup, dump_final_smt2, assume_outputs, assume_neg;
bool nooptimize, nobisection;
bool sat, unsat, show_smtbmc;
+ enum Solver{Z3, Yices, CVC4} solver;
std::string specialize_soln_file;
std::string write_soln_soln_file;
std::string dump_final_smt2_file;
@@ -48,9 +49,21 @@ struct QbfSolveOptions {
QbfSolveOptions() : specialize(false), specialize_from_file(false), write_solution(false),
nocleanup(false), dump_final_smt2(false), assume_outputs(false), assume_neg(false),
nooptimize(false), nobisection(false), sat(false), unsat(false), show_smtbmc(false),
- argidx(0) {};
+ solver(Yices), argidx(0) {};
};
+std::string get_solver_name(const QbfSolveOptions &opt) {
+ if (opt.solver == opt.Solver::Z3)
+ return "z3";
+ else if (opt.solver == opt.Solver::Yices)
+ return "yices";
+ else if (opt.solver == opt.Solver::CVC4)
+ return "cvc4";
+ else
+ log_cmd_error("unknown solver specified.\n");
+ return "";
+}
+
void recover_solution(QbfSolutionType &sol) {
YS_REGEX_TYPE sat_regex = YS_REGEX_COMPILE("Status: PASSED");
YS_REGEX_TYPE unsat_regex = YS_REGEX_COMPILE("Solver Error.*model is not available");
@@ -315,19 +328,18 @@ QbfSolutionType call_qbf_solver(RTLIL::Module *mod, const QbfSolveOptions &opt,
QbfSolutionType ret;
const std::string yosys_smtbmc_exe = proc_self_dirname() + "yosys-smtbmc";
const std::string smt2_command = "write_smt2 -stbv -wires " + tempdir_name + "/problem" + (iter_num != 0? stringf("%d", iter_num) : "") + ".smt2";
- const std::string smtbmc_cmd = yosys_smtbmc_exe + " -s z3 -t 1 -g --binary " + (opt.dump_final_smt2? "--dump-smt2 " + opt.dump_final_smt2_file + " " : "") + tempdir_name + "/problem" + (iter_num != 0? stringf("%d", iter_num) : "") + ".smt2 2>&1";
const std::string smtbmc_warning = "z3: WARNING:";
- const bool show_smtbmc = opt.show_smtbmc;
+ const std::string smtbmc_cmd = yosys_smtbmc_exe + " -s " + (get_solver_name(opt)) + " -t 1 -g --binary " + (opt.dump_final_smt2? "--dump-smt2 " + opt.dump_final_smt2_file + " " : "") + tempdir_name + "/problem" + (iter_num != 0? stringf("%d", iter_num) : "") + ".smt2 2>&1";
Pass::call(mod->design, smt2_command);
- auto process_line = [&ret, &smtbmc_warning, &show_smtbmc, &quiet](const std::string &line) {
+ auto process_line = [&ret, &smtbmc_warning, &opt, &quiet](const std::string &line) {
ret.stdout_lines.push_back(line.substr(0, line.size()-1)); //don't include trailing newline
auto warning_pos = line.find(smtbmc_warning);
if (warning_pos != std::string::npos)
log_warning("%s", line.substr(warning_pos + smtbmc_warning.size() + 1).c_str());
else
- if (show_smtbmc && !quiet)
+ if (opt.show_smtbmc && !quiet)
log("smtbmc output: %s", line.c_str());
};
log_header(mod->design, "Solving QBF-SAT problem.\n");
@@ -486,6 +498,22 @@ QbfSolveOptions parse_args(const std::vector<std::string> &args) {
opt.nobisection = true;
continue;
}
+ else if (args[opt.argidx] == "-solver") {
+ if (args.size() <= opt.argidx + 1)
+ log_cmd_error("solver not specified.\n");
+ else {
+ if (args[opt.argidx+1] == "z3")
+ opt.solver = opt.Solver::Z3;
+ else if (args[opt.argidx+1] == "yices")
+ opt.solver = opt.Solver::Yices;
+ else if (args[opt.argidx+1] == "cvc4")
+ opt.solver = opt.Solver::CVC4;
+ else
+ log_cmd_error("Unknown solver \"%s\".\n", args[opt.argidx+1].c_str());
+ opt.argidx++;
+ }
+ continue;
+ }
else if (args[opt.argidx] == "-sat") {
opt.sat = true;
continue;
@@ -563,21 +591,20 @@ struct QbfSatPass : public Pass {
log("\n");
log(" qbfsat [options] [selection]\n");
log("\n");
- log("This command solves a 2QBF-SAT problem defined over the currently selected module.\n");
- log("Existentially-quantified variables are declared by assigning a wire \"$anyconst\".\n");
- log("Universally-quantified variables may be explicitly declared by assigning a wire\n");
- log("\"$allconst\", but module inputs will be treated as universally-quantified variables\n");
- log("by default.\n");
+ log("This command solves an \"exists-forall\" 2QBF-SAT problem defined over the currently\n");
+ log("selected module. Existentially-quantified variables are declared by assigning a wire\n");
+ log("\"$anyconst\". Universally-quantified variables may be explicitly declared by assigning\n");
+ log("a wire \"$allconst\", but module inputs will be treated as universally-quantified\n");
+ log("variables by default.\n");
log("\n");
log(" -nocleanup\n");
- log(" Do not delete temporary files and directories. Useful for\n");
- log(" debugging.\n");
+ log(" Do not delete temporary files and directories. Useful for debugging.\n");
log("\n");
log(" -dump-final-smt2 <file>\n");
log(" Pass the --dump-smt2 option to yosys-smtbmc.\n");
log("\n");
log(" -assume-outputs\n");
- log(" Add an $assume cell for the conjunction of all one-bit module output wires.\n");
+ log(" Add an \"$assume\" cell for the conjunction of all one-bit module output wires.\n");
log("\n");
log(" -assume-negative-polarity\n");
log(" When adding $assume cells for one-bit module output wires, assume they are\n");
@@ -586,15 +613,18 @@ struct QbfSatPass : public Pass {
log("\n");
log(" -nooptimize\n");
log(" Ignore \"\\minimize\" and \"\\maximize\" attributes, do not emit \"(maximize)\" or\n");
- log(" \"(minimize)\" in the SMTLIBv2, and generally make no attempt to optimize anything.\n");
+ log(" \"(minimize)\" in the SMT-LIBv2, and generally make no attempt to optimize anything.\n");
log("\n");
log(" -nobisection\n");
log(" If a wire is marked with the \"\\minimize\" or \"\\maximize\" attribute, do not\n");
log(" attempt to optimize that value with the default iterated solving and threshold\n");
log(" bisection approach. Instead, have yosys-smtbmc emit a \"(minimize)\" or \"(maximize)\"\n");
- log(" command in the SMTLIBv2 output and hope that the solver supports optimizing\n");
+ log(" command in the SMT-LIBv2 output and hope that the solver supports optimizing\n");
log(" quantified bitvector problems.\n");
log("\n");
+ log(" -solver <solver>\n");
+ log(" Use a particular solver. Choose one of: \"z3\", \"yices\", and \"cvc4\".\n");
+ log("\n");
log(" -sat\n");
log(" Generate an error if the solver does not return \"sat\".\n");
log("\n");
@@ -605,15 +635,16 @@ struct QbfSatPass : public Pass {
log(" Print the output from yosys-smtbmc.\n");
log("\n");
log(" -specialize\n");
- log(" Replace all \"$anyconst\" cells with constant values determined by the solver.\n");
+ log(" If the problem is satisfiable, replace each \"$anyconst\" cell with its\n");
+ log(" corresponding constant value from the model produced by the solver.\n");
log("\n");
log(" -specialize-from-file <solution file>\n");
- log(" Do not run the solver, but instead only attempt to replace all \"$anyconst\"\n");
- log(" cells in the current module with values provided by the specified file.\n");
+ log(" Do not run the solver, but instead only attempt to replace each \"$anyconst\"\n");
+ log(" cell in the current module with a constant value provided by the specified file.\n");
log("\n");
log(" -write-solution <solution file>\n");
- log(" Write the assignments discovered by the solver for all \"$anyconst\" cells\n");
- log(" to the specified file.");
+ log(" If the problem is satisfiable, write the corresponding constant value for each\n");
+ log(" \"$anyconst\" cell from the model produced by the solver to the specified file.");
log("\n");
log("\n");
}
diff --git a/tests/various/printattr.ys b/tests/various/printattr.ys
new file mode 100644
index 000000000..afc6d8eb6
--- /dev/null
+++ b/tests/various/printattr.ys
@@ -0,0 +1,14 @@
+logger -expect log ".*cells_not_processed=[01]* .*" 1
+logger -expect log ".*src=.<<EOT:1\.1-9\.10. .*" 1
+read_verilog <<EOT
+module mux2(a, b, s, y);
+ input a, b, s;
+ output y;
+
+ wire s_n = ~s;
+ wire t0 = s & a;
+ wire t1 = s_n & b;
+ assign y = t0 | t1;
+endmodule
+EOT
+printattrs
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-12 18:23:52 +0000