aboutsummaryrefslogtreecommitdiffstats
path: root/backends
diff options
context:
space:
mode:
Diffstat (limited to 'backends')
-rw-r--r--backends/aiger/xaiger.cc4
-rw-r--r--backends/cxxrtl/cxxrtl.cc97
-rw-r--r--backends/firrtl/firrtl.cc80
-rw-r--r--backends/json/json.cc44
-rw-r--r--backends/smt2/Makefile.inc14
-rw-r--r--backends/smt2/smtbmc.py21
-rw-r--r--backends/verilog/verilog_backend.cc2
7 files changed, 197 insertions, 65 deletions
diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc
index 3b51d8685..3c7c745fe 100644
--- a/backends/aiger/xaiger.cc
+++ b/backends/aiger/xaiger.cc
@@ -280,6 +280,10 @@ struct XAigerWriter
if (abc9_flop)
continue;
}
+ else {
+ if (cell->type == ID($__ABC9_DELAY))
+ log_error("Cell type '%s' not recognised. Check that '+/abc9_model.v' has been read.\n", cell->type.c_str());
+ }
bool cell_known = inst_module || cell->known();
for (const auto &c : cell->connections()) {
diff --git a/backends/cxxrtl/cxxrtl.cc b/backends/cxxrtl/cxxrtl.cc
index 465882858..d1a855bf0 100644
--- a/backends/cxxrtl/cxxrtl.cc
+++ b/backends/cxxrtl/cxxrtl.cc
@@ -357,13 +357,19 @@ struct FlowGraph {
};
struct CxxrtlWorker {
+ bool split_intf = false;
+ std::string intf_filename;
+ std::string design_ns = "cxxrtl_design";
+ std::ostream *impl_f = nullptr;
+ std::ostream *intf_f = nullptr;
+
bool elide_internal = false;
bool elide_public = false;
bool localize_internal = false;
bool localize_public = false;
bool run_splitnets = false;
- std::ostream &f;
+ std::ostringstream f;
std::string indent;
int temporary = 0;
@@ -377,8 +383,6 @@ struct CxxrtlWorker {
dict<const RTLIL::Module*, std::vector<FlowGraph::Node>> schedule;
pool<const RTLIL::Wire*> localized_wires;
- CxxrtlWorker(std::ostream &f) : f(f) {}
-
void inc_indent() {
indent += "\t";
}
@@ -867,7 +871,8 @@ struct CxxrtlWorker {
dump_sigspec_rhs(cell->getPort(ID(ADDR)));
f << ", " << memory->start_offset << ", " << memory->size << ");\n";
if (cell->type == ID($memrd)) {
- if (!cell->getPort(ID(EN)).is_fully_ones()) {
+ bool has_enable = cell->getParam(ID(CLK_ENABLE)).as_bool() && !cell->getPort(ID(EN)).is_fully_ones();
+ if (has_enable) {
f << indent << "if (";
dump_sigspec_rhs(cell->getPort(ID(EN)));
f << ") {\n";
@@ -926,7 +931,7 @@ struct CxxrtlWorker {
f << " = value<" << memory->width << "> {};\n";
dec_indent();
f << indent << "}\n";
- if (!cell->getPort(ID(EN)).is_fully_ones()) {
+ if (has_enable) {
dec_indent();
f << indent << "}\n";
}
@@ -970,6 +975,8 @@ struct CxxrtlWorker {
continue;
}
if (cell->output(conn.first)) {
+ if (conn.second.empty())
+ continue; // ignore disconnected ports
f << indent;
dump_sigspec_lhs(conn.second);
f << " = " << mangle(cell) << "." << mangle_wire_name(conn.first) << ".curr;\n";
@@ -1191,7 +1198,7 @@ struct CxxrtlWorker {
}
}
- void dump_module(RTLIL::Module *module)
+ void dump_module_intf(RTLIL::Module *module)
{
dump_attrs(module);
f << "struct " << mangle(module) << " : public module {\n";
@@ -1220,7 +1227,10 @@ struct CxxrtlWorker {
dec_indent();
f << "}; // struct " << mangle(module) << "\n";
f << "\n";
+ }
+ void dump_module_impl(RTLIL::Module *module)
+ {
f << "void " << mangle(module) << "::eval() {\n";
inc_indent();
for (auto wire : module->wires())
@@ -1323,18 +1333,49 @@ struct CxxrtlWorker {
}
log_assert(topo_design.sort());
- f << "#include <cxxrtl.h>\n";
+ if (split_intf) {
+ // The only thing more depraved than include guards, is mangling filenames to turn them into include guards.
+ std::string include_guard = design_ns + "_header";
+ std::transform(include_guard.begin(), include_guard.end(), include_guard.begin(), ::toupper);
+
+ f << "#ifndef " << include_guard << "\n";
+ f << "#define " << include_guard << "\n";
+ f << "\n";
+ f << "#include <backends/cxxrtl/cxxrtl.h>\n";
+ f << "\n";
+ f << "using namespace cxxrtl;\n";
+ f << "\n";
+ f << "namespace " << design_ns << " {\n";
+ f << "\n";
+ for (auto module : topo_design.sorted) {
+ if (!design->selected_module(module))
+ continue;
+ dump_module_intf(module);
+ }
+ f << "} // namespace " << design_ns << "\n";
+ f << "\n";
+ f << "#endif\n";
+ *intf_f << f.str(); f.str("");
+ }
+
+ if (split_intf)
+ f << "#include \"" << intf_filename << "\"\n";
+ else
+ f << "#include <backends/cxxrtl/cxxrtl.h>\n";
f << "\n";
f << "using namespace cxxrtl_yosys;\n";
f << "\n";
- f << "namespace cxxrtl_design {\n";
+ f << "namespace " << design_ns << " {\n";
f << "\n";
for (auto module : topo_design.sorted) {
if (!design->selected_module(module))
continue;
- dump_module(module);
+ if (!split_intf)
+ dump_module_intf(module);
+ dump_module_impl(module);
}
- f << "} // namespace cxxrtl_design\n";
+ f << "} // namespace " << design_ns << "\n";
+ *impl_f << f.str(); f.str("");
}
// Edge-type sync rules require us to emit edge detectors, which require coordination between
@@ -1618,6 +1659,16 @@ struct CxxrtlBackend : public Backend {
log("\n");
log("The following options are supported by this backend:\n");
log("\n");
+ log(" -header\n");
+ log(" generate separate interface (.h) and implementation (.cc) files.\n");
+ log(" if specified, the backend must be called with a filename, and filename\n");
+ log(" of the interface is derived from filename of the implementation.\n");
+ log(" otherwise, interface and implementation are generated together.\n");
+ log("\n");
+ log(" -namespace <ns-name>\n");
+ log(" place the generated code into namespace <ns-name>. if not specified,\n");
+ log(" \"cxxrtl_design\" is used.\n");
+ log("\n");
log(" -O <level>\n");
log(" set the optimization level. the default is -O%d. higher optimization\n", DEFAULT_OPT_LEVEL);
log(" levels dramatically decrease compile and run time, and highest level\n");
@@ -1645,6 +1696,7 @@ struct CxxrtlBackend : public Backend {
void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
{
int opt_level = DEFAULT_OPT_LEVEL;
+ CxxrtlWorker worker;
log_header(design, "Executing CXXRTL backend.\n");
@@ -1659,11 +1711,18 @@ struct CxxrtlBackend : public Backend {
opt_level = std::stoi(args[argidx].substr(2));
continue;
}
+ if (args[argidx] == "-header") {
+ worker.split_intf = true;
+ continue;
+ }
+ if (args[argidx] == "-namespace" && argidx+1 < args.size()) {
+ worker.design_ns = args[++argidx];
+ continue;
+ }
break;
}
extra_args(f, filename, args, argidx);
- CxxrtlWorker worker(*f);
switch (opt_level) {
case 5:
worker.run_splitnets = true;
@@ -1680,6 +1739,22 @@ struct CxxrtlBackend : public Backend {
default:
log_cmd_error("Invalid optimization level %d.\n", opt_level);
}
+
+ std::ofstream intf_f;
+ if (worker.split_intf) {
+ if (filename == "<stdout>")
+ log_cmd_error("Option -header must be used with a filename.\n");
+
+ worker.intf_filename = filename.substr(0, filename.rfind('.')) + ".h";
+ intf_f.open(worker.intf_filename, std::ofstream::trunc);
+ if (intf_f.fail())
+ log_cmd_error("Can't open file `%s' for writing: %s\n",
+ worker.intf_filename.c_str(), strerror(errno));
+
+ worker.intf_f = &intf_f;
+ }
+ worker.impl_f = f;
+
worker.prepare_design(design);
worker.dump_design(design);
}
diff --git a/backends/firrtl/firrtl.cc b/backends/firrtl/firrtl.cc
index 1f750b359..fd7f20cc6 100644
--- a/backends/firrtl/firrtl.cc
+++ b/backends/firrtl/firrtl.cc
@@ -42,6 +42,13 @@ static const FDirection FD_OUT = 0x2;
static const FDirection FD_INOUT = 0x3;
static const int FIRRTL_MAX_DSH_WIDTH_ERROR = 20; // For historic reasons, this is actually one greater than the maximum allowed shift width
+std::string getFileinfo(const RTLIL::AttrObject *design_entity)
+{
+ std::string src(design_entity->get_src_attribute());
+ std::string fileinfo_str = src.empty() ? "" : "@[" + src + "]";
+ return fileinfo_str;
+}
+
// Get a port direction with respect to a specific module.
FDirection getPortFDirection(IdString id, Module *module)
{
@@ -192,9 +199,10 @@ struct FirrtlWorker
if (this->width == 0) {
log_error("Memory %s has zero width%s\n", this->name.c_str(), this->atLine());
}
- }
+ }
+
// We need a default constructor for the dict insert.
- memory() : pCell(0), read_latency(0), write_latency(1), init_file(""), init_file_srcFileSpec(""){}
+ memory() : pCell(0), read_latency(0), write_latency(1), init_file(""), init_file_srcFileSpec(""){}
const char *atLine() {
if (srcLine == "") {
@@ -329,7 +337,8 @@ struct FirrtlWorker
log_warning("No instance for %s.%s\n", cell_type.c_str(), cell_name.c_str());
return;
}
- wire_exprs.push_back(stringf("%s" "inst %s%s of %s", indent.c_str(), cell_name.c_str(), cell_name_comment.c_str(), instanceOf.c_str()));
+ std::string cellFileinfo = getFileinfo(cell);
+ wire_exprs.push_back(stringf("%s" "inst %s%s of %s %s", indent.c_str(), cell_name.c_str(), cell_name_comment.c_str(), instanceOf.c_str(), cellFileinfo.c_str()));
for (auto it = cell->connections().begin(); it != cell->connections().end(); ++it) {
if (it->second.size() > 0) {
@@ -370,7 +379,7 @@ struct FirrtlWorker
// as part of the coalesced subfield assignments for this wire.
register_reverse_wire_map(sourceExpr, *sinkSig);
} else {
- wire_exprs.push_back(stringf("\n%s%s <= %s", indent.c_str(), sinkExpr.c_str(), sourceExpr.c_str()));
+ wire_exprs.push_back(stringf("\n%s%s <= %s %s", indent.c_str(), sinkExpr.c_str(), sourceExpr.c_str(), cellFileinfo.c_str()));
}
}
}
@@ -394,12 +403,15 @@ struct FirrtlWorker
void run()
{
- f << stringf(" module %s:\n", make_id(module->name));
+ std::string moduleFileinfo = getFileinfo(module);
+ f << stringf(" module %s: %s\n", make_id(module->name), moduleFileinfo.c_str());
vector<string> port_decls, wire_decls, cell_exprs, wire_exprs;
for (auto wire : module->wires())
{
const auto wireName = make_id(wire->name);
+ std::string wireFileinfo = getFileinfo(wire);
+
// If a wire has initial data, issue a warning since FIRRTL doesn't currently support it.
if (wire->attributes.count(ID::init)) {
log_warning("Initial value (%s) for (%s.%s) not supported\n",
@@ -410,12 +422,12 @@ struct FirrtlWorker
{
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>\n", wire->port_input ? "input" : "output",
- wireName, wire->width));
+ port_decls.push_back(stringf(" %s %s: UInt<%d> %s\n", wire->port_input ? "input" : "output",
+ wireName, wire->width, wireFileinfo.c_str()));
}
else
{
- wire_decls.push_back(stringf(" wire %s: UInt<%d>\n", wireName, wire->width));
+ wire_decls.push_back(stringf(" wire %s: UInt<%d> %s\n", wireName, wire->width, wireFileinfo.c_str()));
}
}
@@ -423,7 +435,7 @@ struct FirrtlWorker
{
static Const ndef(0, 0);
- // Is this cell is a module instance?
+ // Is this cell is a module instance?
if (cell->type[0] != '$')
{
process_instance(cell, wire_exprs);
@@ -441,11 +453,12 @@ struct FirrtlWorker
string primop;
bool always_uint = false;
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)))
{
string a_expr = make_expr(cell->getPort(ID::A));
- wire_decls.push_back(stringf(" wire %s: UInt<%d>\n", y_id.c_str(), y_width));
+ wire_decls.push_back(stringf(" wire %s: UInt<%d> %s\n", y_id.c_str(), y_width, cellFileinfo.c_str()));
if (a_signed) {
a_expr = "asSInt(" + a_expr + ")";
@@ -464,16 +477,16 @@ struct FirrtlWorker
firrtl_is_signed = true; // Result of "neg" is signed (an SInt).
firrtl_width = a_width;
} else if (cell->type == ID($logic_not)) {
- primop = "eq";
- a_expr = stringf("%s, UInt(0)", a_expr.c_str());
- }
+ primop = "eq";
+ a_expr = stringf("%s, UInt(0)", a_expr.c_str());
+ }
else if (cell->type == ID($reduce_and)) primop = "andr";
else if (cell->type == ID($reduce_or)) primop = "orr";
else if (cell->type == ID($reduce_xor)) primop = "xorr";
else if (cell->type == ID($reduce_xnor)) {
- primop = "not";
- a_expr = stringf("xorr(%s)", a_expr.c_str());
- }
+ primop = "not";
+ a_expr = stringf("xorr(%s)", a_expr.c_str());
+ }
else if (cell->type == ID($reduce_bool)) {
primop = "neq";
// Use the sign of the a_expr and its width as the type (UInt/SInt) and width of the comparand.
@@ -485,18 +498,19 @@ struct FirrtlWorker
if ((firrtl_is_signed && !always_uint))
expr = stringf("asUInt(%s)", expr.c_str());
- cell_exprs.push_back(stringf(" %s <= %s\n", y_id.c_str(), expr.c_str()));
+ cell_exprs.push_back(stringf(" %s <= %s %s\n", y_id.c_str(), expr.c_str(), cellFileinfo.c_str()));
register_reverse_wire_map(y_id, cell->getPort(ID::Y));
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),
- 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)))
+ 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)))
{
string a_expr = make_expr(cell->getPort(ID::A));
string b_expr = make_expr(cell->getPort(ID::B));
- wire_decls.push_back(stringf(" wire %s: UInt<%d>\n", y_id.c_str(), y_width));
+ std::string cellFileinfo = getFileinfo(cell);
+ wire_decls.push_back(stringf(" wire %s: UInt<%d> %s\n", y_id.c_str(), y_width, cellFileinfo.c_str()));
if (a_signed) {
a_expr = "asSInt(" + a_expr + ")";
@@ -579,7 +593,7 @@ struct FirrtlWorker
primop = "eq";
always_uint = true;
firrtl_width = 1;
- }
+ }
else if ((cell->type == ID($ne)) | (cell->type == ID($nex))) {
primop = "neq";
always_uint = true;
@@ -712,7 +726,7 @@ struct FirrtlWorker
if ((firrtl_is_signed && !always_uint))
expr = stringf("asUInt(%s)", expr.c_str());
- cell_exprs.push_back(stringf(" %s <= %s\n", y_id.c_str(), expr.c_str()));
+ cell_exprs.push_back(stringf(" %s <= %s %s\n", y_id.c_str(), expr.c_str(), cellFileinfo.c_str()));
register_reverse_wire_map(y_id, cell->getPort(ID::Y));
continue;
@@ -724,11 +738,11 @@ struct FirrtlWorker
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));
- wire_decls.push_back(stringf(" wire %s: UInt<%d>\n", y_id.c_str(), width));
+ wire_decls.push_back(stringf(" wire %s: UInt<%d> %s\n", y_id.c_str(), width, cellFileinfo.c_str()));
string expr = stringf("mux(%s, %s, %s)", s_expr.c_str(), b_expr.c_str(), a_expr.c_str());
- cell_exprs.push_back(stringf(" %s <= %s\n", y_id.c_str(), expr.c_str()));
+ cell_exprs.push_back(stringf(" %s <= %s %s\n", y_id.c_str(), expr.c_str(), cellFileinfo.c_str()));
register_reverse_wire_map(y_id, cell->getPort(ID::Y));
continue;
@@ -867,9 +881,9 @@ struct FirrtlWorker
string expr = make_expr(cell->getPort(ID::D));
string clk_expr = "asClock(" + make_expr(cell->getPort(ID::CLK)) + ")";
- wire_decls.push_back(stringf(" reg %s: UInt<%d>, %s\n", y_id.c_str(), width, clk_expr.c_str()));
+ wire_decls.push_back(stringf(" reg %s: UInt<%d>, %s %s\n", y_id.c_str(), width, clk_expr.c_str(), cellFileinfo.c_str()));
- cell_exprs.push_back(stringf(" %s <= %s\n", y_id.c_str(), expr.c_str()));
+ cell_exprs.push_back(stringf(" %s <= %s %s\n", y_id.c_str(), expr.c_str(), cellFileinfo.c_str()));
register_reverse_wire_map(y_id, cell->getPort(ID::Q));
continue;
@@ -959,6 +973,7 @@ struct FirrtlWorker
for (auto wire : module->wires())
{
string expr;
+ std::string wireFileinfo = getFileinfo(wire);
if (wire->port_input)
continue;
@@ -1017,14 +1032,20 @@ struct FirrtlWorker
if (is_valid) {
if (make_unconn_id) {
- wire_decls.push_back(stringf(" wire %s: UInt<1>\n", unconn_id.c_str()));
+ wire_decls.push_back(stringf(" wire %s: UInt<1> %s\n", unconn_id.c_str(), wireFileinfo.c_str()));
+ // `invalid` is a firrtl construction for simulation so we will not
+ // tag it with a @[fileinfo] tag as it doesn't directly correspond to
+ // a specific line of verilog code.
wire_decls.push_back(stringf(" %s is invalid\n", unconn_id.c_str()));
}
- wire_exprs.push_back(stringf(" %s <= %s\n", make_id(wire->name), expr.c_str()));
+ wire_exprs.push_back(stringf(" %s <= %s %s\n", make_id(wire->name), expr.c_str(), wireFileinfo.c_str()));
} else {
if (make_unconn_id) {
unconn_id.clear();
}
+ // `invalid` is a firrtl construction for simulation so we will not
+ // tag it with a @[fileinfo] tag as it doesn't directly correspond to
+ // a specific line of verilog code.
wire_decls.push_back(stringf(" %s is invalid\n", make_id(wire->name)));
}
}
@@ -1123,7 +1144,8 @@ struct FirrtlBackend : public Backend {
if (top == nullptr)
top = last;
- *f << stringf("circuit %s:\n", make_id(top->name));
+ std::string circuitFileinfo = getFileinfo(top);
+ *f << stringf("circuit %s: %s\n", make_id(top->name), circuitFileinfo.c_str());
for (auto module : design->modules())
{
diff --git a/backends/json/json.cc b/backends/json/json.cc
index 6c924ff99..1da23bb7d 100644
--- a/backends/json/json.cc
+++ b/backends/json/json.cc
@@ -303,8 +303,13 @@ struct JsonBackend : public Backend {
log("The general syntax of the JSON output created by this command is as follows:\n");
log("\n");
log(" {\n");
+ log(" \"creator\": \"Yosys <version info>\",\n");
log(" \"modules\": {\n");
log(" <module_name>: {\n");
+ log(" \"attributes\": {\n");
+ log(" <attribute_name>: <attribute_value>,\n");
+ log(" ...\n");
+ log(" },\n");
log(" \"ports\": {\n");
log(" <port_name>: <port_details>,\n");
log(" ...\n");
@@ -329,13 +334,19 @@ struct JsonBackend : public Backend {
log(" {\n");
log(" \"direction\": <\"input\" | \"output\" | \"inout\">,\n");
log(" \"bits\": <bit_vector>\n");
+ log(" \"offset\": <the lowest bit index in use, if non-0>\n");
+ log(" \"upto\": <1 if the port bit indexing is MSB-first>\n");
log(" }\n");
log("\n");
+ log("The \"offset\" and \"upto\" fields are skipped if their value would be 0.");
+ log("They don't affect connection semantics, and are only used to preserve original");
+ log("HDL bit indexing.");
log("And <cell_details> is:\n");
log("\n");
log(" {\n");
log(" \"hide_name\": <1 | 0>,\n");
log(" \"type\": <cell_type>,\n");
+ log(" \"model\": <AIG model name, if -aig option used>,\n");
log(" \"parameters\": {\n");
log(" <parameter_name>: <parameter_value>,\n");
log(" ...\n");
@@ -359,6 +370,8 @@ struct JsonBackend : public Backend {
log(" {\n");
log(" \"hide_name\": <1 | 0>,\n");
log(" \"bits\": <bit_vector>\n");
+ log(" \"offset\": <the lowest bit index in use, if non-0>\n");
+ log(" \"upto\": <1 if the port bit indexing is MSB-first>\n");
log(" }\n");
log("\n");
log("The \"hide_name\" fields are set to 1 when the name of this cell or net is\n");
@@ -386,9 +399,15 @@ struct JsonBackend : public Backend {
log("\n");
log("Translates to the following JSON output:\n");
log("\n");
+
log(" {\n");
+ log(" \"creator\": \"Yosys 0.9+2406 (git sha1 fb1168d8, clang 9.0.1 -fPIC -Os)\",\n");
log(" \"modules\": {\n");
log(" \"test\": {\n");
+ log(" \"attributes\": {\n");
+ log(" \"cells_not_processed\": \"00000000000000000000000000000001\",\n");
+ log(" \"src\": \"test.v:1.1-4.10\"\n");
+ log(" },\n");
log(" \"ports\": {\n");
log(" \"x\": {\n");
log(" \"direction\": \"input\",\n");
@@ -404,33 +423,34 @@ struct JsonBackend : public Backend {
log(" \"hide_name\": 0,\n");
log(" \"type\": \"foo\",\n");
log(" \"parameters\": {\n");
- log(" \"Q\": 1337,\n");
- log(" \"P\": 42\n");
+ log(" \"P\": \"00000000000000000000000000101010\",\n");
+ log(" \"Q\": \"00000000000000000000010100111001\"\n");
log(" },\n");
log(" \"attributes\": {\n");
- log(" \"keep\": 1,\n");
- log(" \"src\": \"test.v:2\"\n");
+ log(" \"keep\": \"00000000000000000000000000000001\",\n");
+ log(" \"module_not_derived\": \"00000000000000000000000000000001\",\n");
+ log(" \"src\": \"test.v:3.1-3.55\"\n");
log(" },\n");
log(" \"connections\": {\n");
- log(" \"C\": [ 2, 2, 2, 2, \"0\", \"1\", \"0\", \"1\" ],\n");
+ log(" \"A\": [ 3, 2 ],\n");
log(" \"B\": [ 2, 3 ],\n");
- log(" \"A\": [ 3, 2 ]\n");
+ log(" \"C\": [ 2, 2, 2, 2, \"0\", \"1\", \"0\", \"1\" ]\n");
log(" }\n");
log(" }\n");
log(" },\n");
log(" \"netnames\": {\n");
- log(" \"y\": {\n");
+ log(" \"x\": {\n");
log(" \"hide_name\": 0,\n");
- log(" \"bits\": [ 3 ],\n");
+ log(" \"bits\": [ 2 ],\n");
log(" \"attributes\": {\n");
- log(" \"src\": \"test.v:1\"\n");
+ log(" \"src\": \"test.v:1.19-1.20\"\n");
log(" }\n");
log(" },\n");
- log(" \"x\": {\n");
+ log(" \"y\": {\n");
log(" \"hide_name\": 0,\n");
- log(" \"bits\": [ 2 ],\n");
+ log(" \"bits\": [ 3 ],\n");
log(" \"attributes\": {\n");
- log(" \"src\": \"test.v:1\"\n");
+ log(" \"src\": \"test.v:1.22-1.23\"\n");
log(" }\n");
log(" }\n");
log(" }\n");
diff --git a/backends/smt2/Makefile.inc b/backends/smt2/Makefile.inc
index 68394a909..fb01308bd 100644
--- a/backends/smt2/Makefile.inc
+++ b/backends/smt2/Makefile.inc
@@ -6,23 +6,23 @@ ifneq ($(CONFIG),emcc)
# MSYS targets support yosys-smtbmc, but require a launcher script
ifeq ($(CONFIG),$(filter $(CONFIG),msys2 msys2-64))
-TARGETS += yosys-smtbmc.exe yosys-smtbmc-script.py
+TARGETS += $(PROGRAM_PREFIX)yosys-smtbmc.exe $(PROGRAM_PREFIX)yosys-smtbmc-script.py
# Needed to find the Python interpreter for yosys-smtbmc scripts.
# Override if necessary, it is only used for msys2 targets.
PYTHON := $(shell cygpath -w -m $(PREFIX)/bin/python3)
-yosys-smtbmc-script.py: backends/smt2/smtbmc.py
- $(P) sed -e 's|##yosys-sys-path##|sys.path += [os.path.dirname(os.path.realpath(__file__)) + p for p in ["/share/python3", "/../share/yosys/python3"]]|;' \
+$(PROGRAM_PREFIX)yosys-smtbmc-script.py: backends/smt2/smtbmc.py
+ $(P) sed -e 's|##yosys-sys-path##|sys.path += [os.path.dirname(os.path.realpath(__file__)) + p for p in ["/share/python3", "/../share/$(PROGRAM_PREFIX)yosys/python3"]]|;' \
-e "s|#!/usr/bin/env python3|#!$(PYTHON)|" < $< > $@
-yosys-smtbmc.exe: misc/launcher.c yosys-smtbmc-script.py
+$(PROGRAM_PREFIX)yosys-smtbmc.exe: misc/launcher.c $(PROGRAM_PREFIX)yosys-smtbmc-script.py
$(P) $(CXX) -DGUI=0 -O -s -o $@ $<
# Other targets
else
-TARGETS += yosys-smtbmc
+TARGETS += $(PROGRAM_PREFIX)yosys-smtbmc
-yosys-smtbmc: backends/smt2/smtbmc.py
- $(P) sed 's|##yosys-sys-path##|sys.path += [os.path.dirname(os.path.realpath(__file__)) + p for p in ["/share/python3", "/../share/yosys/python3"]]|;' < $< > $@.new
+$(PROGRAM_PREFIX)yosys-smtbmc: backends/smt2/smtbmc.py
+ $(P) sed 's|##yosys-sys-path##|sys.path += [os.path.dirname(os.path.realpath(__file__)) + p for p in ["/share/python3", "/../share/$(PROGRAM_PREFIX)yosys/python3"]]|;' < $< > $@.new
$(Q) chmod +x $@.new
$(Q) mv $@.new $@
endif
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index 630464419..d3015b066 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -49,12 +49,12 @@ presat = False
smtcinit = False
smtctop = None
noinit = False
+binarymode = False
so = SmtOpts()
def usage():
- print("""
-yosys-smtbmc [options] <yosys_smt2_output>
+ print(os.path.basename(sys.argv[0]) + """ [options] <yosys_smt2_output>
-t <num_steps>
-t <skip_steps>:<num_steps>
@@ -150,6 +150,9 @@ yosys-smtbmc [options] <yosys_smt2_output>
add <num_steps> time steps at the end of the trace
when creating a counter example (this additional time
steps will still be constrained by assumptions)
+
+ --binary
+ dump anyconst values as raw bit strings
""" + so.helpmsg())
sys.exit(1)
@@ -158,7 +161,7 @@ try:
opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igcm:", so.longopts +
["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "btorwit=", "presat",
"dump-vcd=", "dump-vlogtb=", "vlogtb-top=", "dump-smtc=", "dump-all", "noinfo", "append=",
- "smtc-init", "smtc-top=", "noinit"])
+ "smtc-init", "smtc-top=", "noinit", "binary"])
except:
usage()
@@ -229,6 +232,8 @@ for o, a in opts:
covermode = True
elif o == "-m":
topmod = a
+ elif o == "--binary":
+ binarymode = True
elif so.handle(o, a):
pass
else:
@@ -1089,9 +1094,15 @@ def print_anyconsts_worker(mod, state, path):
for fun, info in smt.modinfo[mod].anyconsts.items():
if info[1] is None:
- print_msg("Value for anyconst in %s (%s): %d" % (path, info[0], smt.bv2int(smt.get("(|%s| %s)" % (fun, state)))))
+ if not binarymode:
+ print_msg("Value for anyconst in %s (%s): %d" % (path, info[0], smt.bv2int(smt.get("(|%s| %s)" % (fun, state)))))
+ else:
+ print_msg("Value for anyconst in %s (%s): %s" % (path, info[0], smt.bv2bin(smt.get("(|%s| %s)" % (fun, state)))))
else:
- print_msg("Value for anyconst %s.%s (%s): %d" % (path, info[1], info[0], smt.bv2int(smt.get("(|%s| %s)" % (fun, state)))))
+ if not binarymode:
+ print_msg("Value for anyconst %s.%s (%s): %d" % (path, info[1], info[0], smt.bv2int(smt.get("(|%s| %s)" % (fun, state)))))
+ else:
+ print_msg("Value for anyconst %s.%s (%s): %s" % (path, info[1], info[0], smt.bv2bin(smt.get("(|%s| %s)" % (fun, state)))))
def print_anyconsts(state):
diff --git a/backends/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc
index 5467e250b..11b2ae10f 100644
--- a/backends/verilog/verilog_backend.cc
+++ b/backends/verilog/verilog_backend.cc
@@ -1984,7 +1984,7 @@ struct VerilogBackend : public Backend {
extra_args(f, filename, args, argidx);
if (extmem)
{
- if (filename.empty())
+ if (filename == "<stdout>")
log_cmd_error("Option -extmem must be used with a filename.\n");
extmem_prefix = filename.substr(0, filename.rfind('.'));
}
generated by cgit v1.2.3 (git 2.25.1) at 2025-06-03 04:45:50 +0000