aboutsummaryrefslogtreecommitdiffstats
path: root/backends
diff options
context:
space:
mode:
Diffstat (limited to 'backends')
-rw-r--r--backends/blif/blif.cc235
-rw-r--r--backends/btor/README6
-rw-r--r--backends/btor/btor.cc254
-rw-r--r--backends/btor/btor.ys18
-rwxr-xr-xbackends/btor/verilog2btor.sh18
-rw-r--r--backends/edif/edif.cc59
-rw-r--r--backends/ilang/ilang_backend.cc8
-rw-r--r--backends/ilang/ilang_backend.h4
-rw-r--r--backends/intersynth/intersynth.cc10
-rw-r--r--backends/json/Makefile.inc3
-rw-r--r--backends/json/json.cc538
-rw-r--r--backends/smt2/Makefile.inc13
-rw-r--r--backends/smt2/example.v11
-rw-r--r--backends/smt2/example.ys3
-rw-r--r--backends/smt2/smt2.cc465
-rw-r--r--backends/smt2/smtbmc.py225
-rw-r--r--backends/smt2/smtio.py325
-rw-r--r--backends/smv/Makefile.inc3
-rw-r--r--backends/smv/smv.cc784
-rw-r--r--backends/smv/test_cells.sh33
-rw-r--r--backends/spice/spice.cc73
-rw-r--r--backends/verilog/verilog_backend.cc353
22 files changed, 3088 insertions, 353 deletions
diff --git a/backends/blif/blif.cc b/backends/blif/blif.cc
index 2734ca321..93953049a 100644
--- a/backends/blif/blif.cc
+++ b/backends/blif/blif.cc
@@ -2,11 +2,11 @@
* 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
@@ -37,14 +37,18 @@ struct BlifDumperConfig
bool conn_mode;
bool impltf_mode;
bool gates_mode;
+ bool cname_mode;
bool param_mode;
+ bool attr_mode;
bool blackbox_mode;
+ bool noalias_mode;
std::string buf_type, buf_in, buf_out;
std::map<RTLIL::IdString, std::pair<RTLIL::IdString, RTLIL::IdString>> unbuf_types;
std::string true_type, true_out, false_type, false_out, undef_type, undef_out;
- BlifDumperConfig() : icells_mode(false), conn_mode(false), impltf_mode(false), gates_mode(false), param_mode(false), blackbox_mode(false) { }
+ BlifDumperConfig() : icells_mode(false), conn_mode(false), impltf_mode(false), gates_mode(false),
+ cname_mode(false), param_mode(false), attr_mode(false), blackbox_mode(false), noalias_mode(false) { }
};
struct BlifDumper
@@ -55,12 +59,35 @@ struct BlifDumper
BlifDumperConfig *config;
CellTypes ct;
+ SigMap sigmap;
+ dict<SigBit, int> init_bits;
+
BlifDumper(std::ostream &f, RTLIL::Module *module, RTLIL::Design *design, BlifDumperConfig *config) :
- f(f), module(module), design(design), config(config), ct(design)
+ f(f), module(module), design(design), config(config), ct(design), sigmap(module)
{
+ for (Wire *wire : module->wires())
+ if (wire->attributes.count("\\init")) {
+ SigSpec initsig = sigmap(wire);
+ Const initval = wire->attributes.at("\\init");
+ for (int i = 0; i < GetSize(initsig) && i < GetSize(initval); i++)
+ switch (initval[i]) {
+ case State::S0:
+ init_bits[initsig[i]] = 0;
+ break;
+ case State::S1:
+ init_bits[initsig[i]] = 1;
+ break;
+ case State::Sx:
+ init_bits[initsig[i]] = 2;
+ break;
+ default:
+ break;
+ }
+ }
}
- std::vector<std::string> cstr_buf;
+ vector<shared_str> cstr_buf;
+ pool<SigBit> cstr_bits_seen;
const char *cstr(RTLIL::IdString id)
{
@@ -74,6 +101,8 @@ struct BlifDumper
const char *cstr(RTLIL::SigBit sig)
{
+ cstr_bits_seen.insert(sig);
+
if (sig.wire == NULL) {
if (sig == RTLIL::State::S0) return config->false_type == "-" ? config->false_out.c_str() : "$false";
if (sig == RTLIL::State::S1) return config->true_type == "-" ? config->true_out.c_str() : "$true";
@@ -92,6 +121,19 @@ struct BlifDumper
return cstr_buf.back().c_str();
}
+ const char *cstr_init(RTLIL::SigBit sig)
+ {
+ sigmap.apply(sig);
+
+ if (init_bits.count(sig) == 0)
+ return "";
+
+ string str = stringf(" %d", init_bits.at(sig));
+
+ cstr_buf.push_back(str);
+ return cstr_buf.back().c_str();
+ }
+
const char *subckt_or_gate(std::string cell_type)
{
if (!config->gates_mode)
@@ -103,6 +145,26 @@ struct BlifDumper
return "subckt";
}
+ void dump_params(const char *command, dict<IdString, Const> &params)
+ {
+ for (auto &param : params) {
+ f << stringf("%s %s ", command, RTLIL::id2cstr(param.first));
+ if (param.second.flags & RTLIL::CONST_FLAG_STRING) {
+ std::string str = param.second.decode_string();
+ f << stringf("\"");
+ for (char ch : str)
+ if (ch == '"' || ch == '\\')
+ f << stringf("\\%c", ch);
+ else if (ch < 32 || ch >= 127)
+ f << stringf("\\%03o", ch);
+ else
+ f << stringf("%c", ch);
+ f << stringf("\"\n");
+ } else
+ f << stringf("%s\n", param.second.as_string().c_str());
+ }
+ }
+
void dump()
{
f << stringf("\n");
@@ -202,6 +264,50 @@ struct BlifDumper
continue;
}
+ if (!config->icells_mode && cell->type == "$_NAND_") {
+ f << stringf(".names %s %s %s\n0- 1\n-0 1\n",
+ cstr(cell->getPort("\\A")), cstr(cell->getPort("\\B")), cstr(cell->getPort("\\Y")));
+ continue;
+ }
+
+ if (!config->icells_mode && cell->type == "$_NOR_") {
+ f << stringf(".names %s %s %s\n00 1\n",
+ cstr(cell->getPort("\\A")), cstr(cell->getPort("\\B")), cstr(cell->getPort("\\Y")));
+ continue;
+ }
+
+ if (!config->icells_mode && cell->type == "$_XNOR_") {
+ f << stringf(".names %s %s %s\n11 1\n00 1\n",
+ cstr(cell->getPort("\\A")), cstr(cell->getPort("\\B")), cstr(cell->getPort("\\Y")));
+ continue;
+ }
+
+ if (!config->icells_mode && cell->type == "$_AOI3_") {
+ f << stringf(".names %s %s %s %s\n-00 1\n0-0 1\n",
+ cstr(cell->getPort("\\A")), cstr(cell->getPort("\\B")), cstr(cell->getPort("\\C")), cstr(cell->getPort("\\Y")));
+ continue;
+ }
+
+ if (!config->icells_mode && cell->type == "$_OAI3_") {
+ f << stringf(".names %s %s %s %s\n00- 1\n--0 1\n",
+ cstr(cell->getPort("\\A")), cstr(cell->getPort("\\B")), cstr(cell->getPort("\\C")), cstr(cell->getPort("\\Y")));
+ continue;
+ }
+
+ if (!config->icells_mode && cell->type == "$_AOI4_") {
+ f << stringf(".names %s %s %s %s %s\n-0-0 1\n-00- 1\n0--0 1\n0-0- 1\n",
+ cstr(cell->getPort("\\A")), cstr(cell->getPort("\\B")),
+ cstr(cell->getPort("\\C")), cstr(cell->getPort("\\D")), cstr(cell->getPort("\\Y")));
+ continue;
+ }
+
+ if (!config->icells_mode && cell->type == "$_OAI4_") {
+ f << stringf(".names %s %s %s %s %s\n00-- 1\n--00 1\n",
+ cstr(cell->getPort("\\A")), cstr(cell->getPort("\\B")),
+ cstr(cell->getPort("\\C")), cstr(cell->getPort("\\D")), cstr(cell->getPort("\\Y")));
+ continue;
+ }
+
if (!config->icells_mode && cell->type == "$_MUX_") {
f << stringf(".names %s %s %s %s\n1-0 1\n-11 1\n",
cstr(cell->getPort("\\A")), cstr(cell->getPort("\\B")),
@@ -210,14 +316,26 @@ struct BlifDumper
}
if (!config->icells_mode && cell->type == "$_DFF_N_") {
- f << stringf(".latch %s %s fe %s\n",
- cstr(cell->getPort("\\D")), cstr(cell->getPort("\\Q")), cstr(cell->getPort("\\C")));
+ f << stringf(".latch %s %s fe %s%s\n", cstr(cell->getPort("\\D")), cstr(cell->getPort("\\Q")),
+ cstr(cell->getPort("\\C")), cstr_init(cell->getPort("\\Q")));
continue;
}
if (!config->icells_mode && cell->type == "$_DFF_P_") {
- f << stringf(".latch %s %s re %s\n",
- cstr(cell->getPort("\\D")), cstr(cell->getPort("\\Q")), cstr(cell->getPort("\\C")));
+ f << stringf(".latch %s %s re %s%s\n", cstr(cell->getPort("\\D")), cstr(cell->getPort("\\Q")),
+ cstr(cell->getPort("\\C")), cstr_init(cell->getPort("\\Q")));
+ continue;
+ }
+
+ if (!config->icells_mode && cell->type == "$_DLATCH_N_") {
+ f << stringf(".latch %s %s al %s%s\n", cstr(cell->getPort("\\D")), cstr(cell->getPort("\\Q")),
+ cstr(cell->getPort("\\E")), cstr_init(cell->getPort("\\Q")));
+ continue;
+ }
+
+ if (!config->icells_mode && cell->type == "$_DLATCH_P_") {
+ f << stringf(".latch %s %s ah %s%s\n", cstr(cell->getPort("\\D")), cstr(cell->getPort("\\Q")),
+ cstr(cell->getPort("\\E")), cstr_init(cell->getPort("\\Q")));
continue;
}
@@ -226,9 +344,8 @@ struct BlifDumper
auto &inputs = cell->getPort("\\A");
auto width = cell->parameters.at("\\WIDTH").as_int();
log_assert(inputs.size() == width);
- for (int i = width-1; i >= 0; i--) {
+ for (int i = width-1; i >= 0; i--)
f << stringf(" %s", cstr(inputs.extract(i, 1)));
- }
auto &output = cell->getPort("\\Y");
log_assert(output.size() == 1);
f << stringf(" %s", cstr(output));
@@ -255,6 +372,34 @@ struct BlifDumper
continue;
}
+ if (!config->icells_mode && cell->type == "$sop") {
+ f << stringf(".names");
+ auto &inputs = cell->getPort("\\A");
+ auto width = cell->parameters.at("\\WIDTH").as_int();
+ auto depth = cell->parameters.at("\\DEPTH").as_int();
+ vector<State> table = cell->parameters.at("\\TABLE").bits;
+ while (GetSize(table) < 2*width*depth)
+ table.push_back(State::S0);
+ log_assert(inputs.size() == width);
+ for (int i = 0; i < width; i++)
+ f << stringf(" %s", cstr(inputs.extract(i, 1)));
+ auto &output = cell->getPort("\\Y");
+ log_assert(output.size() == 1);
+ f << stringf(" %s", cstr(output));
+ f << stringf("\n");
+ for (int i = 0; i < depth; i++) {
+ for (int j = 0; j < width; j++) {
+ bool pat0 = table.at(2*width*i + 2*j + 0) == State::S1;
+ bool pat1 = table.at(2*width*i + 2*j + 1) == State::S1;
+ if (pat0 && !pat1) f << "0";
+ else if (!pat0 && pat1) f << "1";
+ else f << "-";
+ }
+ f << " 1\n";
+ }
+ continue;
+ }
+
f << stringf(".%s %s", subckt_or_gate(cell->type.str()), cstr(cell->type));
for (auto &conn : cell->connections())
for (int i = 0; i < conn.second.size(); i++) {
@@ -266,35 +411,31 @@ struct BlifDumper
}
f << stringf("\n");
+ if (config->cname_mode)
+ f << stringf(".cname %s\n", cstr(cell->name));
+ if (config->attr_mode)
+ dump_params(".attr", cell->attributes);
if (config->param_mode)
- for (auto &param : cell->parameters) {
- f << stringf(".param %s ", RTLIL::id2cstr(param.first));
- if (param.second.flags & RTLIL::CONST_FLAG_STRING) {
- std::string str = param.second.decode_string();
- f << stringf("\"");
- for (char ch : str)
- if (ch == '"' || ch == '\\')
- f << stringf("\\%c", ch);
- else if (ch < 32 || ch >= 127)
- f << stringf("\\%03o", ch);
- else
- f << stringf("%c", ch);
- f << stringf("\"\n");
- } else
- f << stringf("%s\n", param.second.as_string().c_str());
- }
+ dump_params(".param", cell->parameters);
}
for (auto &conn : module->connections())
for (int i = 0; i < conn.first.size(); i++)
+ {
+ SigBit lhs_bit = conn.first[i];
+ SigBit rhs_bit = conn.second[i];
+
+ if (config->noalias_mode && cstr_bits_seen.count(lhs_bit) == 0)
+ continue;
+
if (config->conn_mode)
- f << stringf(".conn %s %s\n", cstr(conn.second.extract(i, 1)), cstr(conn.first.extract(i, 1)));
+ f << stringf(".conn %s %s\n", cstr(rhs_bit), cstr(lhs_bit));
else if (!config->buf_type.empty())
- f << stringf(".%s %s %s=%s %s=%s\n", subckt_or_gate(config->buf_type), config->buf_type.c_str(), config->buf_in.c_str(), cstr(conn.second.extract(i, 1)),
- config->buf_out.c_str(), cstr(conn.first.extract(i, 1)));
+ f << stringf(".%s %s %s=%s %s=%s\n", subckt_or_gate(config->buf_type), config->buf_type.c_str(),
+ config->buf_in.c_str(), cstr(rhs_bit), config->buf_out.c_str(), cstr(lhs_bit));
else
- f << stringf(".names %s %s\n1 1\n", cstr(conn.second.extract(i, 1)), cstr(conn.first.extract(i, 1)));
-
+ f << stringf(".names %s %s\n1 1\n", cstr(rhs_bit), cstr(lhs_bit));
+ }
f << stringf(".end\n");
}
@@ -334,6 +475,11 @@ struct BlifBackend : public Backend {
log(" the wire name to be used for the constant signal and no cell driving\n");
log(" that wire is generated.\n");
log("\n");
+ log(" -noalias\n");
+ log(" if a net name is aliasing another net name, then by default a net\n");
+ log(" without fanout is created that is driven by the other net. This option\n");
+ log(" suppresses the generation of this nets without fanout.\n");
+ log("\n");
log("The following options can be useful when the generated file is not going to be\n");
log("read by a BLIF parser but a custom tool. It is recommended to not name the output\n");
log("file *.blif when any of this options is used.\n");
@@ -350,8 +496,14 @@ struct BlifBackend : public Backend {
log(" do not generate buffers for connected wires. instead use the\n");
log(" non-standard .conn statement.\n");
log("\n");
+ log(" -attr\n");
+ log(" use the non-standard .attr statement to write cell attributes\n");
+ log("\n");
log(" -param\n");
- log(" use the non-standard .param statement to write module parameters\n");
+ log(" use the non-standard .param statement to write cell parameters\n");
+ log("\n");
+ log(" -cname\n");
+ log(" use the non-standard .cname statement to write cell names\n");
log("\n");
log(" -blackbox\n");
log(" write blackbox cells with .blackbox statement.\n");
@@ -368,7 +520,7 @@ struct BlifBackend : public Backend {
std::string false_type, false_out;
BlifDumperConfig config;
- log_header("Executing BLIF backend.\n");
+ log_header(design, "Executing BLIF backend.\n");
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++)
@@ -417,10 +569,18 @@ struct BlifBackend : public Backend {
config.conn_mode = true;
continue;
}
+ if (args[argidx] == "-cname") {
+ config.cname_mode = true;
+ continue;
+ }
if (args[argidx] == "-param") {
config.param_mode = true;
continue;
}
+ if (args[argidx] == "-attr") {
+ config.attr_mode = true;
+ continue;
+ }
if (args[argidx] == "-blackbox") {
config.blackbox_mode = true;
continue;
@@ -429,6 +589,10 @@ struct BlifBackend : public Backend {
config.impltf_mode = true;
continue;
}
+ if (args[argidx] == "-noalias") {
+ config.noalias_mode = true;
+ continue;
+ }
break;
}
extra_args(f, filename, args, argidx);
@@ -442,6 +606,7 @@ struct BlifBackend : public Backend {
std::vector<RTLIL::Module*> mod_list;
+ design->sort();
for (auto module_it : design->modules_)
{
RTLIL::Module *module = module_it.second;
@@ -451,7 +616,7 @@ struct BlifBackend : public Backend {
if (module->processes.size() != 0)
log_error("Found unmapped processes in module %s: unmapped processes are not supported in BLIF backend!\n", RTLIL::id2cstr(module->name));
if (module->memories.size() != 0)
- log_error("Found munmapped emories in module %s: unmapped memories are not supported in BLIF backend!\n", RTLIL::id2cstr(module->name));
+ log_error("Found unmapped memories in module %s: unmapped memories are not supported in BLIF backend!\n", RTLIL::id2cstr(module->name));
if (module->name == RTLIL::escape_id(top_module_name)) {
BlifDumper::dump(*f, module, design, config);
diff --git a/backends/btor/README b/backends/btor/README
index 26cb377c6..efcf0d8f5 100644
--- a/backends/btor/README
+++ b/backends/btor/README
@@ -3,10 +3,10 @@ This is the Yosys BTOR backend.
It is developed by Ahmed Irfan <irfan@fbk.eu> - Fondazione Bruno Kessler, Trento, Italy
Master git repository for the BTOR backend:
-https://github.com/ahmedirfan1983/yosys/tree/btor
+https://github.com/ahmedirfan1983/yosys
-[[CITE]] BTOR: Bit-Precise Modelling of Word-Level Problems for Model Checking
+[[CITE]] BTOR: Bit-Precise Modelling of Word-Level Problems for Model Checking
Johannes Kepler University, Linz, Austria
http://fmv.jku.at/papers/BrummayerBiereLonsing-BPR08.pdf
@@ -19,5 +19,5 @@ Todos:
- async resets
- etc..
-- Add support for $pmux and $lut cells
+- Add support for $lut cells
diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index c8fbf8d67..bbe90e85f 100644
--- a/backends/btor/btor.cc
+++ b/backends/btor/btor.cc
@@ -3,11 +3,11 @@
*
* Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
* Copyright (C) 2014 Ahmed Irfan <irfan@fbk.eu>
- *
+ *
* 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
@@ -18,7 +18,7 @@
*
*/
-// [[CITE]] BTOR: Bit-Precise Modelling of Word-Level Problems for Model Checking
+// [[CITE]] BTOR: Bit-Precise Modelling of Word-Level Problems for Model Checking
// Johannes Kepler University, Linz, Austria
// http://fmv.jku.at/papers/BrummayerBiereLonsing-BPR08.pdf
@@ -70,17 +70,17 @@ struct BtorDumper
CellTypes ct;
SigMap sigmap;
- std::map<RTLIL::IdString, std::set<WireInfo,WireInfoOrder>> inter_wire_map;//<wire, dependency list> for maping the intermediate wires that are output of some cell
+ std::map<RTLIL::IdString, std::set<WireInfo,WireInfoOrder>> inter_wire_map;//<wire, dependency list> for mapping the intermediate wires that are output of some cell
std::map<RTLIL::IdString, int> line_ref;//mapping of ids to line_num of the btor file
std::map<RTLIL::SigSpec, int> sig_ref;//mapping of sigspec to the line_num of the btor file
int line_num;//last line number of btor file
std::string str;//temp string for writing file
- std::map<RTLIL::IdString, bool> basic_wires;//input wires and registers
+ std::map<RTLIL::IdString, bool> basic_wires;//input wires and registers
RTLIL::IdString curr_cell; //current cell being dumped
std::map<std::string, std::string> cell_type_translation, s_cell_type_translation; //RTLIL to BTOR translation
- std::set<int> mem_next; //if memory (line_number) already has next
- BtorDumper(std::ostream &f, RTLIL::Module *module, RTLIL::Design *design, BtorDumperConfig *config) :
- f(f), module(module), design(design), config(config), ct(design), sigmap(module)
+ std::map<int, std::set<std::pair<int,int>>> mem_next; // memory (line_number)'s set of condition and write
+ BtorDumper(std::ostream &f, RTLIL::Module *module, RTLIL::Design *design, BtorDumperConfig *config) :
+ f(f), module(module), design(design), config(config), ct(design), sigmap(module)
{
line_num=0;
str.clear();
@@ -143,7 +143,7 @@ struct BtorDumper
//concat
cell_type_translation["$concat"] = "concat";
- //signed cell type translation
+ //signed cell type translation
//binary
s_cell_type_translation["$modx"] = "srem";
s_cell_type_translation["$mody"] = "smod";
@@ -152,10 +152,10 @@ struct BtorDumper
s_cell_type_translation["$le"] = "slte";
s_cell_type_translation["$gt"] = "sgt";
s_cell_type_translation["$ge"] = "sgte";
-
+
}
-
- std::vector<std::string> cstr_buf;
+
+ vector<shared_str> cstr_buf;
const char *cstr(const RTLIL::IdString id)
{
@@ -166,17 +166,17 @@ struct BtorDumper
cstr_buf.push_back(str);
return cstr_buf.back().c_str();
}
-
+
int dump_wire(RTLIL::Wire* wire)
{
if(basic_wires[wire->name])
- {
+ {
log("writing wire %s\n", cstr(wire->name));
auto it = line_ref.find(wire->name);
if(it==std::end(line_ref))
{
++line_num;
- line_ref[wire->name]=line_num;
+ line_ref[wire->name]=line_num;
str = stringf("%d var %d %s", line_num, wire->width, cstr(wire->name));
f << stringf("%s\n", str.c_str());
return line_num;
@@ -200,7 +200,7 @@ struct BtorDumper
log(" -- found cell %s\n", cstr(cell_id));
RTLIL::Cell* cell = module->cells_.at(cell_id);
const RTLIL::SigSpec* cell_output = get_cell_output(cell);
- int cell_line = dump_cell(cell);
+ int cell_line = dump_cell(cell);
if(dep_set.size()==1 && wire->width == cell_output->size())
{
@@ -235,7 +235,7 @@ struct BtorDumper
}
if(dep_set.size()==0)
{
- log(" - checking sigmap\n");
+ log(" - checking sigmap\n");
RTLIL::SigSpec s = RTLIL::SigSpec(wire);
wire_line = dump_sigspec(&s, s.size());
line_ref[wire->name]=wire_line;
@@ -243,16 +243,16 @@ struct BtorDumper
line_ref[wire->name]=wire_line;
return wire_line;
}
- else
+ else
{
- log(" -- already processed wire\n");
+ log(" -- already processed wire\n");
return it->second;
}
}
log_abort();
return -1;
}
-
+
int dump_memory(const RTLIL::Memory* memory)
{
log("writing memory %s\n", cstr(memory->name));
@@ -260,15 +260,54 @@ struct BtorDumper
if(it==std::end(line_ref))
{
++line_num;
- int address_bits = ceil(log(memory->size)/log(2));
+ int address_bits = ceil_log2(memory->size);
str = stringf("%d array %d %d", line_num, memory->width, address_bits);
- line_ref[memory->name]=line_num;
+ line_ref[memory->name]=line_num;
f << stringf("%s\n", str.c_str());
return line_num;
}
else return it->second;
}
+ int dump_memory_next(const RTLIL::Memory* memory)
+ {
+ auto mem_it = line_ref.find(memory->name);
+ int address_bits = ceil_log2(memory->size);
+ if(mem_it==std::end(line_ref))
+ {
+ log("can not write next of a memory that is not dumped yet\n");
+ log_abort();
+ }
+ else
+ {
+ auto acond_list_it = mem_next.find(mem_it->second);
+ if(acond_list_it!=std::end(mem_next))
+ {
+ std::set<std::pair<int,int>>& cond_list = acond_list_it->second;
+ if(cond_list.empty())
+ {
+ return 0;
+ }
+ auto it=cond_list.begin();
+ ++line_num;
+ str = stringf("%d acond %d %d %d %d %d", line_num, memory->width, address_bits, it->first, it->second, mem_it->second);
+ f << stringf("%s\n", str.c_str());
+ ++it;
+ for(; it!=cond_list.end(); ++it)
+ {
+ ++line_num;
+ str = stringf("%d acond %d %d %d %d %d", line_num, memory->width, address_bits, it->first, it->second, line_num-1);
+ f << stringf("%s\n", str.c_str());
+ }
+ ++line_num;
+ str = stringf("%d anext %d %d %d %d", line_num, memory->width, address_bits, mem_it->second, line_num-1);
+ f << stringf("%s\n", str.c_str());
+ return 1;
+ }
+ return 0;
+ }
+ }
+
int dump_const(const RTLIL::Const* data, int width, int offset)
{
log("writing const \n");
@@ -287,11 +326,11 @@ struct BtorDumper
return line_num;
}
else
- log("writing const error\n");
+ log("writing const error\n");
log_abort();
return -1;
}
-
+
int dump_sigchunk(const RTLIL::SigChunk* chunk)
{
log("writing sigchunk\n");
@@ -299,21 +338,21 @@ struct BtorDumper
if(chunk->wire == NULL)
{
RTLIL::Const data_const(chunk->data);
- l=dump_const(&data_const, chunk->width, chunk->offset);
+ l=dump_const(&data_const, chunk->width, chunk->offset);
}
else
{
if (chunk->width == chunk->wire->width && chunk->offset == 0)
l = dump_wire(chunk->wire);
- else
+ else
{
int wire_line_num = dump_wire(chunk->wire);
log_assert(wire_line_num>0);
++line_num;
- str = stringf("%d slice %d %d %d %d;2", line_num, chunk->width, wire_line_num,
+ str = stringf("%d slice %d %d %d %d;2", line_num, chunk->width, wire_line_num,
chunk->width + chunk->offset - 1, chunk->offset);
f << stringf("%s\n", str.c_str());
- l = line_num;
+ l = line_num;
}
}
return l;
@@ -330,8 +369,8 @@ struct BtorDumper
if (s.is_chunk())
{
l = dump_sigchunk(&s.chunks().front());
- }
- else
+ }
+ else
{
int l1, l2, w1, w2;
l1 = dump_sigchunk(&s.chunks().front());
@@ -356,7 +395,7 @@ struct BtorDumper
{
l = it->second;
}
-
+
if (expected_width != s.size())
{
log(" - changing width of sigspec\n");
@@ -383,7 +422,7 @@ struct BtorDumper
log_assert(l>0);
return l;
}
-
+
int dump_cell(const RTLIL::Cell* cell)
{
auto it = line_ref.find(cell->name);
@@ -427,10 +466,10 @@ struct BtorDumper
int w = cell->parameters.at(RTLIL::IdString("\\A_WIDTH")).as_int();
int output_width = cell->parameters.at(RTLIL::IdString("\\Y_WIDTH")).as_int();
w = w>output_width ? w:output_width; //padding of w
- int l = dump_sigspec(&cell->getPort(RTLIL::IdString("\\A")), w);
+ int l = dump_sigspec(&cell->getPort(RTLIL::IdString("\\A")), w);
int cell_line = l;
if(cell->type != "$pos")
- {
+ {
cell_line = ++line_num;
bool reduced = (cell->type == "$not" || cell->type == "$neg") ? false : true;
str = stringf ("%d %s %d %d", cell_line, cell_type_translation.at(cell->type.str()).c_str(), reduced?output_width:w, l);
@@ -442,7 +481,7 @@ struct BtorDumper
str = stringf ("%d slice %d %d %d %d;4", line_num, output_width, cell_line, output_width-1, 0);
f << stringf("%s\n", str.c_str());
cell_line = line_num;
- }
+ }
line_ref[cell->name]=cell_line;
}
else if(cell->type == "$reduce_xnor" || cell->type == "$logic_not")//no direct translation in btor
@@ -463,7 +502,7 @@ struct BtorDumper
++line_num;
str = stringf ("%d %s %d %d", line_num, cell_type_translation.at("$reduce_xor").c_str(), output_width, l);
f << stringf("%s\n", str.c_str());
- }
+ }
++line_num;
str = stringf ("%d %s %d %d", line_num, cell_type_translation.at("$not").c_str(), output_width, l);
f << stringf("%s\n", str.c_str());
@@ -471,7 +510,7 @@ struct BtorDumper
}
//binary cells
else if(cell->type == "$and" || cell->type == "$or" || cell->type == "$xor" || cell->type == "$xnor" ||
- cell->type == "$lt" || cell->type == "$le" || cell->type == "$eq" || cell->type == "$ne" ||
+ cell->type == "$lt" || cell->type == "$le" || cell->type == "$eq" || cell->type == "$ne" ||
cell->type == "$eqx" || cell->type == "$nex" || cell->type == "$ge" || cell->type == "$gt" )
{
log("writing binary cell - %s\n", cstr(cell->type));
@@ -481,16 +520,16 @@ struct BtorDumper
bool l1_signed = cell->parameters.at(RTLIL::IdString("\\A_SIGNED")).as_bool();
bool l2_signed YS_ATTRIBUTE(unused) = cell->parameters.at(RTLIL::IdString("\\B_SIGNED")).as_bool();
int l1_width = cell->parameters.at(RTLIL::IdString("\\A_WIDTH")).as_int();
- int l2_width = cell->parameters.at(RTLIL::IdString("\\B_WIDTH")).as_int();
-
+ int l2_width = cell->parameters.at(RTLIL::IdString("\\B_WIDTH")).as_int();
+
log_assert(l1_signed == l2_signed);
- l1_width = l1_width > output_width ? l1_width : output_width;
+ l1_width = l1_width > output_width ? l1_width : output_width;
l1_width = l1_width > l2_width ? l1_width : l2_width;
l2_width = l2_width > l1_width ? l2_width : l1_width;
int l1 = dump_sigspec(&cell->getPort(RTLIL::IdString("\\A")), l1_width);
int l2 = dump_sigspec(&cell->getPort(RTLIL::IdString("\\B")), l2_width);
-
+
++line_num;
std::string op = cell_type_translation.at(cell->type.str());
if(cell->type == "$lt" || cell->type == "$le" ||
@@ -500,13 +539,13 @@ struct BtorDumper
if(l1_signed)
op = s_cell_type_translation.at(cell->type.str());
}
-
+
str = stringf ("%d %s %d %d %d", line_num, op.c_str(), output_width, l1, l2);
f << stringf("%s\n", str.c_str());
line_ref[cell->name]=line_num;
}
- else if(cell->type == "$add" || cell->type == "$sub" || cell->type == "$mul" || cell->type == "$div" ||
+ else if(cell->type == "$add" || cell->type == "$sub" || cell->type == "$mul" || cell->type == "$div" ||
cell->type == "$mod" )
{
//TODO: division by zero case
@@ -515,16 +554,16 @@ struct BtorDumper
bool l1_signed = cell->parameters.at(RTLIL::IdString("\\A_SIGNED")).as_bool();
bool l2_signed = cell->parameters.at(RTLIL::IdString("\\B_SIGNED")).as_bool();
int l1_width = cell->parameters.at(RTLIL::IdString("\\A_WIDTH")).as_int();
- int l2_width = cell->parameters.at(RTLIL::IdString("\\B_WIDTH")).as_int();
-
+ int l2_width = cell->parameters.at(RTLIL::IdString("\\B_WIDTH")).as_int();
+
log_assert(l1_signed == l2_signed);
- l1_width = l1_width > output_width ? l1_width : output_width;
+ l1_width = l1_width > output_width ? l1_width : output_width;
l1_width = l1_width > l2_width ? l1_width : l2_width;
l2_width = l2_width > l1_width ? l2_width : l1_width;
int l1 = dump_sigspec(&cell->getPort(RTLIL::IdString("\\A")), l1_width);
int l2 = dump_sigspec(&cell->getPort(RTLIL::IdString("\\B")), l2_width);
-
+
++line_num;
std::string op = cell_type_translation.at(cell->type.str());
if(cell->type == "$div" && l1_signed)
@@ -554,18 +593,18 @@ struct BtorDumper
bool l1_signed = cell->parameters.at(RTLIL::IdString("\\A_SIGNED")).as_bool();
//bool l2_signed = cell->parameters.at(RTLIL::IdString("\\B_SIGNED")).as_bool();
int l1_width = cell->parameters.at(RTLIL::IdString("\\A_WIDTH")).as_int();
- l1_width = pow(2, ceil(log(l1_width)/log(2)));
- int l2_width = cell->parameters.at(RTLIL::IdString("\\B_WIDTH")).as_int();
- //log_assert(l2_width <= ceil(log(l1_width)/log(2)) );
+ l1_width = 1 << ceil_log2(l1_width);
+ int l2_width = cell->parameters.at(RTLIL::IdString("\\B_WIDTH")).as_int();
+ //log_assert(l2_width <= ceil_log2(l1_width)) );
int l1 = dump_sigspec(&cell->getPort(RTLIL::IdString("\\A")), l1_width);
- int l2 = dump_sigspec(&cell->getPort(RTLIL::IdString("\\B")), ceil(log(l1_width)/log(2)));
+ int l2 = dump_sigspec(&cell->getPort(RTLIL::IdString("\\B")), ceil_log2(l1_width));
int cell_output = ++line_num;
str = stringf ("%d %s %d %d %d", line_num, cell_type_translation.at(cell->type.str()).c_str(), l1_width, l1, l2);
f << stringf("%s\n", str.c_str());
- if(l2_width > ceil(log(l1_width)/log(2)))
+ if(l2_width > ceil_log2(l1_width))
{
- int extra_width = l2_width - ceil(log(l1_width)/log(2));
+ int extra_width = l2_width - ceil_log2(l1_width);
l2 = dump_sigspec(&cell->getPort(RTLIL::IdString("\\B")), l2_width);
++line_num;
str = stringf ("%d slice %d %d %d %d;6", line_num, extra_width, l2, l2_width-1, l2_width-extra_width);
@@ -592,7 +631,7 @@ struct BtorDumper
f << stringf("%s\n", str.c_str());
cell_output = line_num;
}
- line_ref[cell->name] = cell_output;
+ line_ref[cell->name] = cell_output;
}
else if(cell->type == "$logic_and" || cell->type == "$logic_or")//no direct translation in btor
{
@@ -602,7 +641,7 @@ struct BtorDumper
int l1 = dump_sigspec(&cell->getPort(RTLIL::IdString("\\A")), output_width);
int l2 = dump_sigspec(&cell->getPort(RTLIL::IdString("\\B")), output_width);
int l1_width = cell->parameters.at(RTLIL::IdString("\\A_WIDTH")).as_int();
- int l2_width = cell->parameters.at(RTLIL::IdString("\\B_WIDTH")).as_int();
+ int l2_width = cell->parameters.at(RTLIL::IdString("\\B_WIDTH")).as_int();
if(l1_width >1)
{
++line_num;
@@ -639,7 +678,7 @@ struct BtorDumper
int l2 = dump_sigspec(&cell->getPort(RTLIL::IdString("\\B")), output_width);
int s = dump_sigspec(&cell->getPort(RTLIL::IdString("\\S")), 1);
++line_num;
- str = stringf ("%d %s %d %d %d %d",
+ str = stringf ("%d %s %d %d %d %d",
line_num, cell_type_translation.at(cell->type.str()).c_str(), output_width, s, l2, l1);
//if s is 0 then l1, if s is 1 then l2 //according to the implementation of mux cell
f << stringf("%s\n", str.c_str());
@@ -654,7 +693,7 @@ struct BtorDumper
int cases = dump_sigspec(&cell->getPort(RTLIL::IdString("\\B")), output_width*select_width);
int select = dump_sigspec(&cell->getPort(RTLIL::IdString("\\S")), select_width);
int *c = new int[select_width];
-
+
for (int i=0; i<select_width; ++i)
{
++line_num;
@@ -662,15 +701,15 @@ struct BtorDumper
f << stringf("%s\n", str.c_str());
c[i] = line_num;
++line_num;
- str = stringf ("%d slice %d %d %d %d", line_num, output_width, cases, i*output_width+output_width-1,
+ str = stringf ("%d slice %d %d %d %d", line_num, output_width, cases, i*output_width+output_width-1,
i*output_width);
f << stringf("%s\n", str.c_str());
}
-
+
++line_num;
str = stringf ("%d cond %d %d %d %d", line_num, output_width, c[select_width-1], c[select_width-1]+1, default_case);
f << stringf("%s\n", str.c_str());
-
+
for (int i=select_width-2; i>=0; --i)
{
++line_num;
@@ -683,7 +722,7 @@ struct BtorDumper
//registers
else if(cell->type == "$dff" || cell->type == "$adff" || cell->type == "$dffsr")
{
- //TODO: remodelling fo adff cells
+ //TODO: remodelling of adff cells
log("writing cell - %s\n", cstr(cell->type));
int output_width = cell->parameters.at(RTLIL::IdString("\\WIDTH")).as_int();
log(" - width is %d\n", output_width);
@@ -702,7 +741,7 @@ struct BtorDumper
{
start_bit+=output_width;
slice = ++line_num;
- str = stringf ("%d slice %d %d %d %d;", line_num, output_width, value, start_bit-1,
+ str = stringf ("%d slice %d %d %d %d;", line_num, output_width, value, start_bit-1,
start_bit-output_width);
f << stringf("%s\n", str.c_str());
}
@@ -714,16 +753,16 @@ struct BtorDumper
output_width);
bool sync_reset_value_pol = cell->parameters.at(RTLIL::IdString("\\SET_POLARITY")).as_bool();
++line_num;
- str = stringf ("%d %s %d %s%d %s%d %d", line_num, cell_type_translation.at("$mux").c_str(),
- output_width, sync_reset_pol ? "":"-", sync_reset, sync_reset_value_pol? "":"-",
+ str = stringf ("%d %s %d %s%d %s%d %d", line_num, cell_type_translation.at("$mux").c_str(),
+ output_width, sync_reset_pol ? "":"-", sync_reset, sync_reset_value_pol? "":"-",
sync_reset_value, slice);
f << stringf("%s\n", str.c_str());
slice = line_num;
}
++line_num;
- str = stringf ("%d %s %d %s%d %d %d", line_num, cell_type_translation.at("$mux").c_str(),
+ str = stringf ("%d %s %d %s%d %d %d", line_num, cell_type_translation.at("$mux").c_str(),
output_width, polarity?"":"-", cond, slice, reg);
-
+
f << stringf("%s\n", str.c_str());
int next = line_num;
if(cell->type == "$adff")
@@ -733,12 +772,12 @@ struct BtorDumper
int async_reset_value = dump_const(&cell->parameters.at(RTLIL::IdString("\\ARST_VALUE")),
output_width, 0);
++line_num;
- str = stringf ("%d %s %d %s%d %d %d", line_num, cell_type_translation.at("$mux").c_str(),
+ str = stringf ("%d %s %d %s%d %d %d", line_num, cell_type_translation.at("$mux").c_str(),
output_width, async_reset_pol ? "":"-", async_reset, async_reset_value, next);
f << stringf("%s\n", str.c_str());
}
++line_num;
- str = stringf ("%d %s %d %d %d", line_num, cell_type_translation.at(cell->type.str()).c_str(),
+ str = stringf ("%d %s %d %d %d", line_num, cell_type_translation.at(cell->type.str()).c_str(),
output_width, reg, next);
f << stringf("%s\n", str.c_str());
}
@@ -756,7 +795,7 @@ struct BtorDumper
int address = dump_sigspec(&cell->getPort(RTLIL::IdString("\\ADDR")), address_width);
int data_width = cell->parameters.at(RTLIL::IdString("\\WIDTH")).as_int();
++line_num;
- str = stringf("%d read %d %d %d", line_num, data_width, mem, address);
+ str = stringf("%d read %d %d %d", line_num, data_width, mem, address);
f << stringf("%s\n", str.c_str());
line_ref[cell->name]=line_num;
}
@@ -775,43 +814,46 @@ struct BtorDumper
str = cell->parameters.at(RTLIL::IdString("\\MEMID")).decode_string();
int mem = dump_memory(module->memories.at(RTLIL::IdString(str.c_str())));
//check if the memory has already next
- auto it = mem_next.find(mem);
+ /*
+ auto it = mem_next.find(mem);
if(it != std::end(mem_next))
{
++line_num;
str = cell->parameters.at(RTLIL::IdString("\\MEMID")).decode_string();
RTLIL::Memory *memory = module->memories.at(RTLIL::IdString(str.c_str()));
- int address_bits = ceil(log(memory->size)/log(2));
+ int address_bits = ceil_log2(memory->size);
str = stringf("%d array %d %d", line_num, memory->width, address_bits);
f << stringf("%s\n", str.c_str());
++line_num;
- str = stringf("%d eq 1 %d %d", line_num, mem, line_num - 1);
+ str = stringf("%d eq 1 %d %d; mem invar", line_num, mem, line_num - 1);
f << stringf("%s\n", str.c_str());
mem = line_num - 1;
- }
- ++line_num;
+ }
+ */
+ ++line_num;
if(polarity)
str = stringf("%d one 1", line_num);
else
str = stringf("%d zero 1", line_num);
f << stringf("%s\n", str.c_str());
++line_num;
- str = stringf("%d eq 1 %d %d", line_num, clk, line_num-1);
+ str = stringf("%d eq 1 %d %d", line_num, clk, line_num-1);
f << stringf("%s\n", str.c_str());
++line_num;
- str = stringf("%d and 1 %d %d", line_num, line_num-1, enable);
+ str = stringf("%d and 1 %d %d", line_num, line_num-1, enable);
f << stringf("%s\n", str.c_str());
++line_num;
- str = stringf("%d write %d %d %d %d %d", line_num, data_width, address_width, mem, address, data);
+ str = stringf("%d write %d %d %d %d %d", line_num, data_width, address_width, mem, address, data);
f << stringf("%s\n", str.c_str());
+ /*
++line_num;
- str = stringf("%d acond %d %d %d %d %d", line_num, data_width, address_width, line_num-2/*enable*/, line_num-1, mem);
- f << stringf("%s\n", str.c_str());
+ str = stringf("%d acond %d %d %d %d %d", line_num, data_width, address_width, line_num-2, line_num-1, mem);
+ f << stringf("%s\n", str.c_str());
++line_num;
- str = stringf("%d anext %d %d %d %d", line_num, data_width, address_width, mem, line_num-1);
- f << stringf("%s\n", str.c_str());
- mem_next.insert(mem);
- line_ref[cell->name]=line_num;
+ str = stringf("%d anext %d %d %d %d", line_num, data_width, address_width, mem, line_num-1);
+ f << stringf("%s\n", str.c_str());
+ */
+ mem_next[mem].insert(std::make_pair(line_num-1, line_num));
}
else if(cell->type == "$slice")
{
@@ -823,11 +865,11 @@ struct BtorDumper
const RTLIL::SigSpec* output YS_ATTRIBUTE(unused) = &cell->getPort(RTLIL::IdString("\\Y"));
int output_width = cell->parameters.at(RTLIL::IdString("\\Y_WIDTH")).as_int();
log_assert(output->size() == output_width);
- int offset = cell->parameters.at(RTLIL::IdString("\\OFFSET")).as_int();
+ int offset = cell->parameters.at(RTLIL::IdString("\\OFFSET")).as_int();
++line_num;
str = stringf("%d %s %d %d %d %d", line_num, cell_type_translation.at(cell->type.str()).c_str(), output_width, input_line, output_width+offset-1, offset);
- f << stringf("%s\n", str.c_str());
- line_ref[cell->name]=line_num;
+ f << stringf("%s\n", str.c_str());
+ line_ref[cell->name]=line_num;
}
else if(cell->type == "$concat")
{
@@ -841,10 +883,10 @@ struct BtorDumper
log_assert(input_b->size() == input_b_width);
int input_b_line = dump_sigspec(input_b, input_b_width);
++line_num;
- str = stringf("%d %s %d %d %d", line_num, cell_type_translation.at(cell->type.str()).c_str(), input_a_width+input_b_width,
- input_a_line, input_b_line);
- f << stringf("%s\n", str.c_str());
- line_ref[cell->name]=line_num;
+ str = stringf("%d %s %d %d %d", line_num, cell_type_translation.at(cell->type.str()).c_str(), input_a_width+input_b_width,
+ input_a_line, input_b_line);
+ f << stringf("%s\n", str.c_str());
+ line_ref[cell->name]=line_num;
}
curr_cell.clear();
return line_num;
@@ -870,7 +912,7 @@ struct BtorDumper
{
output_sig = &cell->getPort(RTLIL::IdString("\\Q"));
}
- else
+ else
{
output_sig = &cell->getPort(RTLIL::IdString("\\Y"));
}
@@ -888,7 +930,7 @@ struct BtorDumper
void dump()
{
f << stringf(";module %s\n", cstr(module->name));
-
+
log("creating intermediate wires map\n");
//creating map of intermediate wires as output of some cell
for (auto it = module->cells_.begin(); it != module->cells_.end(); ++it)
@@ -924,7 +966,7 @@ struct BtorDumper
basic_wires[wire_id] = true;
}
}
- else
+ else
{
for(unsigned i=0; i<output_sig->chunks().size(); ++i)
{
@@ -934,11 +976,11 @@ struct BtorDumper
}
}
}
-
+
log("writing input\n");
std::map<int, RTLIL::Wire*> inputs, outputs;
std::vector<RTLIL::Wire*> safety;
-
+
for (auto &wire_it : module->wires_) {
RTLIL::Wire *wire = wire_it.second;
if (wire->port_input)
@@ -956,7 +998,7 @@ struct BtorDumper
dump_wire(wire);
}
f << stringf("\n");
-
+
log("writing memories\n");
for(auto mem_it = module->memories.begin(); mem_it != module->memories.end(); ++mem_it)
{
@@ -972,14 +1014,20 @@ struct BtorDumper
log("writing cells\n");
for(auto cell_it = module->cells_.begin(); cell_it != module->cells_.end(); ++cell_it)
{
- dump_cell(cell_it->second);
+ dump_cell(cell_it->second);
}
-
+
+ log("writing memory next");
+ for(auto mem_it = module->memories.begin(); mem_it != module->memories.end(); ++mem_it)
+ {
+ dump_memory_next(mem_it->second);
+ }
+
for(auto it: safety)
dump_property(it);
f << stringf("\n");
-
+
log("writing outputs info\n");
f << stringf(";outputs\n");
for (auto &it : outputs) {
@@ -999,7 +1047,7 @@ struct BtorDumper
struct BtorBackend : public Backend {
BtorBackend() : Backend("btor", "write design to BTOR file") { }
-
+
virtual void help()
{
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
@@ -1017,11 +1065,11 @@ struct BtorBackend : public Backend {
std::string false_type, false_out;
BtorDumperConfig config;
- log_header("Executing BTOR backend.\n");
+ log_header(design, "Executing BTOR backend.\n");
size_t argidx=1;
extra_args(f, filename, args, argidx);
-
+
if (top_module_name.empty())
for (auto & mod_it:design->modules_)
if (mod_it.second->get_bool_attribute("\\top"))
@@ -1031,7 +1079,7 @@ struct BtorBackend : public Backend {
*f << stringf("; %s developed and maintained by Clifford Wolf <clifford@clifford.at>\n", yosys_version_str);
*f << stringf("; BTOR Backend developed by Ahmed Irfan <irfan@fbk.eu> - Fondazione Bruno Kessler, Trento, Italy\n");
*f << stringf(";;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;\n");
-
+
std::vector<RTLIL::Module*> mod_list;
for (auto module_it : design->modules_)
diff --git a/backends/btor/btor.ys b/backends/btor/btor.ys
deleted file mode 100644
index ec28245d3..000000000
--- a/backends/btor/btor.ys
+++ /dev/null
@@ -1,18 +0,0 @@
-proc;
-opt; opt_const -mux_undef; opt;
-rename -hide;;;
-#converting pmux to mux
-techmap -share_map pmux2mux.v;;
-#explicit type conversion
-splice; opt;
-#extracting memories;
-memory_dff -wr_only; memory_collect;;
-#flatten design
-flatten;;
-#converting asyn memory write to syn memory
-memory_unpack;
-#cell output to be a single wire
-splitnets -driver;
-setundef -zero -undriven;
-opt;;;
-
diff --git a/backends/btor/verilog2btor.sh b/backends/btor/verilog2btor.sh
index ab45b4901..dfd7f1a85 100755
--- a/backends/btor/verilog2btor.sh
+++ b/backends/btor/verilog2btor.sh
@@ -1,7 +1,7 @@
#!/bin/sh
#
-# Script to writing btor from verilog design
+# Script to write BTOR from Verilog design
#
if [ "$#" -ne 3 ]; then
@@ -17,19 +17,19 @@ FULL_PATH=$(readlink -f $1)
DIR=$(dirname $FULL_PATH)
./yosys -q -p "
-read_verilog -sv $1;
-hierarchy -top $3;
-hierarchy -libdir $DIR;
-hierarchy -check;
-proc;
-opt; opt_const -mux_undef; opt;
+read_verilog -sv $1;
+hierarchy -top $3;
+hierarchy -libdir $DIR;
+hierarchy -check;
+proc;
+opt; opt_expr -mux_undef; opt;
rename -hide;;;
-#techmap -share_map pmux2mux.v;;
+#techmap -map +/pmux2mux.v;;
splice; opt;
memory_dff -wr_only;
memory_collect;;
flatten;;
-memory_unpack;
+memory_unpack;
splitnets -driver;
setundef -zero -undriven;
opt;;;
diff --git a/backends/edif/edif.cc b/backends/edif/edif.cc
index b089be143..d16f18316 100644
--- a/backends/edif/edif.cc
+++ b/backends/edif/edif.cc
@@ -2,11 +2,11 @@
* 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
@@ -100,6 +100,11 @@ struct EdifBackend : public Backend {
log(" -top top_module\n");
log(" set the specified module as design top module\n");
log("\n");
+ log(" -nogndvcc\n");
+ log(" do not create \"GND\" and \"VCC\" cells. (this will produce an error\n");
+ log(" if the design contains constant nets. use \"hilomap\" to map to custom\n");
+ log(" constant drivers first)\n");
+ log("\n");
log("Unfortunately there are different \"flavors\" of the EDIF file format. This\n");
log("command generates EDIF files for the Xilinx place&route tools. It might be\n");
log("necessary to make small modifications to this command when a different tool\n");
@@ -108,10 +113,11 @@ struct EdifBackend : public Backend {
}
virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
{
- log_header("Executing EDIF backend.\n");
+ log_header(design, "Executing EDIF backend.\n");
std::string top_module_name;
std::map<RTLIL::IdString, std::map<RTLIL::IdString, int>> lib_cell_ports;
+ bool nogndvcc = false;
CellTypes ct(design);
EdifNames edif_names;
@@ -122,6 +128,10 @@ struct EdifBackend : public Backend {
top_module_name = args[++argidx];
continue;
}
+ if (args[argidx] == "-nogndvcc") {
+ nogndvcc = true;
+ continue;
+ }
break;
}
extra_args(f, filename, args, argidx);
@@ -143,7 +153,7 @@ struct EdifBackend : public Backend {
if (module->processes.size() != 0)
log_error("Found unmapped processes in module %s: unmapped processes are not supported in EDIF backend!\n", RTLIL::id2cstr(module->name));
if (module->memories.size() != 0)
- log_error("Found munmapped emories in module %s: unmapped memories are not supported in EDIF backend!\n", RTLIL::id2cstr(module->name));
+ log_error("Found unmapped memories in module %s: unmapped memories are not supported in EDIF backend!\n", RTLIL::id2cstr(module->name));
for (auto cell_it : module->cells_)
{
@@ -169,21 +179,24 @@ struct EdifBackend : public Backend {
*f << stringf(" (edifLevel 0)\n");
*f << stringf(" (technology (numberDefinition))\n");
- *f << stringf(" (cell GND\n");
- *f << stringf(" (cellType GENERIC)\n");
- *f << stringf(" (view VIEW_NETLIST\n");
- *f << stringf(" (viewType NETLIST)\n");
- *f << stringf(" (interface (port G (direction OUTPUT)))\n");
- *f << stringf(" )\n");
- *f << stringf(" )\n");
-
- *f << stringf(" (cell VCC\n");
- *f << stringf(" (cellType GENERIC)\n");
- *f << stringf(" (view VIEW_NETLIST\n");
- *f << stringf(" (viewType NETLIST)\n");
- *f << stringf(" (interface (port P (direction OUTPUT)))\n");
- *f << stringf(" )\n");
- *f << stringf(" )\n");
+ if (!nogndvcc)
+ {
+ *f << stringf(" (cell GND\n");
+ *f << stringf(" (cellType GENERIC)\n");
+ *f << stringf(" (view VIEW_NETLIST\n");
+ *f << stringf(" (viewType NETLIST)\n");
+ *f << stringf(" (interface (port G (direction OUTPUT)))\n");
+ *f << stringf(" )\n");
+ *f << stringf(" )\n");
+
+ *f << stringf(" (cell VCC\n");
+ *f << stringf(" (cellType GENERIC)\n");
+ *f << stringf(" (view VIEW_NETLIST\n");
+ *f << stringf(" (viewType NETLIST)\n");
+ *f << stringf(" (interface (port P (direction OUTPUT)))\n");
+ *f << stringf(" )\n");
+ *f << stringf(" )\n");
+ }
for (auto &cell_it : lib_cell_ports) {
*f << stringf(" (cell %s\n", EDIF_DEF(cell_it.first));
@@ -279,8 +292,10 @@ struct EdifBackend : public Backend {
}
*f << stringf(" )\n");
*f << stringf(" (contents\n");
- *f << stringf(" (instance GND (viewRef VIEW_NETLIST (cellRef GND (libraryRef LIB))))\n");
- *f << stringf(" (instance VCC (viewRef VIEW_NETLIST (cellRef VCC (libraryRef LIB))))\n");
+ if (!nogndvcc) {
+ *f << stringf(" (instance GND (viewRef VIEW_NETLIST (cellRef GND (libraryRef LIB))))\n");
+ *f << stringf(" (instance VCC (viewRef VIEW_NETLIST (cellRef VCC (libraryRef LIB))))\n");
+ }
for (auto &cell_it : module->cells_) {
RTLIL::Cell *cell = cell_it.second;
*f << stringf(" (instance %s\n", EDIF_DEF(cell->name));
@@ -326,6 +341,8 @@ struct EdifBackend : public Backend {
for (auto &ref : it.second)
*f << stringf(" %s\n", ref.c_str());
if (sig.wire == NULL) {
+ if (nogndvcc)
+ log_error("Design contains constant nodes (map with \"hilomap\" first).\n");
if (sig == RTLIL::State::S0)
*f << stringf(" (portRef G (instanceRef GND))\n");
if (sig == RTLIL::State::S1)
diff --git a/backends/ilang/ilang_backend.cc b/backends/ilang/ilang_backend.cc
index 814d3e8fe..03e29c524 100644
--- a/backends/ilang/ilang_backend.cc
+++ b/backends/ilang/ilang_backend.cc
@@ -2,11 +2,11 @@
* 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
@@ -391,7 +391,7 @@ struct IlangBackend : public Backend {
{
bool selected = false;
- log_header("Executing ILANG backend.\n");
+ log_header(design, "Executing ILANG backend.\n");
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++) {
@@ -492,5 +492,5 @@ struct DumpPass : public Pass {
}
}
} DumpPass;
-
+
PRIVATE_NAMESPACE_END
diff --git a/backends/ilang/ilang_backend.h b/backends/ilang/ilang_backend.h
index 159cd7192..97dcbb628 100644
--- a/backends/ilang/ilang_backend.h
+++ b/backends/ilang/ilang_backend.h
@@ -2,11 +2,11 @@
* 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
diff --git a/backends/intersynth/intersynth.cc b/backends/intersynth/intersynth.cc
index 6d4731e73..34cb52fb4 100644
--- a/backends/intersynth/intersynth.cc
+++ b/backends/intersynth/intersynth.cc
@@ -2,11 +2,11 @@
* 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
@@ -73,7 +73,7 @@ struct IntersynthBackend : public Backend {
}
virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
{
- log_header("Executing INTERSYNTH backend.\n");
+ log_header(design, "Executing INTERSYNTH backend.\n");
log_push();
std::vector<std::string> libfiles;
@@ -113,7 +113,7 @@ struct IntersynthBackend : public Backend {
}
if (libs.size() > 0)
- log_header("Continuing INTERSYNTH backend.\n");
+ log_header(design, "Continuing INTERSYNTH backend.\n");
std::set<std::string> conntypes_code, celltypes_code;
std::string netlists_code;
@@ -159,7 +159,7 @@ struct IntersynthBackend : public Backend {
}
}
- // Submodules: "std::set<string> celltypes_code" prevents duplicate cell types
+ // Submodules: "std::set<string> celltypes_code" prevents duplicate cell types
for (auto cell_it : module->cells_)
{
RTLIL::Cell *cell = cell_it.second;
diff --git a/backends/json/Makefile.inc b/backends/json/Makefile.inc
new file mode 100644
index 000000000..a463daf91
--- /dev/null
+++ b/backends/json/Makefile.inc
@@ -0,0 +1,3 @@
+
+OBJS += backends/json/json.o
+
diff --git a/backends/json/json.cc b/backends/json/json.cc
new file mode 100644
index 000000000..05530ee69
--- /dev/null
+++ b/backends/json/json.cc
@@ -0,0 +1,538 @@
+/*
+ * 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
+ * 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/rtlil.h"
+#include "kernel/register.h"
+#include "kernel/sigtools.h"
+#include "kernel/celltypes.h"
+#include "kernel/cellaigs.h"
+#include "kernel/log.h"
+#include <string>
+
+USING_YOSYS_NAMESPACE
+PRIVATE_NAMESPACE_BEGIN
+
+struct JsonWriter
+{
+ std::ostream &f;
+ bool use_selection;
+ bool aig_mode;
+
+ Design *design;
+ Module *module;
+
+ SigMap sigmap;
+ int sigidcounter;
+ dict<SigBit, string> sigids;
+ pool<Aig> aig_models;
+
+ JsonWriter(std::ostream &f, bool use_selection, bool aig_mode) :
+ f(f), use_selection(use_selection), aig_mode(aig_mode) { }
+
+ string get_string(string str)
+ {
+ string newstr = "\"";
+ for (char c : str) {
+ if (c == '\\')
+ newstr += c;
+ newstr += c;
+ }
+ return newstr + "\"";
+ }
+
+ string get_name(IdString name)
+ {
+ return get_string(RTLIL::unescape_id(name));
+ }
+
+ string get_bits(SigSpec sig)
+ {
+ bool first = true;
+ string str = "[";
+ for (auto bit : sigmap(sig)) {
+ str += first ? " " : ", ";
+ first = false;
+ if (sigids.count(bit) == 0) {
+ string &s = sigids[bit];
+ if (bit.wire == nullptr) {
+ if (bit == State::S0) s = "\"0\"";
+ else if (bit == State::S1) s = "\"1\"";
+ else if (bit == State::Sz) s = "\"z\"";
+ else s = "\"x\"";
+ } else
+ s = stringf("%d", sigidcounter++);
+ }
+ str += sigids[bit];
+ }
+ return str + " ]";
+ }
+
+ void write_parameters(const dict<IdString, Const> &parameters)
+ {
+ bool first = true;
+ for (auto &param : parameters) {
+ f << stringf("%s\n", first ? "" : ",");
+ f << stringf(" %s: ", get_name(param.first).c_str());
+ if ((param.second.flags & RTLIL::ConstFlags::CONST_FLAG_STRING) != 0)
+ f << get_string(param.second.decode_string());
+ else if (GetSize(param.second.bits) > 32)
+ f << get_string(param.second.as_string());
+ else
+ f << stringf("%d", param.second.as_int());
+ first = false;
+ }
+ }
+
+ void write_module(Module *module_)
+ {
+ module = module_;
+ log_assert(module->design == design);
+ sigmap.set(module);
+ sigids.clear();
+
+ // reserve 0 and 1 to avoid confusion with "0" and "1"
+ sigidcounter = 2;
+
+ f << stringf(" %s: {\n", get_name(module->name).c_str());
+
+ f << stringf(" \"ports\": {");
+ bool first = true;
+ for (auto n : module->ports) {
+ Wire *w = module->wire(n);
+ if (use_selection && !module->selected(w))
+ continue;
+ f << stringf("%s\n", first ? "" : ",");
+ f << stringf(" %s: {\n", get_name(n).c_str());
+ f << stringf(" \"direction\": \"%s\",\n", w->port_input ? w->port_output ? "inout" : "input" : "output");
+ f << stringf(" \"bits\": %s\n", get_bits(w).c_str());
+ f << stringf(" }");
+ first = false;
+ }
+ f << stringf("\n },\n");
+
+ f << stringf(" \"cells\": {");
+ first = true;
+ for (auto c : module->cells()) {
+ if (use_selection && !module->selected(c))
+ continue;
+ f << stringf("%s\n", first ? "" : ",");
+ f << stringf(" %s: {\n", get_name(c->name).c_str());
+ f << stringf(" \"hide_name\": %s,\n", c->name[0] == '$' ? "1" : "0");
+ f << stringf(" \"type\": %s,\n", get_name(c->type).c_str());
+ if (aig_mode) {
+ Aig aig(c);
+ if (!aig.name.empty()) {
+ f << stringf(" \"model\": \"%s\",\n", aig.name.c_str());
+ aig_models.insert(aig);
+ }
+ }
+ f << stringf(" \"parameters\": {");
+ write_parameters(c->parameters);
+ f << stringf("\n },\n");
+ f << stringf(" \"attributes\": {");
+ write_parameters(c->attributes);
+ f << stringf("\n },\n");
+ if (c->known()) {
+ f << stringf(" \"port_directions\": {");
+ bool first2 = true;
+ for (auto &conn : c->connections()) {
+ string direction = "output";
+ if (c->input(conn.first))
+ direction = c->output(conn.first) ? "inout" : "input";
+ f << stringf("%s\n", first2 ? "" : ",");
+ f << stringf(" %s: \"%s\"", get_name(conn.first).c_str(), direction.c_str());
+ first2 = false;
+ }
+ f << stringf("\n },\n");
+ }
+ f << stringf(" \"connections\": {");
+ bool first2 = true;
+ for (auto &conn : c->connections()) {
+ f << stringf("%s\n", first2 ? "" : ",");
+ f << stringf(" %s: %s", get_name(conn.first).c_str(), get_bits(conn.second).c_str());
+ first2 = false;
+ }
+ f << stringf("\n }\n");
+ f << stringf(" }");
+ first = false;
+ }
+ f << stringf("\n },\n");
+
+ f << stringf(" \"netnames\": {");
+ first = true;
+ for (auto w : module->wires()) {
+ if (use_selection && !module->selected(w))
+ continue;
+ f << stringf("%s\n", first ? "" : ",");
+ f << stringf(" %s: {\n", get_name(w->name).c_str());
+ f << stringf(" \"hide_name\": %s,\n", w->name[0] == '$' ? "1" : "0");
+ f << stringf(" \"bits\": %s,\n", get_bits(w).c_str());
+ f << stringf(" \"attributes\": {");
+ write_parameters(w->attributes);
+ f << stringf("\n }\n");
+ f << stringf(" }");
+ first = false;
+ }
+ f << stringf("\n }\n");
+
+ f << stringf(" }");
+ }
+
+ void write_design(Design *design_)
+ {
+ design = design_;
+ f << stringf("{\n");
+ f << stringf(" \"creator\": %s,\n", get_string(yosys_version_str).c_str());
+ f << stringf(" \"modules\": {\n");
+ vector<Module*> modules = use_selection ? design->selected_modules() : design->modules();
+ bool first_module = true;
+ for (auto mod : modules) {
+ if (!first_module)
+ f << stringf(",\n");
+ write_module(mod);
+ first_module = false;
+ }
+ f << stringf("\n }");
+ if (!aig_models.empty()) {
+ f << stringf(",\n \"models\": {\n");
+ bool first_model = true;
+ for (auto &aig : aig_models) {
+ if (!first_model)
+ f << stringf(",\n");
+ f << stringf(" \"%s\": [\n", aig.name.c_str());
+ int node_idx = 0;
+ for (auto &node : aig.nodes) {
+ if (node_idx != 0)
+ f << stringf(",\n");
+ f << stringf(" /* %3d */ [ ", node_idx);
+ if (node.portbit >= 0)
+ f << stringf("\"%sport\", \"%s\", %d", node.inverter ? "n" : "",
+ log_id(node.portname), node.portbit);
+ else if (node.left_parent < 0 && node.right_parent < 0)
+ f << stringf("\"%s\"", node.inverter ? "true" : "false");
+ else
+ f << stringf("\"%s\", %d, %d", node.inverter ? "nand" : "and", node.left_parent, node.right_parent);
+ for (auto &op : node.outports)
+ f << stringf(", \"%s\", %d", log_id(op.first), op.second);
+ f << stringf(" ]");
+ node_idx++;
+ }
+ f << stringf("\n ]");
+ first_model = false;
+ }
+ f << stringf("\n }");
+ }
+ f << stringf("\n}\n");
+ }
+};
+
+struct JsonBackend : public Backend {
+ JsonBackend() : Backend("json", "write design to a JSON file") { }
+ virtual void help()
+ {
+ // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+ log("\n");
+ log(" write_json [options] [filename]\n");
+ log("\n");
+ log("Write a JSON netlist of the current design.\n");
+ log("\n");
+ log(" -aig\n");
+ log(" include AIG models for the different gate types\n");
+ log("\n");
+ log("\n");
+ log("The general syntax of the JSON output created by this command is as follows:\n");
+ log("\n");
+ log(" {\n");
+ log(" \"modules\": {\n");
+ log(" <module_name>: {\n");
+ log(" \"ports\": {\n");
+ log(" <port_name>: <port_details>,\n");
+ log(" ...\n");
+ log(" },\n");
+ log(" \"cells\": {\n");
+ log(" <cell_name>: <cell_details>,\n");
+ log(" ...\n");
+ log(" },\n");
+ log(" \"netnames\": {\n");
+ log(" <net_name>: <net_details>,\n");
+ log(" ...\n");
+ log(" }\n");
+ log(" }\n");
+ log(" },\n");
+ log(" \"models\": {\n");
+ log(" ...\n");
+ log(" },\n");
+ log(" }\n");
+ log("\n");
+ log("Where <port_details> is:\n");
+ log("\n");
+ log(" {\n");
+ log(" \"direction\": <\"input\" | \"output\" | \"inout\">,\n");
+ log(" \"bits\": <bit_vector>\n");
+ log(" }\n");
+ log("\n");
+ log("And <cell_details> is:\n");
+ log("\n");
+ log(" {\n");
+ log(" \"hide_name\": <1 | 0>,\n");
+ log(" \"type\": <cell_type>,\n");
+ log(" \"parameters\": {\n");
+ log(" <parameter_name>: <parameter_value>,\n");
+ log(" ...\n");
+ log(" },\n");
+ log(" \"attributes\": {\n");
+ log(" <attribute_name>: <attribute_value>,\n");
+ log(" ...\n");
+ log(" },\n");
+ log(" \"port_directions\": {\n");
+ log(" <port_name>: <\"input\" | \"output\" | \"inout\">,\n");
+ log(" ...\n");
+ log(" },\n");
+ log(" \"connections\": {\n");
+ log(" <port_name>: <bit_vector>,\n");
+ log(" ...\n");
+ log(" },\n");
+ log(" }\n");
+ log("\n");
+ log("And <net_details> is:\n");
+ log("\n");
+ log(" {\n");
+ log(" \"hide_name\": <1 | 0>,\n");
+ log(" \"bits\": <bit_vector>\n");
+ log(" }\n");
+ log("\n");
+ log("The \"hide_name\" fields are set to 1 when the name of this cell or net is\n");
+ log("automatically created and is likely not of interest for a regular user.\n");
+ log("\n");
+ log("The \"port_directions\" section is only included for cells for which the\n");
+ log("interface is known.\n");
+ log("\n");
+ log("Module and cell ports and nets can be single bit wide or vectors of multiple\n");
+ log("bits. Each individual signal bit is assigned a unique integer. The <bit_vector>\n");
+ log("values referenced above are vectors of this integers. Signal bits that are\n");
+ log("connected to a constant driver are denoted as string \"0\" or \"1\" instead of\n");
+ log("a number.\n");
+ log("\n");
+ log("For example the following Verilog code:\n");
+ log("\n");
+ log(" module test(input x, y);\n");
+ log(" (* keep *) foo #(.P(42), .Q(1337))\n");
+ log(" foo_inst (.A({x, y}), .B({y, x}), .C({4'd10, {4{x}}}));\n");
+ log(" endmodule\n");
+ log("\n");
+ log("Translates to the following JSON output:\n");
+ log("\n");
+ log(" {\n");
+ log(" \"modules\": {\n");
+ log(" \"test\": {\n");
+ log(" \"ports\": {\n");
+ log(" \"x\": {\n");
+ log(" \"direction\": \"input\",\n");
+ log(" \"bits\": [ 2 ]\n");
+ log(" },\n");
+ log(" \"y\": {\n");
+ log(" \"direction\": \"input\",\n");
+ log(" \"bits\": [ 3 ]\n");
+ log(" }\n");
+ log(" },\n");
+ log(" \"cells\": {\n");
+ log(" \"foo_inst\": {\n");
+ log(" \"hide_name\": 0,\n");
+ log(" \"type\": \"foo\",\n");
+ log(" \"parameters\": {\n");
+ log(" \"Q\": 1337,\n");
+ log(" \"P\": 42\n");
+ log(" },\n");
+ log(" \"attributes\": {\n");
+ log(" \"keep\": 1,\n");
+ log(" \"src\": \"test.v:2\"\n");
+ log(" },\n");
+ log(" \"connections\": {\n");
+ log(" \"C\": [ 2, 2, 2, 2, \"0\", \"1\", \"0\", \"1\" ],\n");
+ log(" \"B\": [ 2, 3 ],\n");
+ log(" \"A\": [ 3, 2 ]\n");
+ log(" }\n");
+ log(" }\n");
+ log(" },\n");
+ log(" \"netnames\": {\n");
+ log(" \"y\": {\n");
+ log(" \"hide_name\": 0,\n");
+ log(" \"bits\": [ 3 ],\n");
+ log(" \"attributes\": {\n");
+ log(" \"src\": \"test.v:1\"\n");
+ log(" }\n");
+ log(" },\n");
+ log(" \"x\": {\n");
+ log(" \"hide_name\": 0,\n");
+ log(" \"bits\": [ 2 ],\n");
+ log(" \"attributes\": {\n");
+ log(" \"src\": \"test.v:1\"\n");
+ log(" }\n");
+ log(" }\n");
+ log(" }\n");
+ log(" }\n");
+ log(" }\n");
+ log(" }\n");
+ log("\n");
+ log("The models are given as And-Inverter-Graphs (AIGs) in the following form:\n");
+ log("\n");
+ log(" \"models\": {\n");
+ log(" <model_name>: [\n");
+ log(" /* 0 */ [ <node-spec> ],\n");
+ log(" /* 1 */ [ <node-spec> ],\n");
+ log(" /* 2 */ [ <node-spec> ],\n");
+ log(" ...\n");
+ log(" ],\n");
+ log(" ...\n");
+ log(" },\n");
+ log("\n");
+ log("The following node-types may be used:\n");
+ log("\n");
+ log(" [ \"port\", <portname>, <bitindex>, <out-list> ]\n");
+ log(" - the value of the specified input port bit\n");
+ log("\n");
+ log(" [ \"nport\", <portname>, <bitindex>, <out-list> ]\n");
+ log(" - the inverted value of the specified input port bit\n");
+ log("\n");
+ log(" [ \"and\", <node-index>, <node-index>, <out-list> ]\n");
+ log(" - the ANDed value of the specified nodes\n");
+ log("\n");
+ log(" [ \"nand\", <node-index>, <node-index>, <out-list> ]\n");
+ log(" - the inverted ANDed value of the specified nodes\n");
+ log("\n");
+ log(" [ \"true\", <out-list> ]\n");
+ log(" - the constant value 1\n");
+ log("\n");
+ log(" [ \"false\", <out-list> ]\n");
+ log(" - the constant value 0\n");
+ log("\n");
+ log("All nodes appear in topological order. I.e. only nodes with smaller indices\n");
+ log("are referenced by \"and\" and \"nand\" nodes.\n");
+ log("\n");
+ log("The optional <out-list> at the end of a node specification is a list of\n");
+ log("output portname and bitindex pairs, specifying the outputs driven by this node.\n");
+ log("\n");
+ log("For example, the following is the model for a 3-input 3-output $reduce_and cell\n");
+ log("inferred by the following code:\n");
+ log("\n");
+ log(" module test(input [2:0] in, output [2:0] out);\n");
+ log(" assign in = &out;\n");
+ log(" endmodule\n");
+ log("\n");
+ log(" \"$reduce_and:3U:3\": [\n");
+ log(" /* 0 */ [ \"port\", \"A\", 0 ],\n");
+ log(" /* 1 */ [ \"port\", \"A\", 1 ],\n");
+ log(" /* 2 */ [ \"and\", 0, 1 ],\n");
+ log(" /* 3 */ [ \"port\", \"A\", 2 ],\n");
+ log(" /* 4 */ [ \"and\", 2, 3, \"Y\", 0 ],\n");
+ log(" /* 5 */ [ \"false\", \"Y\", 1, \"Y\", 2 ]\n");
+ log(" ]\n");
+ log("\n");
+ log("Future version of Yosys might add support for additional fields in the JSON\n");
+ log("format. A program processing this format must ignore all unknown fields.\n");
+ log("\n");
+ }
+ virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
+ {
+ bool aig_mode = false;
+
+ size_t argidx;
+ for (argidx = 1; argidx < args.size(); argidx++)
+ {
+ if (args[argidx] == "-aig") {
+ aig_mode = true;
+ continue;
+ }
+ break;
+ }
+ extra_args(f, filename, args, argidx);
+
+ log_header(design, "Executing JSON backend.\n");
+
+ JsonWriter json_writer(*f, false, aig_mode);
+ json_writer.write_design(design);
+ }
+} JsonBackend;
+
+struct JsonPass : public Pass {
+ JsonPass() : Pass("json", "write design in JSON format") { }
+ virtual void help()
+ {
+ // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+ log("\n");
+ log(" json [options] [selection]\n");
+ log("\n");
+ log("Write a JSON netlist of all selected objects.\n");
+ log("\n");
+ log(" -o <filename>\n");
+ log(" write to the specified file.\n");
+ log("\n");
+ log(" -aig\n");
+ log(" also include AIG models for the different gate types\n");
+ log("\n");
+ log("See 'help write_json' for a description of the JSON format used.\n");
+ log("\n");
+ }
+ virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
+ {
+ std::string filename;
+ bool aig_mode = false;
+
+ size_t argidx;
+ for (argidx = 1; argidx < args.size(); argidx++)
+ {
+ if (args[argidx] == "-o" && argidx+1 < args.size()) {
+ filename = args[++argidx];
+ continue;
+ }
+ if (args[argidx] == "-aig") {
+ aig_mode = true;
+ continue;
+ }
+ break;
+ }
+ extra_args(args, argidx, design);
+
+ std::ostream *f;
+ std::stringstream buf;
+
+ if (!filename.empty()) {
+ std::ofstream *ff = new std::ofstream;
+ ff->open(filename.c_str(), std::ofstream::trunc);
+ if (ff->fail()) {
+ delete ff;
+ log_error("Can't open file `%s' for writing: %s\n", filename.c_str(), strerror(errno));
+ }
+ f = ff;
+ } else {
+ f = &buf;
+ }
+
+ JsonWriter json_writer(*f, true, aig_mode);
+ json_writer.write_design(design);
+
+ if (!filename.empty()) {
+ delete f;
+ } else {
+ log("%s", buf.str().c_str());
+ }
+ }
+} JsonPass;
+
+PRIVATE_NAMESPACE_END
diff --git a/backends/smt2/Makefile.inc b/backends/smt2/Makefile.inc
index 4e0a393a8..eacda2734 100644
--- a/backends/smt2/Makefile.inc
+++ b/backends/smt2/Makefile.inc
@@ -1,3 +1,16 @@
OBJS += backends/smt2/smt2.o
+ifneq ($(CONFIG),mxe)
+ifneq ($(CONFIG),emcc)
+TARGETS += yosys-smtbmc
+
+yosys-smtbmc: backends/smt2/smtbmc.py
+ $(P) sed 's|##yosys-sys-path##|sys.path += [os.path.dirname(__file__) + p for p in ["/share/python3", "/../share/yosys/python3"]]|;' < $< > $@.new
+ $(Q) chmod +x $@.new
+ $(Q) mv $@.new $@
+
+$(eval $(call add_share_file,share/python3,backends/smt2/smtio.py))
+endif
+endif
+
diff --git a/backends/smt2/example.v b/backends/smt2/example.v
new file mode 100644
index 000000000..b195266eb
--- /dev/null
+++ b/backends/smt2/example.v
@@ -0,0 +1,11 @@
+module main(input clk);
+ reg [3:0] counter = 0;
+ always @(posedge clk) begin
+ if (counter == 10)
+ counter <= 0;
+ else
+ counter <= counter + 1;
+ end
+ assert property (counter != 15);
+ // assert property (counter <= 10);
+endmodule
diff --git a/backends/smt2/example.ys b/backends/smt2/example.ys
new file mode 100644
index 000000000..6fccb344f
--- /dev/null
+++ b/backends/smt2/example.ys
@@ -0,0 +1,3 @@
+read_verilog -formal example.v
+hierarchy; proc; opt; memory -nordff -nomap; opt -fast
+write_smt2 -bv -mem -wires example.smt2
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 8451eff4f..e869f78cd 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -2,11 +2,11 @@
* 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
@@ -32,17 +32,21 @@ struct Smt2Worker
CellTypes ct;
SigMap sigmap;
RTLIL::Module *module;
- bool bvmode;
+ bool bvmode, memmode, regsmode, wiresmode, verbose;
int idcounter;
std::vector<std::string> decls, trans;
std::map<RTLIL::SigBit, RTLIL::Cell*> bit_driver;
std::set<RTLIL::Cell*> exported_cells;
+ pool<Cell*> recursive_cells, registers;
std::map<RTLIL::SigBit, std::pair<int, int>> fcache;
+ std::map<Cell*, int> memarrays;
std::map<int, int> bvsizes;
- Smt2Worker(RTLIL::Module *module, bool bvmode) : ct(module->design), sigmap(module), module(module), bvmode(bvmode), idcounter(0)
+ Smt2Worker(RTLIL::Module *module, bool bvmode, bool memmode, bool regsmode, bool wiresmode, bool verbose) :
+ ct(module->design), sigmap(module), module(module), bvmode(bvmode), memmode(memmode),
+ regsmode(regsmode), wiresmode(wiresmode), verbose(verbose), idcounter(0)
{
decls.push_back(stringf("(declare-sort |%s_s| 0)\n", log_id(module)));
@@ -64,6 +68,9 @@ struct Smt2Worker
void register_bool(RTLIL::SigBit bit, int id)
{
+ if (verbose) log("%*s-> register_bool: %s %d\n", 2+2*GetSize(recursive_cells), "",
+ log_signal(bit), id);
+
sigmap.apply(bit);
log_assert(fcache.count(bit) == 0);
fcache[bit] = std::pair<int, int>(id, -1);
@@ -71,6 +78,9 @@ struct Smt2Worker
void register_bv(RTLIL::SigSpec sig, int id)
{
+ if (verbose) log("%*s-> register_bv: %s %d\n", 2+2*GetSize(recursive_cells), "",
+ log_signal(sig), id);
+
log_assert(bvmode);
sigmap.apply(sig);
@@ -85,6 +95,9 @@ struct Smt2Worker
void register_boolvec(RTLIL::SigSpec sig, int id)
{
+ if (verbose) log("%*s-> register_boolvec: %s %d\n", 2+2*GetSize(recursive_cells), "",
+ log_signal(sig), id);
+
log_assert(bvmode);
sigmap.apply(sig);
register_bool(sig[0], id);
@@ -105,6 +118,8 @@ struct Smt2Worker
sigmap.apply(bit);
if (fcache.count(bit) == 0) {
+ if (verbose) log("%*s-> external bool: %s\n", 2+2*GetSize(recursive_cells), "",
+ log_signal(bit));
decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) Bool) ; %s\n",
log_id(module), idcounter, log_id(module), log_signal(bit)));
register_bool(bit, idcounter++);
@@ -118,7 +133,7 @@ struct Smt2Worker
std::string get_bool(RTLIL::SigSpec sig, const char *state_name = "state")
{
- return get_bool(sig.to_single_sigbit(), state_name);
+ return get_bool(sig.as_bit(), state_name);
}
std::string get_bv(RTLIL::SigSpec sig, const char *state_name = "state")
@@ -128,10 +143,14 @@ struct Smt2Worker
std::vector<std::string> subexpr;
- for (auto bit : sig)
- if (bit_driver.count(bit))
- export_cell(bit_driver.at(bit));
- sigmap.apply(sig);
+ SigSpec orig_sig;
+ while (orig_sig != sig) {
+ for (auto bit : sig)
+ if (bit_driver.count(bit))
+ export_cell(bit_driver.at(bit));
+ orig_sig = sig;
+ sigmap.apply(sig);
+ }
for (int i = 0, j = 1; i < GetSize(sig); i += j, j = 1)
{
@@ -161,9 +180,10 @@ struct Smt2Worker
j++;
}
if (t1.second == 0 && j == bvsizes.at(t1.first))
- subexpr.push_back(stringf("(|%s#%d| state)", log_id(module), t1.first));
+ subexpr.push_back(stringf("(|%s#%d| %s)", log_id(module), t1.first, state_name));
else
- subexpr.push_back(stringf("((_ extract %d %d) (|%s#%d| state))", t1.second + j - 1, t1.second, log_id(module), t1.first));
+ subexpr.push_back(stringf("((_ extract %d %d) (|%s#%d| %s))",
+ t1.second + j - 1, t1.second, log_id(module), t1.first, state_name));
continue;
}
@@ -171,17 +191,23 @@ struct Smt2Worker
while (i+j < GetSize(sig) && sig[i+j].wire && !fcache.count(sig[i+j]) && !seen_bits.count(sig[i+j]))
seen_bits.insert(sig[i+j]), j++;
+ if (verbose) log("%*s-> external bv: %s\n", 2+2*GetSize(recursive_cells), "",
+ log_signal(sig.extract(i, j)));
+ for (auto bit : sig.extract(i, j))
+ log_assert(bit_driver.count(bit) == 0);
decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) (_ BitVec %d)) ; %s\n",
log_id(module), idcounter, log_id(module), j, log_signal(sig.extract(i, j))));
- subexpr.push_back(stringf("(|%s#%d| state)", log_id(module), idcounter));
+ subexpr.push_back(stringf("(|%s#%d| %s)", log_id(module), idcounter, state_name));
register_bv(sig.extract(i, j), idcounter++);
}
if (GetSize(subexpr) > 1) {
- std::string expr = "(concat";
- for (int i = GetSize(subexpr)-1; i >= 0; i--)
+ std::string expr = "", end_str = "";
+ for (int i = GetSize(subexpr)-1; i >= 0; i--) {
+ if (i > 0) expr += " (concat", end_str += ")";
expr += " " + subexpr[i];
- return expr + ")";
+ }
+ return expr.substr(1) + end_str;
} else {
log_assert(GetSize(subexpr) == 1);
return subexpr[0];
@@ -190,7 +216,7 @@ struct Smt2Worker
void export_gate(RTLIL::Cell *cell, std::string expr)
{
- RTLIL::SigBit bit = sigmap(cell->getPort("\\Y").to_single_sigbit());
+ RTLIL::SigBit bit = sigmap(cell->getPort("\\Y").as_bit());
std::string processed_expr;
for (char ch : expr) {
@@ -202,10 +228,12 @@ struct Smt2Worker
else processed_expr += ch;
}
+ if (verbose) log("%*s-> import cell: %s\n", 2+2*GetSize(recursive_cells), "",
+ log_id(cell));
decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool %s) ; %s\n",
log_id(module), idcounter, log_id(module), processed_expr.c_str(), log_signal(bit)));
register_bool(bit, idcounter++);
- return;
+ recursive_cells.erase(cell);
}
void export_bvop(RTLIL::Cell *cell, std::string expr, char type = 0)
@@ -216,8 +244,8 @@ struct Smt2Worker
int width = GetSize(sig_y);
if (type == 's' || type == 'd' || type == 'b') {
- width = std::max(width, GetSize(cell->getPort("\\A")));
- width = std::max(width, GetSize(cell->getPort("\\B")));
+ width = max(width, GetSize(cell->getPort("\\A")));
+ width = max(width, GetSize(cell->getPort("\\B")));
}
if (cell->hasPort("\\A")) {
@@ -243,6 +271,9 @@ struct Smt2Worker
if (width != GetSize(sig_y) && type != 'b')
processed_expr = stringf("((_ extract %d 0) %s)", GetSize(sig_y)-1, processed_expr.c_str());
+ if (verbose) log("%*s-> import cell: %s\n", 2+2*GetSize(recursive_cells), "",
+ log_id(cell));
+
if (type == 'b') {
decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool %s) ; %s\n",
log_id(module), idcounter, log_id(module), processed_expr.c_str(), log_signal(sig_y)));
@@ -252,7 +283,8 @@ struct Smt2Worker
log_id(module), idcounter, log_id(module), GetSize(sig_y), processed_expr.c_str(), log_signal(sig_y)));
register_bv(sig_y, idcounter++);
}
- return;
+
+ recursive_cells.erase(cell);
}
void export_reduce(RTLIL::Cell *cell, std::string expr, bool identity_val)
@@ -270,23 +302,35 @@ struct Smt2Worker
} else
processed_expr += ch;
+ if (verbose) log("%*s-> import cell: %s\n", 2+2*GetSize(recursive_cells), "",
+ log_id(cell));
decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool %s) ; %s\n",
log_id(module), idcounter, log_id(module), processed_expr.c_str(), log_signal(sig_y)));
register_boolvec(sig_y, idcounter++);
- return;
+ recursive_cells.erase(cell);
}
void export_cell(RTLIL::Cell *cell)
{
+ if (verbose) log("%*s=> export_cell %s (%s) [%s]\n", 2+2*GetSize(recursive_cells), "",
+ log_id(cell), log_id(cell->type), exported_cells.count(cell) ? "old" : "new");
+
+ if (recursive_cells.count(cell))
+ log_error("Found logic loop in module %s! See cell %s.\n", log_id(module), log_id(cell));
+
if (exported_cells.count(cell))
return;
+
exported_cells.insert(cell);
+ recursive_cells.insert(cell);
if (cell->type == "$_DFF_P_" || cell->type == "$_DFF_N_")
{
- std::string expr_d = get_bool(cell->getPort("\\D"));
- std::string expr_q = get_bool(cell->getPort("\\Q"), "next_state");
- trans.push_back(stringf(" (= %s %s)\n", expr_d.c_str(), expr_q.c_str()));
+ registers.insert(cell);
+ decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) Bool) ; %s\n",
+ log_id(module), idcounter, log_id(module), log_signal(cell->getPort("\\Q"))));
+ register_bool(cell->getPort("\\Q"), idcounter++);
+ recursive_cells.erase(cell);
return;
}
@@ -304,94 +348,157 @@ struct Smt2Worker
if (cell->type == "$_AOI4_") return export_gate(cell, "(not (or (and A B) (and C D)))");
if (cell->type == "$_OAI4_") return export_gate(cell, "(not (and (or A B) (or C D)))");
- // FIXME: $lut $assert
-
- if (!bvmode)
- log_error("Unsupported cell type %s for cell %s.%s. (Maybe this cell type would be supported in -bv mode?)\n",
- log_id(cell->type), log_id(module), log_id(cell));
+ // FIXME: $lut
- if (cell->type == "$dff")
+ if (bvmode)
{
- std::string expr_d = get_bv(cell->getPort("\\D"));
- std::string expr_q = get_bv(cell->getPort("\\Q"), "next_state");
- trans.push_back(stringf(" (= %s %s)\n", expr_d.c_str(), expr_q.c_str()));
- return;
+ if (cell->type == "$dff")
+ {
+ registers.insert(cell);
+ decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) (_ BitVec %d)) ; %s\n",
+ log_id(module), idcounter, log_id(module), GetSize(cell->getPort("\\Q")), log_signal(cell->getPort("\\Q"))));
+ register_bv(cell->getPort("\\Q"), idcounter++);
+ recursive_cells.erase(cell);
+ return;
+ }
+
+ if (cell->type == "$and") return export_bvop(cell, "(bvand A B)");
+ if (cell->type == "$or") return export_bvop(cell, "(bvor A B)");
+ if (cell->type == "$xor") return export_bvop(cell, "(bvxor A B)");
+ if (cell->type == "$xnor") return export_bvop(cell, "(bvxnor A B)");
+
+ if (cell->type == "$shl") return export_bvop(cell, "(bvshl A B)", 's');
+ if (cell->type == "$shr") return export_bvop(cell, "(bvlshr A B)", 's');
+ if (cell->type == "$sshl") return export_bvop(cell, "(bvshl A B)", 's');
+ if (cell->type == "$sshr") return export_bvop(cell, "(bvLshr A B)", 's');
+
+ // FIXME: $shift $shiftx
+
+ if (cell->type == "$lt") return export_bvop(cell, "(bvUlt A B)", 'b');
+ if (cell->type == "$le") return export_bvop(cell, "(bvUle A B)", 'b');
+ if (cell->type == "$ge") return export_bvop(cell, "(bvUge A B)", 'b');
+ if (cell->type == "$gt") return export_bvop(cell, "(bvUgt A B)", 'b');
+
+ if (cell->type == "$ne") return export_bvop(cell, "(distinct A B)", 'b');
+ if (cell->type == "$nex") return export_bvop(cell, "(distinct A B)", 'b');
+ if (cell->type == "$eq") return export_bvop(cell, "(= A B)", 'b');
+ if (cell->type == "$eqx") return export_bvop(cell, "(= A B)", 'b');
+
+ if (cell->type == "$not") return export_bvop(cell, "(bvnot A)");
+ if (cell->type == "$pos") return export_bvop(cell, "A");
+ if (cell->type == "$neg") return export_bvop(cell, "(bvneg A)");
+
+ if (cell->type == "$add") return export_bvop(cell, "(bvadd A B)");
+ if (cell->type == "$sub") return export_bvop(cell, "(bvsub A B)");
+ if (cell->type == "$mul") return export_bvop(cell, "(bvmul A B)");
+ if (cell->type == "$div") return export_bvop(cell, "(bvUdiv A B)", 'd');
+ if (cell->type == "$mod") return export_bvop(cell, "(bvUrem A B)", 'd');
+
+ if (cell->type == "$reduce_and") return export_reduce(cell, "(and A)", true);
+ if (cell->type == "$reduce_or") return export_reduce(cell, "(or A)", false);
+ if (cell->type == "$reduce_xor") return export_reduce(cell, "(xor A)", false);
+ if (cell->type == "$reduce_xnor") return export_reduce(cell, "(not (xor A))", false);
+ if (cell->type == "$reduce_bool") return export_reduce(cell, "(or A)", false);
+
+ if (cell->type == "$logic_not") return export_reduce(cell, "(not (or A))", false);
+ if (cell->type == "$logic_and") return export_reduce(cell, "(and (or A) (or B))", false);
+ if (cell->type == "$logic_or") return export_reduce(cell, "(or A B)", false);
+
+ if (cell->type == "$mux" || cell->type == "$pmux")
+ {
+ int width = GetSize(cell->getPort("\\Y"));
+ std::string processed_expr = get_bv(cell->getPort("\\A"));
+
+ RTLIL::SigSpec sig_b = cell->getPort("\\B");
+ RTLIL::SigSpec sig_s = cell->getPort("\\S");
+ get_bv(sig_b);
+ get_bv(sig_s);
+
+ for (int i = 0; i < GetSize(sig_s); i++)
+ processed_expr = stringf("(ite %s %s %s)", get_bool(sig_s[i]).c_str(),
+ get_bv(sig_b.extract(i*width, width)).c_str(), processed_expr.c_str());
+
+ if (verbose) log("%*s-> import cell: %s\n", 2+2*GetSize(recursive_cells), "",
+ log_id(cell));
+ RTLIL::SigSpec sig = sigmap(cell->getPort("\\Y"));
+ decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
+ log_id(module), idcounter, log_id(module), width, processed_expr.c_str(), log_signal(sig)));
+ register_bv(sig, idcounter++);
+ recursive_cells.erase(cell);
+ return;
+ }
+
+ // FIXME: $slice $concat
}
- if (cell->type == "$and") return export_bvop(cell, "(bvand A B)");
- if (cell->type == "$or") return export_bvop(cell, "(bvor A B)");
- if (cell->type == "$xor") return export_bvop(cell, "(bvxor A B)");
- if (cell->type == "$xnor") return export_bvop(cell, "(bvxnor A B)");
-
- if (cell->type == "$shl") return export_bvop(cell, "(bvshl A B)", 's');
- if (cell->type == "$shr") return export_bvop(cell, "(bvlshr A B)", 's');
- if (cell->type == "$sshl") return export_bvop(cell, "(bvshl A B)", 's');
- if (cell->type == "$sshr") return export_bvop(cell, "(bvLshr A B)", 's');
-
- // FIXME: $shift $shiftx
-
- if (cell->type == "$lt") return export_bvop(cell, "(bvUlt A B)", 'b');
- if (cell->type == "$le") return export_bvop(cell, "(bvUle A B)", 'b');
- if (cell->type == "$ge") return export_bvop(cell, "(bvUge A B)", 'b');
- if (cell->type == "$gt") return export_bvop(cell, "(bvUgt A B)", 'b');
-
- if (cell->type == "$ne") return export_bvop(cell, "(distinct A B)", 'b');
- if (cell->type == "$nex") return export_bvop(cell, "(distinct A B)", 'b');
- if (cell->type == "$eq") return export_bvop(cell, "(= A B)", 'b');
- if (cell->type == "$eqx") return export_bvop(cell, "(= A B)", 'b');
-
- if (cell->type == "$not") return export_bvop(cell, "(bvnot A)");
- if (cell->type == "$pos") return export_bvop(cell, "A");
- if (cell->type == "$neg") return export_bvop(cell, "(bvneg A)");
-
- if (cell->type == "$add") return export_bvop(cell, "(bvadd A B)");
- if (cell->type == "$sub") return export_bvop(cell, "(bvsub A B)");
- if (cell->type == "$mul") return export_bvop(cell, "(bvmul A B)");
- if (cell->type == "$div") return export_bvop(cell, "(bvUdiv A B)", 'd');
- if (cell->type == "$mod") return export_bvop(cell, "(bvUrem A B)", 'd');
-
- if (cell->type == "$reduce_and") return export_reduce(cell, "(and A)", true);
- if (cell->type == "$reduce_or") return export_reduce(cell, "(or A)", false);
- if (cell->type == "$reduce_xor") return export_reduce(cell, "(xor A)", false);
- if (cell->type == "$reduce_xnor") return export_reduce(cell, "(not (xor A))", false);
- if (cell->type == "$reduce_bool") return export_reduce(cell, "(or A)", false);
-
- if (cell->type == "$logic_not") return export_reduce(cell, "(not (or A))", false);
- if (cell->type == "$logic_and") return export_reduce(cell, "(and (or A) (or B))", false);
- if (cell->type == "$logic_or") return export_reduce(cell, "(or A B)", false);
-
- if (cell->type == "$mux" || cell->type == "$pmux")
+ if (memmode && cell->type == "$mem")
{
- int width = GetSize(cell->getPort("\\Y"));
- std::string processed_expr = get_bv(cell->getPort("\\A"));
+ int arrayid = idcounter++;
+ memarrays[cell] = arrayid;
- RTLIL::SigSpec sig_b = cell->getPort("\\B");
- RTLIL::SigSpec sig_s = cell->getPort("\\S");
- get_bv(sig_b);
- get_bv(sig_s);
+ int abits = cell->getParam("\\ABITS").as_int();
+ int width = cell->getParam("\\WIDTH").as_int();
+ int rd_ports = cell->getParam("\\RD_PORTS").as_int();
- for (int i = 0; i < GetSize(sig_s); i++)
- processed_expr = stringf("(ite %s %s %s)", get_bool(sig_s[i]).c_str(),
- get_bv(sig_b.extract(i*width, width)).c_str(), processed_expr.c_str());
+ decls.push_back(stringf("(declare-fun |%s#%d#0| (|%s_s|) (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n",
+ log_id(module), arrayid, log_id(module), abits, width, log_id(cell)));
- RTLIL::SigSpec sig = sigmap(cell->getPort("\\Y"));
- decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
- log_id(module), idcounter, log_id(module), width, processed_expr.c_str(), log_signal(sig)));
- register_bv(sig, idcounter++);
+ decls.push_back(stringf("(define-fun |%s_m %s| ((state |%s_s|)) (Array (_ BitVec %d) (_ BitVec %d)) (|%s#%d#0| state))\n",
+ log_id(module), log_id(cell), log_id(module), abits, width, log_id(module), arrayid));
+
+ for (int i = 0; i < rd_ports; i++)
+ {
+ std::string addr = get_bv(cell->getPort("\\RD_ADDR").extract(abits*i, abits));
+ SigSpec data_sig = cell->getPort("\\RD_DATA").extract(width*i, width);
+
+ if (cell->getParam("\\RD_CLK_ENABLE").extract(i).as_bool())
+ log_error("Read port %d (%s) of memory %s.%s is clocked. This is not supported by \"write_smt2\"! "
+ "Call \"memory\" with -nordff to avoid this error.\n", i, log_signal(data_sig), log_id(cell), log_id(module));
+
+ decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d) (select (|%s#%d#0| state) %s)) ; %s\n",
+ log_id(module), idcounter, log_id(module), width, log_id(module), arrayid, addr.c_str(), log_signal(data_sig)));
+ register_bv(data_sig, idcounter++);
+ }
+
+ registers.insert(cell);
+ recursive_cells.erase(cell);
return;
}
- // FIXME: $slice $concat
-
- log_error("Unsupported cell type %s for cell %s.%s.\n",
+ log_error("Unsupported cell type %s for cell %s.%s. (Maybe this cell type would be supported in -bv or -mem mode?)\n",
log_id(cell->type), log_id(module), log_id(cell));
}
void run()
{
- for (auto wire : module->wires())
- if (wire->port_id || wire->get_bool_attribute("\\keep")) {
+ if (verbose) log("=> export logic driving outputs\n");
+
+ pool<SigBit> reg_bits;
+ if (regsmode) {
+ for (auto cell : module->cells())
+ if (cell->type.in("$_DFF_P_", "$_DFF_N_", "$dff")) {
+ // not using sigmap -- we want the net directly at the dff output
+ for (auto bit : cell->getPort("\\Q"))
+ reg_bits.insert(bit);
+ }
+ }
+
+ for (auto wire : module->wires()) {
+ bool is_register = false;
+ if (regsmode)
+ for (auto bit : SigSpec(wire))
+ if (reg_bits.count(bit))
+ is_register = true;
+ if (wire->port_id || is_register || wire->get_bool_attribute("\\keep") || (wiresmode && wire->name[0] == '\\')) {
RTLIL::SigSpec sig = sigmap(wire);
+ if (wire->port_input)
+ decls.push_back(stringf("; yosys-smt2-input %s %d\n", log_id(wire), wire->width));
+ if (wire->port_output)
+ decls.push_back(stringf("; yosys-smt2-output %s %d\n", log_id(wire), wire->width));
+ if (is_register)
+ decls.push_back(stringf("; yosys-smt2-register %s %d\n", log_id(wire), wire->width));
+ if (wire->get_bool_attribute("\\keep") || (wiresmode && wire->name[0] == '\\'))
+ decls.push_back(stringf("; yosys-smt2-wire %s %d\n", log_id(wire), wire->width));
if (bvmode && GetSize(sig) > 1) {
decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) (_ BitVec %d) %s)\n",
log_id(module), log_id(wire), log_id(module), GetSize(sig), get_bv(sig).c_str()));
@@ -405,6 +512,118 @@ struct Smt2Worker
log_id(module), log_id(wire), log_id(module), get_bool(sig[i]).c_str()));
}
}
+ }
+
+ if (verbose) log("=> export logic associated with the initial state\n");
+
+ vector<string> init_list;
+ for (auto wire : module->wires())
+ if (wire->attributes.count("\\init")) {
+ RTLIL::SigSpec sig = sigmap(wire);
+ Const val = wire->attributes.at("\\init");
+ val.bits.resize(GetSize(sig));
+ if (bvmode && GetSize(sig) > 1) {
+ init_list.push_back(stringf("(= %s #b%s) ; %s", get_bv(sig).c_str(), val.as_string().c_str(), log_id(wire)));
+ } else {
+ for (int i = 0; i < GetSize(sig); i++)
+ init_list.push_back(stringf("(= %s %s) ; %s", get_bool(sig[i]).c_str(), val.bits[i] == State::S1 ? "true" : "false", log_id(wire)));
+ }
+ }
+
+ if (verbose) log("=> export logic driving asserts\n");
+
+ vector<int> assert_list, assume_list;
+ for (auto cell : module->cells())
+ if (cell->type.in("$assert", "$assume")) {
+ string name_a = get_bool(cell->getPort("\\A"));
+ string name_en = get_bool(cell->getPort("\\EN"));
+ decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool (or %s (not %s))) ; %s\n",
+ log_id(module), idcounter, log_id(module), name_a.c_str(), name_en.c_str(), log_id(cell)));
+ if (cell->type == "$assert")
+ assert_list.push_back(idcounter++);
+ else
+ assume_list.push_back(idcounter++);
+ }
+
+ for (int iter = 1; !registers.empty(); iter++)
+ {
+ pool<Cell*> this_regs;
+ this_regs.swap(registers);
+
+ if (verbose) log("=> export logic driving registers [iteration %d]\n", iter);
+
+ for (auto cell : this_regs)
+ {
+ if (cell->type == "$_DFF_P_" || cell->type == "$_DFF_N_")
+ {
+ std::string expr_d = get_bool(cell->getPort("\\D"));
+ std::string expr_q = get_bool(cell->getPort("\\Q"), "next_state");
+ trans.push_back(stringf(" (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), log_id(cell), log_signal(cell->getPort("\\Q"))));
+ }
+
+ if (cell->type == "$dff")
+ {
+ std::string expr_d = get_bv(cell->getPort("\\D"));
+ std::string expr_q = get_bv(cell->getPort("\\Q"), "next_state");
+ trans.push_back(stringf(" (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), log_id(cell), log_signal(cell->getPort("\\Q"))));
+ }
+
+ if (cell->type == "$mem")
+ {
+ int arrayid = memarrays.at(cell);
+
+ int abits = cell->getParam("\\ABITS").as_int();
+ int width = cell->getParam("\\WIDTH").as_int();
+ int wr_ports = cell->getParam("\\WR_PORTS").as_int();
+
+ for (int i = 0; i < wr_ports; i++)
+ {
+ std::string addr = get_bv(cell->getPort("\\WR_ADDR").extract(abits*i, abits));
+ std::string data = get_bv(cell->getPort("\\WR_DATA").extract(width*i, width));
+ std::string mask = get_bv(cell->getPort("\\WR_EN").extract(width*i, width));
+
+ data = stringf("(bvor (bvand %s %s) (bvand (select (|%s#%d#%d| state) %s) (bvnot %s)))",
+ data.c_str(), mask.c_str(), log_id(module), arrayid, i, addr.c_str(), mask.c_str());
+
+ decls.push_back(stringf("(define-fun |%s#%d#%d| ((state |%s_s|)) (Array (_ BitVec %d) (_ BitVec %d)) "
+ "(store (|%s#%d#%d| state) %s %s)) ; %s\n",
+ log_id(module), arrayid, i+1, log_id(module), abits, width,
+ log_id(module), arrayid, i, addr.c_str(), data.c_str(), log_id(cell)));
+ }
+
+ std::string expr_d = stringf("(|%s#%d#%d| state)", log_id(module), arrayid, wr_ports);
+ std::string expr_q = stringf("(|%s#%d#0| next_state)", log_id(module), arrayid);
+ trans.push_back(stringf(" (= %s %s) ; %s\n", expr_d.c_str(), expr_q.c_str(), log_id(cell)));
+ }
+ }
+ }
+
+ string assert_expr = assert_list.empty() ? "true" : "(and";
+ if (!assert_list.empty()) {
+ for (int i : assert_list)
+ assert_expr += stringf(" (|%s#%d| state)", log_id(module), i);
+ assert_expr += ")";
+ }
+ decls.push_back(stringf("(define-fun |%s_a| ((state |%s_s|)) Bool %s)\n",
+ log_id(module), log_id(module), assert_expr.c_str()));
+
+ string assume_expr = assume_list.empty() ? "true" : "(and";
+ if (!assume_list.empty()) {
+ for (int i : assume_list)
+ assume_expr += stringf(" (|%s#%d| state)", log_id(module), i);
+ assume_expr += ")";
+ }
+ decls.push_back(stringf("(define-fun |%s_u| ((state |%s_s|)) Bool %s)\n",
+ log_id(module), log_id(module), assume_expr.c_str()));
+
+ string init_expr = init_list.empty() ? "true" : "(and";
+ if (!init_list.empty()) {
+ for (auto &str : init_list)
+ init_expr += stringf("\n\t%s", str.c_str());
+ init_expr += "\n)";
+ }
+ decls.push_back(stringf("(define-fun |%s_i| ((state |%s_s|)) Bool %s)\n",
+ log_id(module), log_id(module), init_expr.c_str()));
}
void write(std::ostream &f)
@@ -412,6 +631,7 @@ struct Smt2Worker
for (auto it : decls)
f << it;
+ f << stringf("; yosys-smt2-module %s\n", log_id(module));
f << stringf("(define-fun |%s_t| ((state |%s_s|) (next_state |%s_s|)) Bool ", log_id(module), log_id(module), log_id(module));
if (GetSize(trans) > 1) {
f << "(and\n";
@@ -436,8 +656,8 @@ struct Smt2Backend : public Backend {
log(" write_smt2 [options] [filename]\n");
log("\n");
log("Write a SMT-LIBv2 [1] description of the current design. For a module with name\n");
- log("'<mod>' this will declare the sort '<mod>_s' (state of the module) and the the\n");
- log("function '<mod>_t' (state transition function).\n");
+ log("'<mod>' this will declare the sort '<mod>_s' (state of the module) and the\n");
+ log("functions operating on that state.\n");
log("\n");
log("The '<mod>_s' sort represents a module state. Additional '<mod>_n' functions\n");
log("are provided that can be used to access the values of the signals in the module.\n");
@@ -449,11 +669,37 @@ struct Smt2Backend : public Backend {
log("The '<mod>_t' function evaluates to 'true' when the given pair of states\n");
log("describes a valid state transition.\n");
log("\n");
+ log("The '<mod>_a' function evaluates to 'true' when the given state satisfies\n");
+ log("the asserts in the module.\n");
+ log("\n");
+ log("The '<mod>_u' function evaluates to 'true' when the given state satisfies\n");
+ log("the assumptions in the module.\n");
+ log("\n");
+ log("The '<mod>_i' function evaluates to 'true' when the given state conforms\n");
+ log("to the initial state.\n");
+ log("\n");
+ log(" -verbose\n");
+ log(" this will print the recursive walk used to export the modules.\n");
+ log("\n");
log(" -bv\n");
log(" enable support for BitVec (FixedSizeBitVectors theory). with this\n");
log(" option set multi-bit wires are represented using the BitVec sort and\n");
log(" support for coarse grain cells (incl. arithmetic) is enabled.\n");
log("\n");
+ log(" -mem\n");
+ log(" enable support for memories (via ArraysEx theory). this option\n");
+ log(" also implies -bv. only $mem cells without merged registers in\n");
+ log(" read ports are supported. call \"memory\" with -nordff to make sure\n");
+ log(" that no registers are merged into $mem read ports. '<mod>_m' functions\n");
+ log(" will be generated for accessing the arrays that are used to represent\n");
+ log(" memories.\n");
+ log("\n");
+ log(" -regs\n");
+ log(" also create '<mod>_n' functions for all registers.\n");
+ log("\n");
+ log(" -wires\n");
+ log(" also create '<mod>_n' functions for all public wires.\n");
+ log("\n");
log(" -tpl <template_file>\n");
log(" use the given template file. the line containing only the token '%%%%'\n");
log(" is replaced with the regular output of this command.\n");
@@ -500,7 +746,7 @@ struct Smt2Backend : public Backend {
log("The following yosys script will create a 'test.smt2' file for our proof:\n");
log("\n");
log(" read_verilog test.v\n");
- log(" hierarchy; proc; techmap; opt -fast\n");
+ log(" hierarchy -check; proc; opt; check -assert\n");
log(" write_smt2 -bv -tpl test.tpl test.smt2\n");
log("\n");
log("Running 'cvc4 test.smt2' will print 'unsat' because y can never transition\n");
@@ -510,9 +756,9 @@ struct Smt2Backend : public Backend {
virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
{
std::ifstream template_f;
- bool bvmode = false;
+ bool bvmode = false, memmode = false, regsmode = false, wiresmode = false, verbose = false;
- log_header("Executing SMT2 backend.\n");
+ log_header(design, "Executing SMT2 backend.\n");
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++)
@@ -527,6 +773,23 @@ struct Smt2Backend : public Backend {
bvmode = true;
continue;
}
+ if (args[argidx] == "-mem") {
+ bvmode = true;
+ memmode = true;
+ continue;
+ }
+ if (args[argidx] == "-regs") {
+ regsmode = true;
+ continue;
+ }
+ if (args[argidx] == "-wires") {
+ wiresmode = true;
+ continue;
+ }
+ if (args[argidx] == "-verbose") {
+ verbose = true;
+ continue;
+ }
break;
}
extra_args(f, filename, args, argidx);
@@ -552,7 +815,7 @@ struct Smt2Backend : public Backend {
log("Creating SMT-LIBv2 representation of module %s.\n", log_id(module));
- Smt2Worker worker(module, bvmode);
+ Smt2Worker worker(module, bvmode, memmode, regsmode, wiresmode, verbose);
worker.run();
worker.write(*f);
}
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
new file mode 100644
index 000000000..f2911b3e7
--- /dev/null
+++ b/backends/smt2/smtbmc.py
@@ -0,0 +1,225 @@
+#!/usr/bin/env python3
+#
+# 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
+# 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.
+#
+
+import os, sys, getopt, re
+##yosys-sys-path##
+from smtio import smtio, smtopts, mkvcd
+
+skip_steps = 0
+step_size = 1
+num_steps = 20
+vcdfile = None
+tempind = False
+assume_skipped = None
+topmod = None
+so = smtopts()
+
+
+def usage():
+ print("""
+yosys-smtbmc [options] <yosys_smt2_output>
+
+ -t <num_steps>, -t <skip_steps>:<num_steps>
+ default: skip_steps=0, num_steps=20
+
+ -u <start_step>
+ assume asserts in skipped steps in BMC
+
+ -S <step_size>
+ proof <step_size> time steps at once
+
+ -c <vcd_filename>
+ write counter-example to this VCD file
+ (hint: use 'write_smt2 -wires' for maximum
+ coverage of signals in generated VCD file)
+
+ -i
+ instead of BMC run temporal induction
+
+ -m <module_name>
+ name of the top module
+""" + so.helpmsg())
+ sys.exit(1)
+
+
+try:
+ opts, args = getopt.getopt(sys.argv[1:], so.optstr + "t:u:S:c:im:")
+except:
+ usage()
+
+for o, a in opts:
+ if o == "-t":
+ match = re.match(r"(\d+):(.*)", a)
+ if match:
+ skip_steps = int(match.group(1))
+ num_steps = int(match.group(2))
+ else:
+ num_steps = int(a)
+ elif o == "-u":
+ assume_skipped = int(a)
+ elif o == "-S":
+ step_size = int(a)
+ elif o == "-c":
+ vcdfile = a
+ elif o == "-i":
+ tempind = True
+ elif o == "-m":
+ topmod = a
+ elif so.handle(o, a):
+ pass
+ else:
+ usage()
+
+if len(args) != 1:
+ usage()
+
+
+smt = smtio(opts=so)
+
+print("%s Solver: %s" % (smt.timestamp(), so.solver))
+smt.setup("QF_AUFBV")
+
+debug_nets = set()
+debug_nets_re = re.compile(r"^; yosys-smt2-(input|output|register|wire) (\S+) (\d+)")
+
+with open(args[0], "r") as f:
+ for line in f:
+ match = debug_nets_re.match(line)
+ if match:
+ debug_nets.add(match.group(2))
+ if line.startswith("; yosys-smt2-module") and topmod is None:
+ topmod = line.split()[2]
+ smt.write(line)
+
+assert topmod is not None
+
+
+def write_vcd_model(steps):
+ print("%s Writing model to VCD file." % smt.timestamp())
+
+ vcd = mkvcd(open(vcdfile, "w"))
+ for netname in sorted(debug_nets):
+ width = len(smt.get_net_bin(topmod, netname, "s0"))
+ vcd.add_net(netname, width)
+
+ for i in range(steps):
+ vcd.set_time(i)
+ for netname in debug_nets:
+ vcd.set_net(netname, smt.get_net_bin(topmod, netname, "s%d" % i))
+
+ vcd.set_time(steps)
+
+
+if tempind:
+ retstatus = False
+ skip_counter = step_size
+ for step in range(num_steps, -1, -1):
+ smt.write("(declare-fun s%d () %s_s)" % (step, topmod))
+ smt.write("(assert (%s_u s%d))" % (topmod, step))
+
+ if step == num_steps:
+ smt.write("(assert (not (%s_a s%d)))" % (topmod, step))
+
+ else:
+ smt.write("(assert (%s_t s%d s%d))" % (topmod, step, step+1))
+ smt.write("(assert (%s_a s%d))" % (topmod, step))
+
+ if step > num_steps-skip_steps:
+ print("%s Skipping induction in step %d.." % (smt.timestamp(), step))
+ continue
+
+ skip_counter += 1
+ if skip_counter < step_size:
+ print("%s Skipping induction in step %d.." % (smt.timestamp(), step))
+ continue
+
+ skip_counter = 0
+ print("%s Trying induction in step %d.." % (smt.timestamp(), step))
+
+ if smt.check_sat() == "sat":
+ if step == 0:
+ print("%s Temporal induction failed!" % smt.timestamp())
+ if vcdfile is not None:
+ write_vcd_model(num_steps+1)
+
+ else:
+ print("%s Temporal induction successful." % smt.timestamp())
+ retstatus = True
+ break
+
+
+else: # not tempind
+ step = 0
+ retstatus = True
+ while step < num_steps:
+ smt.write("(declare-fun s%d () %s_s)" % (step, topmod))
+ smt.write("(assert (%s_u s%d))" % (topmod, step))
+
+ if step == 0:
+ smt.write("(assert (%s_i s0))" % (topmod))
+
+ else:
+ smt.write("(assert (%s_t s%d s%d))" % (topmod, step-1, step))
+
+ if step < skip_steps:
+ if assume_skipped is not None and step >= assume_skipped:
+ print("%s Skipping step %d (and assuming pass).." % (smt.timestamp(), step))
+ smt.write("(assert (%s_a s%d))" % (topmod, step))
+ else:
+ print("%s Skipping step %d.." % (smt.timestamp(), step))
+ step += 1
+ continue
+
+ last_check_step = step
+ for i in range(1, step_size):
+ if step+i < num_steps:
+ smt.write("(declare-fun s%d () %s_s)" % (step+i, topmod))
+ smt.write("(assert (%s_u s%d))" % (topmod, step+i))
+ smt.write("(assert (%s_t s%d s%d))" % (topmod, step+i-1, step+i))
+ last_check_step = step+i
+
+ if last_check_step == step:
+ print("%s Checking asserts in step %d.." % (smt.timestamp(), step))
+ else:
+ print("%s Checking asserts in steps %d to %d.." % (smt.timestamp(), step, last_check_step))
+ smt.write("(push 1)")
+
+ smt.write("(assert (not (and %s)))" % " ".join(["(%s_a s%d)" % (topmod, i) for i in range(step, last_check_step+1)]))
+
+ if smt.check_sat() == "sat":
+ print("%s BMC failed!" % smt.timestamp())
+ if vcdfile is not None:
+ write_vcd_model(step+step_size)
+ retstatus = False
+ break
+
+ else: # unsat
+ smt.write("(pop 1)")
+ for i in range(step, last_check_step+1):
+ smt.write("(assert (%s_a s%d))" % (topmod, i))
+
+ step += step_size
+
+
+smt.write("(exit)")
+smt.wait()
+
+print("%s Status: %s" % (smt.timestamp(), "PASSED" if retstatus else "FAILED (!)"))
+sys.exit(0 if retstatus else 1)
+
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
new file mode 100644
index 000000000..6e8bded77
--- /dev/null
+++ b/backends/smt2/smtio.py
@@ -0,0 +1,325 @@
+#!/usr/bin/env python3
+#
+# 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
+# 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.
+#
+
+import sys
+import subprocess
+from select import select
+from time import time
+
+class smtio:
+ def __init__(self, solver=None, debug_print=None, debug_file=None, timeinfo=None, opts=None):
+ if opts is not None:
+ self.solver = opts.solver
+ self.debug_print = opts.debug_print
+ self.debug_file = opts.debug_file
+ self.timeinfo = opts.timeinfo
+
+ else:
+ self.solver = "z3"
+ self.debug_print = False
+ self.debug_file = None
+ self.timeinfo = True
+
+ if solver is not None:
+ self.solver = solver
+
+ if debug_print is not None:
+ self.debug_print = debug_print
+
+ if debug_file is not None:
+ self.debug_file = debug_file
+
+ if timeinfo is not None:
+ self.timeinfo = timeinfo
+
+ if self.solver == "yices":
+ popen_vargs = ['yices-smt2', '--incremental']
+
+ if self.solver == "z3":
+ popen_vargs = ['z3', '-smt2', '-in']
+
+ if self.solver == "cvc4":
+ popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2']
+
+ if self.solver == "mathsat":
+ popen_vargs = ['mathsat']
+
+ self.p = subprocess.Popen(popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
+ self.start_time = time()
+
+ def setup(self, logic="ALL", info=None):
+ self.write("(set-logic %s)" % logic)
+ if info is not None:
+ self.write("(set-info :source |%s|)" % info)
+ self.write("(set-info :smt-lib-version 2.5)")
+ self.write("(set-info :category \"industrial\")")
+
+ def timestamp(self):
+ secs = int(time() - self.start_time)
+ return "## %6d %3d:%02d:%02d " % (secs, secs // (60*60), (secs // 60) % 60, secs % 60)
+
+ def write(self, stmt):
+ stmt = stmt.strip()
+ if self.debug_print:
+ print("> %s" % stmt)
+ if self.debug_file:
+ print(stmt, file=self.debug_file)
+ self.debug_file.flush()
+ self.p.stdin.write(bytes(stmt + "\n", "ascii"))
+ self.p.stdin.flush()
+
+ def read(self):
+ stmt = []
+ count_brackets = 0
+
+ while True:
+ line = self.p.stdout.readline().decode("ascii").strip()
+ count_brackets += line.count("(")
+ count_brackets -= line.count(")")
+ stmt.append(line)
+ if self.debug_print:
+ print("< %s" % line)
+ if count_brackets == 0:
+ break
+ if not self.p.poll():
+ print("SMT Solver terminated unexpectedly: %s" % "".join(stmt))
+ sys.exit(1)
+
+ stmt = "".join(stmt)
+ if stmt.startswith("(error"):
+ print("SMT Solver Error: %s" % stmt, file=sys.stderr)
+ sys.exit(1)
+
+ return stmt
+
+ def check_sat(self):
+ if self.debug_print:
+ print("> (check-sat)")
+ if self.debug_file:
+ print("; running check-sat..", file=self.debug_file)
+ self.debug_file.flush()
+
+ self.p.stdin.write(bytes("(check-sat)\n", "ascii"))
+ self.p.stdin.flush()
+
+ if self.timeinfo:
+ i = 0
+ s = "/-\|"
+
+ count = 0
+ num_bs = 0
+ while select([self.p.stdout], [], [], 0.1) == ([], [], []):
+ count += 1
+
+ if count < 25:
+ continue
+
+ if count % 10 == 0 or count == 25:
+ secs = count // 10
+
+ if secs < 60:
+ m = "(%d seconds)" % secs
+ elif secs < 60*60:
+ m = "(%d seconds -- %d:%02d)" % (secs, secs // 60, secs % 60)
+ else:
+ m = "(%d seconds -- %d:%02d:%02d)" % (secs, secs // (60*60), (secs // 60) % 60, secs % 60)
+
+ print("%s %s %c" % ("\b \b" * num_bs, m, s[i]), end="", file=sys.stderr)
+ num_bs = len(m) + 3
+
+ else:
+ print("\b" + s[i], end="", file=sys.stderr)
+
+ sys.stderr.flush()
+ i = (i + 1) % len(s)
+
+ if num_bs != 0:
+ print("\b \b" * num_bs, end="", file=sys.stderr)
+ sys.stderr.flush()
+
+ result = self.read()
+ if self.debug_file:
+ print("(set-info :status %s)" % result, file=self.debug_file)
+ print("(check-sat)", file=self.debug_file)
+ self.debug_file.flush()
+ return result
+
+ def parse(self, stmt):
+ def worker(stmt):
+ if stmt[0] == '(':
+ expr = []
+ cursor = 1
+ while stmt[cursor] != ')':
+ el, le = worker(stmt[cursor:])
+ expr.append(el)
+ cursor += le
+ return expr, cursor+1
+
+ if stmt[0] == '|':
+ expr = "|"
+ cursor = 1
+ while stmt[cursor] != '|':
+ expr += stmt[cursor]
+ cursor += 1
+ expr += "|"
+ return expr, cursor+1
+
+ if stmt[0] in [" ", "\t", "\r", "\n"]:
+ el, le = worker(stmt[1:])
+ return el, le+1
+
+ expr = ""
+ cursor = 0
+ while stmt[cursor] not in ["(", ")", "|", " ", "\t", "\r", "\n"]:
+ expr += stmt[cursor]
+ cursor += 1
+ return expr, cursor
+ return worker(stmt)[0]
+
+ def bv2hex(self, v):
+ h = ""
+ v = bv2bin(v)
+ while len(v) > 0:
+ d = 0
+ if len(v) > 0 and v[-1] == "1": d += 1
+ if len(v) > 1 and v[-2] == "1": d += 2
+ if len(v) > 2 and v[-3] == "1": d += 4
+ if len(v) > 3 and v[-4] == "1": d += 8
+ h = hex(d)[2:] + h
+ if len(v) < 4: break
+ v = v[:-4]
+ return h
+
+ def bv2bin(self, v):
+ if v == "true": return "1"
+ if v == "false": return "0"
+ if v.startswith("#b"):
+ return v[2:]
+ if v.startswith("#x"):
+ digits = []
+ for d in v[2:]:
+ if d == "0": digits.append("0000")
+ if d == "1": digits.append("0001")
+ if d == "2": digits.append("0010")
+ if d == "3": digits.append("0011")
+ if d == "4": digits.append("0100")
+ if d == "5": digits.append("0101")
+ if d == "6": digits.append("0110")
+ if d == "7": digits.append("0111")
+ if d == "8": digits.append("1000")
+ if d == "9": digits.append("1001")
+ if d in ("a", "A"): digits.append("1010")
+ if d in ("b", "B"): digits.append("1011")
+ if d in ("c", "C"): digits.append("1100")
+ if d in ("d", "D"): digits.append("1101")
+ if d in ("e", "E"): digits.append("1110")
+ if d in ("f", "F"): digits.append("1111")
+ return "".join(digits)
+ assert False
+
+ def get(self, expr):
+ self.write("(get-value (%s))" % (expr))
+ return self.parse(self.read())[0][1]
+
+ def get_net(self, mod_name, net_name, state_name):
+ return self.get("(|%s_n %s| %s)" % (mod_name, net_name, state_name))
+
+ def get_net_bool(self, mod_name, net_name, state_name):
+ v = self.get_net(mod_name, net_name, state_name)
+ assert v in ["true", "false"]
+ return 1 if v == "true" else 0
+
+ def get_net_hex(self, mod_name, net_name, state_name):
+ return self.bv2hex(self.get_net(mod_name, net_name, state_name))
+
+ def get_net_bin(self, mod_name, net_name, state_name):
+ return self.bv2bin(self.get_net(mod_name, net_name, state_name))
+
+ def wait(self):
+ self.p.wait()
+
+
+class smtopts:
+ def __init__(self):
+ self.optstr = "s:d:vp"
+ self.solver = "z3"
+ self.debug_print = False
+ self.debug_file = None
+ self.timeinfo = True
+
+ def handle(self, o, a):
+ if o == "-s":
+ self.solver = a
+ elif o == "-v":
+ self.debug_print = True
+ elif o == "-p":
+ self.timeinfo = True
+ elif o == "-d":
+ self.debug_file = open(a, "w")
+ else:
+ return False
+ return True
+
+ def helpmsg(self):
+ return """
+ -s <solver>
+ set SMT solver: z3, cvc4, yices, mathsat
+ default: z3
+
+ -v
+ enable debug output
+
+ -p
+ disable timer display during solving
+
+ -d <filename>
+ write smt2 statements to file
+"""
+
+
+class mkvcd:
+ def __init__(self, f):
+ self.f = f
+ self.t = -1
+ self.nets = dict()
+
+ def add_net(self, name, width):
+ assert self.t == -1
+ key = "n%d" % len(self.nets)
+ self.nets[name] = (key, width)
+
+ def set_net(self, name, bits):
+ assert name in self.nets
+ assert self.t >= 0
+ print("b%s %s" % (bits, self.nets[name][0]), file=self.f)
+
+ def set_time(self, t):
+ assert t >= self.t
+ if t != self.t:
+ if self.t == -1:
+ print("$var event 1 ! smt_clock $end", file=self.f)
+ for name in sorted(self.nets):
+ key, width = self.nets[name]
+ print("$var wire %d %s %s $end" % (width, key, name), file=self.f)
+ print("$enddefinitions $end", file=self.f)
+ self.t = t
+ assert self.t >= 0
+ print("#%d" % self.t, file=self.f)
+ print("1!", file=self.f)
+
diff --git a/backends/smv/Makefile.inc b/backends/smv/Makefile.inc
new file mode 100644
index 000000000..66c192d80
--- /dev/null
+++ b/backends/smv/Makefile.inc
@@ -0,0 +1,3 @@
+
+OBJS += backends/smv/smv.o
+
diff --git a/backends/smv/smv.cc b/backends/smv/smv.cc
new file mode 100644
index 000000000..162ce4906
--- /dev/null
+++ b/backends/smv/smv.cc
@@ -0,0 +1,784 @@
+/*
+ * 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
+ * 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/rtlil.h"
+#include "kernel/register.h"
+#include "kernel/sigtools.h"
+#include "kernel/celltypes.h"
+#include "kernel/log.h"
+#include <string>
+
+USING_YOSYS_NAMESPACE
+PRIVATE_NAMESPACE_BEGIN
+
+struct SmvWorker
+{
+ CellTypes ct;
+ SigMap sigmap;
+ RTLIL::Module *module;
+ std::ostream &f;
+ bool verbose;
+
+ int idcounter;
+ dict<IdString, shared_str> idcache;
+ pool<shared_str> used_names;
+ vector<shared_str> strbuf;
+
+ pool<Wire*> partial_assignment_wires;
+ dict<SigBit, std::pair<const char*, int>> partial_assignment_bits;
+ vector<string> assignments, invarspecs;
+
+ const char *cid()
+ {
+ while (true) {
+ shared_str s(stringf("_%d", idcounter++));
+ if (!used_names.count(s)) {
+ used_names.insert(s);
+ return s.c_str();
+ }
+ }
+ }
+
+ const char *cid(IdString id, bool precache = false)
+ {
+ if (!idcache.count(id))
+ {
+ string name = stringf("_%s", id.c_str());
+
+ if (name.substr(0, 2) == "_\\")
+ name = "_" + name.substr(2);
+
+ for (auto &c : name) {
+ if (c == '|' || c == '$' || c == '_') continue;
+ if (c >= 'a' && c <='z') continue;
+ if (c >= 'A' && c <='Z') continue;
+ if (c >= '0' && c <='9') continue;
+ if (precache) return nullptr;
+ c = '#';
+ }
+
+ if (name == "_main")
+ name = "main";
+
+ while (used_names.count(name))
+ name += "_";
+
+ shared_str s(name);
+ used_names.insert(s);
+ idcache[id] = s;
+ }
+
+ return idcache.at(id).c_str();
+ }
+
+ SmvWorker(RTLIL::Module *module, bool verbose, std::ostream &f) :
+ ct(module->design), sigmap(module), module(module), f(f), verbose(verbose), idcounter(0)
+ {
+ for (auto mod : module->design->modules())
+ cid(mod->name, true);
+
+ for (auto wire : module->wires())
+ cid(wire->name, true);
+
+ for (auto cell : module->cells()) {
+ cid(cell->name, true);
+ cid(cell->type, true);
+ for (auto &conn : cell->connections())
+ cid(conn.first, true);
+ }
+ }
+
+ const char *rvalue(SigSpec sig, int width = -1, bool is_signed = false)
+ {
+ string s;
+ int count_chunks = 0;
+ sigmap.apply(sig);
+
+ for (int i = 0; i < GetSize(sig); i++)
+ if (partial_assignment_bits.count(sig[i]))
+ {
+ int width = 1;
+ const auto &bit_a = partial_assignment_bits.at(sig[i]);
+
+ while (i+width < GetSize(sig))
+ {
+ if (!partial_assignment_bits.count(sig[i+width]))
+ break;
+
+ const auto &bit_b = partial_assignment_bits.at(sig[i+width]);
+ if (strcmp(bit_a.first, bit_b.first))
+ break;
+ if (bit_a.second+width != bit_b.second)
+ break;
+
+ width++;
+ }
+
+ if (i+width < GetSize(sig))
+ s = stringf("%s :: ", rvalue(sig.extract(i+width, GetSize(sig)-(width+i))));
+
+ s += stringf("%s[%d:%d]", bit_a.first, bit_a.second+width-1, bit_a.second);
+
+ if (i > 0)
+ s += stringf(" :: %s", rvalue(sig.extract(0, i)));
+
+ count_chunks = 3;
+ goto continue_with_resize;
+ }
+
+ for (auto &c : sig.chunks()) {
+ count_chunks++;
+ if (!s.empty())
+ s = " :: " + s;
+ if (c.wire) {
+ if (c.offset != 0 || c.width != c.wire->width)
+ s = stringf("%s[%d:%d]", cid(c.wire->name), c.offset+c.width-1, c.offset) + s;
+ else
+ s = cid(c.wire->name) + s;
+ } else {
+ string v = stringf("0ub%d_", c.width);
+ for (int i = c.width-1; i >= 0; i--)
+ v += c.data.at(i) == State::S1 ? '1' : '0';
+ s = v + s;
+ }
+ }
+
+ continue_with_resize:;
+ if (width >= 0) {
+ if (is_signed) {
+ if (GetSize(sig) > width)
+ s = stringf("signed(resize(%s, %d))", s.c_str(), width);
+ else
+ s = stringf("resize(signed(%s), %d)", s.c_str(), width);
+ } else
+ s = stringf("resize(%s, %d)", s.c_str(), width);
+ } else if (is_signed)
+ s = stringf("signed(%s)", s.c_str());
+ else if (count_chunks > 1)
+ s = stringf("(%s)", s.c_str());
+
+ strbuf.push_back(s);
+ return strbuf.back().c_str();
+ }
+
+ const char *rvalue_u(SigSpec sig, int width = -1)
+ {
+ return rvalue(sig, width, false);
+ }
+
+ const char *rvalue_s(SigSpec sig, int width = -1, bool is_signed = true)
+ {
+ return rvalue(sig, width, is_signed);
+ }
+
+ const char *lvalue(SigSpec sig)
+ {
+ sigmap.apply(sig);
+
+ if (sig.is_wire())
+ return rvalue(sig);
+
+ const char *temp_id = cid();
+ f << stringf(" %s : unsigned word[%d]; -- %s\n", temp_id, GetSize(sig), log_signal(sig));
+
+ int offset = 0;
+ for (auto bit : sig) {
+ log_assert(bit.wire != nullptr);
+ partial_assignment_wires.insert(bit.wire);
+ partial_assignment_bits[bit] = std::pair<const char*, int>(temp_id, offset++);
+ }
+
+ return temp_id;
+ }
+
+ void run()
+ {
+ f << stringf("MODULE %s\n", cid(module->name));
+ f << stringf(" VAR\n");
+
+ for (auto wire : module->wires())
+ {
+ if (SigSpec(wire) != sigmap(wire))
+ partial_assignment_wires.insert(wire);
+
+ f << stringf(" %s : unsigned word[%d]; -- %s\n", cid(wire->name), wire->width, log_id(wire));
+
+ if (wire->attributes.count("\\init"))
+ assignments.push_back(stringf("init(%s) := %s;", lvalue(wire), rvalue(wire->attributes.at("\\init"))));
+ }
+
+ for (auto cell : module->cells())
+ {
+ // FIXME: $slice, $concat, $mem
+
+ if (cell->type.in("$assert"))
+ {
+ SigSpec sig_a = cell->getPort("\\A");
+ SigSpec sig_en = cell->getPort("\\EN");
+
+ invarspecs.push_back(stringf("!bool(%s) | bool(%s);", rvalue(sig_en), rvalue(sig_a)));
+
+ continue;
+ }
+
+ if (cell->type.in("$shl", "$shr", "$sshl", "$sshr", "$shift", "$shiftx"))
+ {
+ SigSpec sig_a = cell->getPort("\\A");
+ SigSpec sig_b = cell->getPort("\\B");
+
+ int width_y = GetSize(cell->getPort("\\Y"));
+ int shift_b_width = GetSize(sig_b);
+ int width_ay = max(GetSize(sig_a), width_y);
+ int width = width_ay;
+
+ for (int i = 1, j = 0;; i <<= 1, j++)
+ if (width_ay < i) {
+ width = i-1;
+ shift_b_width = min(shift_b_width, j);
+ break;
+ }
+
+ bool signed_a = cell->getParam("\\A_SIGNED").as_bool();
+ bool signed_b = cell->getParam("\\B_SIGNED").as_bool();
+ string op = cell->type.in("$shl", "$sshl") ? "<<" : ">>";
+ string expr, expr_a;
+
+ if (cell->type == "$sshr" && signed_a)
+ {
+ expr_a = rvalue_s(sig_a, width);
+ expr = stringf("resize(unsigned(%s %s %s), %d)", expr_a.c_str(), op.c_str(), rvalue(sig_b.extract(0, shift_b_width)), width_y);
+ if (shift_b_width < GetSize(sig_b))
+ expr = stringf("%s != 0ud%d_0 ? (bool(%s) ? !0ud%d_0 : 0ud%d_0) : %s",
+ rvalue(sig_b.extract(shift_b_width, GetSize(sig_b) - shift_b_width)), GetSize(sig_b) - shift_b_width,
+ rvalue(sig_a[GetSize(sig_a)-1]), width_y, width_y, expr.c_str());
+ }
+ else if (cell->type.in("$shift", "$shiftx") && signed_b)
+ {
+ expr_a = rvalue_u(sig_a, width);
+
+ const char *b_shr = rvalue_u(sig_b);
+ const char *b_shl = cid();
+
+ f << stringf(" %s : unsigned word[%d]; -- neg(%s)\n", b_shl, GetSize(sig_b), log_signal(sig_b));
+ assignments.push_back(stringf("%s := unsigned(-%s);", b_shl, rvalue_s(sig_b)));
+
+ string expr_shl = stringf("resize(%s << %s[%d:0], %d)", expr_a.c_str(), b_shl, shift_b_width-1, width_y);
+ string expr_shr = stringf("resize(%s >> %s[%d:0], %d)", expr_a.c_str(), b_shr, shift_b_width-1, width_y);
+
+ if (shift_b_width < GetSize(sig_b)) {
+ expr_shl = stringf("%s[%d:%d] != 0ud%d_0 ? 0ud%d_0 : %s", b_shl, GetSize(sig_b)-1, shift_b_width,
+ GetSize(sig_b)-shift_b_width, width_y, expr_shl.c_str());
+ expr_shr = stringf("%s[%d:%d] != 0ud%d_0 ? 0ud%d_0 : %s", b_shr, GetSize(sig_b)-1, shift_b_width,
+ GetSize(sig_b)-shift_b_width, width_y, expr_shr.c_str());
+ }
+
+ expr = stringf("bool(%s) ? %s : %s", rvalue(sig_b[GetSize(sig_b)-1]), expr_shl.c_str(), expr_shr.c_str());
+ }
+ else
+ {
+ if (cell->type.in("$shift", "$shiftx") || !signed_a)
+ expr_a = rvalue_u(sig_a, width);
+ else
+ expr_a = stringf("resize(unsigned(%s), %d)", rvalue_s(sig_a, width_ay), width);
+
+ expr = stringf("resize(%s %s %s[%d:0], %d)", expr_a.c_str(), op.c_str(), rvalue_u(sig_b), shift_b_width-1, width_y);
+ if (shift_b_width < GetSize(sig_b))
+ expr = stringf("%s[%d:%d] != 0ud%d_0 ? 0ud%d_0 : %s", rvalue_u(sig_b), GetSize(sig_b)-1, shift_b_width,
+ GetSize(sig_b)-shift_b_width, width_y, expr.c_str());
+ }
+
+ assignments.push_back(stringf("%s := %s;", lvalue(cell->getPort("\\Y")), expr.c_str()));
+
+ continue;
+ }
+
+ if (cell->type.in("$not", "$pos", "$neg"))
+ {
+ int width = GetSize(cell->getPort("\\Y"));
+ string expr_a, op;
+
+ if (cell->type == "$not") op = "!";
+ if (cell->type == "$pos") op = "";
+ if (cell->type == "$neg") op = "-";
+
+ if (cell->getParam("\\A_SIGNED").as_bool())
+ {
+ assignments.push_back(stringf("%s := unsigned(%s%s);", lvalue(cell->getPort("\\Y")),
+ op.c_str(), rvalue_s(cell->getPort("\\A"), width)));
+ }
+ else
+ {
+ assignments.push_back(stringf("%s := %s%s;", lvalue(cell->getPort("\\Y")),
+ op.c_str(), rvalue_u(cell->getPort("\\A"), width)));
+ }
+
+ continue;
+ }
+
+ if (cell->type.in("$add", "$sub", "$mul", "$and", "$or", "$xor", "$xnor"))
+ {
+ int width = GetSize(cell->getPort("\\Y"));
+ string expr_a, expr_b, op;
+
+ if (cell->type == "$add") op = "+";
+ if (cell->type == "$sub") op = "-";
+ if (cell->type == "$mul") op = "*";
+ if (cell->type == "$and") op = "&";
+ if (cell->type == "$or") op = "|";
+ if (cell->type == "$xor") op = "xor";
+ if (cell->type == "$xnor") op = "xnor";
+
+ if (cell->getParam("\\A_SIGNED").as_bool())
+ {
+ assignments.push_back(stringf("%s := unsigned(%s %s %s);", lvalue(cell->getPort("\\Y")),
+ rvalue_s(cell->getPort("\\A"), width), op.c_str(), rvalue_s(cell->getPort("\\B"), width)));
+ }
+ else
+ {
+ assignments.push_back(stringf("%s := %s %s %s;", lvalue(cell->getPort("\\Y")),
+ rvalue_u(cell->getPort("\\A"), width), op.c_str(), rvalue_u(cell->getPort("\\B"), width)));
+ }
+
+ continue;
+ }
+
+ if (cell->type.in("$div", "$mod"))
+ {
+ int width_y = GetSize(cell->getPort("\\Y"));
+ int width = max(width_y, GetSize(cell->getPort("\\A")));
+ width = max(width, GetSize(cell->getPort("\\B")));
+ string expr_a, expr_b, op;
+
+ if (cell->type == "$div") op = "/";
+ if (cell->type == "$mod") op = "mod";
+
+ if (cell->getParam("\\A_SIGNED").as_bool())
+ {
+ assignments.push_back(stringf("%s := resize(unsigned(%s %s %s), %d);", lvalue(cell->getPort("\\Y")),
+ rvalue_s(cell->getPort("\\A"), width), op.c_str(), rvalue_s(cell->getPort("\\B"), width), width_y));
+ }
+ else
+ {
+ assignments.push_back(stringf("%s := resize(%s %s %s, %d);", lvalue(cell->getPort("\\Y")),
+ rvalue_u(cell->getPort("\\A"), width), op.c_str(), rvalue_u(cell->getPort("\\B"), width), width_y));
+ }
+
+ continue;
+ }
+
+ if (cell->type.in("$eq", "$ne", "$eqx", "$nex", "$lt", "$le", "$ge", "$gt"))
+ {
+ int width = max(GetSize(cell->getPort("\\A")), GetSize(cell->getPort("\\B")));
+ string expr_a, expr_b, op;
+
+ if (cell->type == "$eq") op = "=";
+ if (cell->type == "$ne") op = "!=";
+ if (cell->type == "$eqx") op = "=";
+ if (cell->type == "$nex") op = "!=";
+ if (cell->type == "$lt") op = "<";
+ if (cell->type == "$le") op = "<=";
+ if (cell->type == "$ge") op = ">=";
+ if (cell->type == "$gt") op = ">";
+
+ if (cell->getParam("\\A_SIGNED").as_bool())
+ {
+ expr_a = stringf("resize(signed(%s), %d)", rvalue(cell->getPort("\\A")), width);
+ expr_b = stringf("resize(signed(%s), %d)", rvalue(cell->getPort("\\B")), width);
+ }
+ else
+ {
+ expr_a = stringf("resize(%s, %d)", rvalue(cell->getPort("\\A")), width);
+ expr_b = stringf("resize(%s, %d)", rvalue(cell->getPort("\\B")), width);
+ }
+
+ assignments.push_back(stringf("%s := resize(word1(%s %s %s), %d);", lvalue(cell->getPort("\\Y")),
+ expr_a.c_str(), op.c_str(), expr_b.c_str(), GetSize(cell->getPort("\\Y"))));
+
+ continue;
+ }
+
+ if (cell->type.in("$reduce_and", "$reduce_or", "$reduce_bool"))
+ {
+ int width_a = GetSize(cell->getPort("\\A"));
+ int width_y = GetSize(cell->getPort("\\Y"));
+ const char *expr_a = rvalue(cell->getPort("\\A"));
+ const char *expr_y = lvalue(cell->getPort("\\Y"));
+ string expr;
+
+ if (cell->type == "$reduce_and") expr = stringf("%s = !0ub%d_0", expr_a, width_a);
+ if (cell->type == "$reduce_or") expr = stringf("%s != 0ub%d_0", expr_a, width_a);
+ if (cell->type == "$reduce_bool") expr = stringf("%s != 0ub%d_0", expr_a, width_a);
+
+ assignments.push_back(stringf("%s := resize(word1(%s), %d);", expr_y, expr.c_str(), width_y));
+ continue;
+ }
+
+ if (cell->type.in("$reduce_xor", "$reduce_xnor"))
+ {
+ int width_y = GetSize(cell->getPort("\\Y"));
+ const char *expr_y = lvalue(cell->getPort("\\Y"));
+ string expr;
+
+ for (auto bit : cell->getPort("\\A")) {
+ if (!expr.empty())
+ expr += " xor ";
+ expr += rvalue(bit);
+ }
+
+ if (cell->type == "$reduce_xnor")
+ expr = "!(" + expr + ")";
+
+ assignments.push_back(stringf("%s := resize(%s, %d);", expr_y, expr.c_str(), width_y));
+ continue;
+ }
+
+ if (cell->type.in("$logic_and", "$logic_or"))
+ {
+ int width_a = GetSize(cell->getPort("\\A"));
+ int width_b = GetSize(cell->getPort("\\B"));
+ int width_y = GetSize(cell->getPort("\\Y"));
+
+ string expr_a = stringf("(%s != 0ub%d_0)", rvalue(cell->getPort("\\A")), width_a);
+ string expr_b = stringf("(%s != 0ub%d_0)", rvalue(cell->getPort("\\B")), width_b);
+ const char *expr_y = lvalue(cell->getPort("\\Y"));
+
+ string expr;
+ if (cell->type == "$logic_and") expr = expr_a + " & " + expr_b;
+ if (cell->type == "$logic_or") expr = expr_a + " | " + expr_b;
+
+ assignments.push_back(stringf("%s := resize(word1(%s), %d);", expr_y, expr.c_str(), width_y));
+ continue;
+ }
+
+ if (cell->type.in("$logic_not"))
+ {
+ int width_a = GetSize(cell->getPort("\\A"));
+ int width_y = GetSize(cell->getPort("\\Y"));
+
+ string expr_a = stringf("(%s = 0ub%d_0)", rvalue(cell->getPort("\\A")), width_a);
+ const char *expr_y = lvalue(cell->getPort("\\Y"));
+
+ assignments.push_back(stringf("%s := resize(word1(%s), %d);", expr_y, expr_a.c_str(), width_y));
+ continue;
+ }
+
+ if (cell->type.in("$mux", "$pmux"))
+ {
+ int width = GetSize(cell->getPort("\\Y"));
+ SigSpec sig_a = cell->getPort("\\A");
+ SigSpec sig_b = cell->getPort("\\B");
+ SigSpec sig_s = cell->getPort("\\S");
+
+ string expr;
+ for (int i = 0; i < GetSize(sig_s); i++)
+ expr += stringf("bool(%s) ? %s : ", rvalue(sig_s[i]), rvalue(sig_b.extract(i*width, width)));
+ expr += rvalue(sig_a);
+
+ assignments.push_back(stringf("%s := %s;", lvalue(cell->getPort("\\Y")), expr.c_str()));
+ continue;
+ }
+
+ if (cell->type == "$dff")
+ {
+ assignments.push_back(stringf("next(%s) := %s;", lvalue(cell->getPort("\\Q")), rvalue(cell->getPort("\\D"))));
+ continue;
+ }
+
+ if (cell->type.in("$_BUF_", "$_NOT_"))
+ {
+ string op = cell->type == "$_NOT_" ? "!" : "";
+ assignments.push_back(stringf("%s := %s%s;", lvalue(cell->getPort("\\Y")), op.c_str(), rvalue(cell->getPort("\\A"))));
+ continue;
+ }
+
+ if (cell->type.in("$_AND_", "$_NAND_", "$_OR_", "$_NOR_", "$_XOR_", "$_XNOR_"))
+ {
+ string op;
+
+ if (cell->type.in("$_AND_", "$_NAND_")) op = "&";
+ if (cell->type.in("$_OR_", "$_NOR_")) op = "|";
+ if (cell->type.in("$_XOR_")) op = "xor";
+ if (cell->type.in("$_XNOR_")) op = "xnor";
+
+ if (cell->type.in("$_NAND_", "$_NOR_"))
+ assignments.push_back(stringf("%s := !(%s %s %s);", lvalue(cell->getPort("\\Y")),
+ rvalue(cell->getPort("\\A")), op.c_str(), rvalue(cell->getPort("\\B"))));
+ else
+ assignments.push_back(stringf("%s := %s %s %s;", lvalue(cell->getPort("\\Y")),
+ rvalue(cell->getPort("\\A")), op.c_str(), rvalue(cell->getPort("\\B"))));
+ continue;
+ }
+
+ if (cell->type == "$_MUX_")
+ {
+ assignments.push_back(stringf("%s := bool(%s) ? %s : %s;", lvalue(cell->getPort("\\Y")),
+ rvalue(cell->getPort("\\S")), rvalue(cell->getPort("\\B")), rvalue(cell->getPort("\\A"))));
+ continue;
+ }
+
+ if (cell->type == "$_AOI3_")
+ {
+ assignments.push_back(stringf("%s := !((%s & %s) | %s);", lvalue(cell->getPort("\\Y")),
+ rvalue(cell->getPort("\\A")), rvalue(cell->getPort("\\B")), rvalue(cell->getPort("\\C"))));
+ continue;
+ }
+
+ if (cell->type == "$_OAI3_")
+ {
+ assignments.push_back(stringf("%s := !((%s | %s) & %s);", lvalue(cell->getPort("\\Y")),
+ rvalue(cell->getPort("\\A")), rvalue(cell->getPort("\\B")), rvalue(cell->getPort("\\C"))));
+ continue;
+ }
+
+ if (cell->type == "$_AOI4_")
+ {
+ assignments.push_back(stringf("%s := !((%s & %s) | (%s & %s));", lvalue(cell->getPort("\\Y")),
+ rvalue(cell->getPort("\\A")), rvalue(cell->getPort("\\B")), rvalue(cell->getPort("\\C")), rvalue(cell->getPort("\\D"))));
+ continue;
+ }
+
+ if (cell->type == "$_OAI4_")
+ {
+ assignments.push_back(stringf("%s := !((%s | %s) & (%s | %s));", lvalue(cell->getPort("\\Y")),
+ rvalue(cell->getPort("\\A")), rvalue(cell->getPort("\\B")), rvalue(cell->getPort("\\C")), rvalue(cell->getPort("\\D"))));
+ continue;
+ }
+
+ if (cell->type[0] == '$')
+ log_error("Found currently unsupported cell type %s (%s.%s).\n", log_id(cell->type), log_id(module), log_id(cell));
+
+ f << stringf(" %s : %s;\n", cid(cell->name), cid(cell->type));
+
+ for (auto &conn : cell->connections())
+ if (cell->output(conn.first))
+ assignments.push_back(stringf("%s := %s.%s;", lvalue(conn.second), cid(cell->name), cid(conn.first)));
+ else
+ assignments.push_back(stringf("%s.%s := %s;", cid(cell->name), cid(conn.first), rvalue(conn.second)));
+ }
+
+ for (Wire *wire : partial_assignment_wires)
+ {
+ string expr;
+
+ for (int i = 0; i < wire->width; i++)
+ {
+ if (!expr.empty())
+ expr = " :: " + expr;
+
+ if (partial_assignment_bits.count(sigmap(SigBit(wire, i))))
+ {
+ int width = 1;
+ const auto &bit_a = partial_assignment_bits.at(sigmap(SigBit(wire, i)));
+
+ while (i+1 < wire->width)
+ {
+ SigBit next_bit = sigmap(SigBit(wire, i+1));
+
+ if (!partial_assignment_bits.count(next_bit))
+ break;
+
+ const auto &bit_b = partial_assignment_bits.at(next_bit);
+ if (strcmp(bit_a.first, bit_b.first))
+ break;
+ if (bit_a.second+width != bit_b.second)
+ break;
+
+ width++, i++;
+ }
+
+ expr = stringf("%s[%d:%d]", bit_a.first, bit_a.second+width-1, bit_a.second) + expr;
+ }
+ else if (sigmap(SigBit(wire, i)).wire == nullptr)
+ {
+ string bits;
+ SigSpec sig = sigmap(SigSpec(wire, i));
+
+ while (i+1 < wire->width) {
+ SigBit next_bit = sigmap(SigBit(wire, i+1));
+ if (next_bit.wire != nullptr)
+ break;
+ sig.append(next_bit);
+ i++;
+ }
+
+ for (int k = GetSize(sig)-1; k >= 0; k--)
+ bits += sig[k] == State::S1 ? '1' : '0';
+
+ expr = stringf("0ub%d_%s", GetSize(bits), bits.c_str()) + expr;
+ }
+ else if (sigmap(SigBit(wire, i)) == SigBit(wire, i))
+ {
+ int length = 1;
+
+ while (i+1 < wire->width) {
+ if (partial_assignment_bits.count(sigmap(SigBit(wire, i+1))))
+ break;
+ if (sigmap(SigBit(wire, i+1)) != SigBit(wire, i+1))
+ break;
+ i++, length++;
+ }
+
+ expr = stringf("0ub%d_0", length) + expr;
+ }
+ else
+ {
+ string bits;
+ SigSpec sig = sigmap(SigSpec(wire, i));
+
+ while (i+1 < wire->width) {
+ SigBit next_bit = sigmap(SigBit(wire, i+1));
+ if (next_bit.wire == nullptr || partial_assignment_bits.count(next_bit))
+ break;
+ sig.append(next_bit);
+ i++;
+ }
+
+ expr = rvalue(sig) + expr;
+ }
+ }
+
+ assignments.push_back(stringf("%s := %s;", cid(wire->name), expr.c_str()));
+ }
+
+ if (!assignments.empty()) {
+ f << stringf(" ASSIGN\n");
+ for (const string &line : assignments)
+ f << stringf(" %s\n", line.c_str());
+ }
+
+ if (!invarspecs.empty()) {
+ for (const string &line : invarspecs)
+ f << stringf(" INVARSPEC %s\n", line.c_str());
+ }
+ }
+};
+
+struct SmvBackend : public Backend {
+ SmvBackend() : Backend("smv", "write design to SMV file") { }
+ virtual void help()
+ {
+ // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+ log("\n");
+ log(" write_smv [options] [filename]\n");
+ log("\n");
+ log("Write an SMV description of the current design.\n");
+ log("\n");
+ log(" -verbose\n");
+ log(" this will print the recursive walk used to export the modules.\n");
+ log("\n");
+ log(" -tpl <template_file>\n");
+ log(" use the given template file. the line containing only the token '%%%%'\n");
+ log(" is replaced with the regular output of this command.\n");
+ log("\n");
+ log("THIS COMMAND IS UNDER CONSTRUCTION\n");
+ log("\n");
+ }
+ virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
+ {
+ std::ifstream template_f;
+ bool verbose = false;
+
+ log_header(design, "Executing SMV backend.\n");
+
+ size_t argidx;
+ for (argidx = 1; argidx < args.size(); argidx++)
+ {
+ if (args[argidx] == "-tpl" && argidx+1 < args.size()) {
+ template_f.open(args[++argidx]);
+ if (template_f.fail())
+ log_error("Can't open template file `%s'.\n", args[argidx].c_str());
+ continue;
+ }
+ if (args[argidx] == "-verbose") {
+ verbose = true;
+ continue;
+ }
+ break;
+ }
+ extra_args(f, filename, args, argidx);
+
+ pool<Module*> modules;
+
+ for (auto module : design->modules())
+ if (!module->get_bool_attribute("\\blackbox") && !module->has_memories_warn() && !module->has_processes_warn())
+ modules.insert(module);
+
+ if (template_f.is_open())
+ {
+ std::string line;
+ while (std::getline(template_f, line))
+ {
+ int indent = 0;
+ while (indent < GetSize(line) && (line[indent] == ' ' || line[indent] == '\t'))
+ indent++;
+
+ if (line[indent] == '%')
+ {
+ vector<string> stmt = split_tokens(line);
+
+ if (GetSize(stmt) == 1 && stmt[0] == "%%")
+ break;
+
+ if (GetSize(stmt) == 2 && stmt[0] == "%module")
+ {
+ Module *module = design->module(RTLIL::escape_id(stmt[1]));
+ modules.erase(module);
+
+ if (module == nullptr)
+ log_error("Module '%s' not found.\n", stmt[1].c_str());
+
+ *f << stringf("-- SMV description generated by %s\n", yosys_version_str);
+
+ log("Creating SMV representation of module %s.\n", log_id(module));
+ SmvWorker worker(module, verbose, *f);
+ worker.run();
+
+ *f << stringf("-- end of yosys output\n");
+ continue;
+ }
+
+ log_error("Unknown template statement: '%s'", line.c_str() + indent);
+ }
+
+ *f << line << std::endl;
+ }
+ }
+
+ if (!modules.empty())
+ {
+ *f << stringf("-- SMV description generated by %s\n", yosys_version_str);
+
+ for (auto module : modules) {
+ log("Creating SMV representation of module %s.\n", log_id(module));
+ SmvWorker worker(module, verbose, *f);
+ worker.run();
+ }
+
+ *f << stringf("-- end of yosys output\n");
+ }
+
+ if (template_f.is_open()) {
+ std::string line;
+ while (std::getline(template_f, line))
+ *f << line << std::endl;
+ }
+ }
+} SmvBackend;
+
+PRIVATE_NAMESPACE_END
diff --git a/backends/smv/test_cells.sh b/backends/smv/test_cells.sh
new file mode 100644
index 000000000..63de465c0
--- /dev/null
+++ b/backends/smv/test_cells.sh
@@ -0,0 +1,33 @@
+#!/bin/bash
+
+set -ex
+
+rm -rf test_cells.tmp
+mkdir -p test_cells.tmp
+cd test_cells.tmp
+
+# don't test $mul to reduce runtime
+# don't test $div and $mod to reduce runtime and avoid "div by zero" message
+../../../yosys -p 'test_cell -n 5 -w test all /$alu /$fa /$lcu /$lut /$macc /$mul /$div /$mod'
+
+cat > template.txt << "EOT"
+%module main
+ INVARSPEC ! bool(_trigger);
+EOT
+
+for fn in test_*.il; do
+ ../../../yosys -p "
+ read_ilang $fn
+ rename gold gate
+ synth
+
+ read_ilang $fn
+ miter -equiv -flatten gold gate main
+ hierarchy -top main
+ write_smv -tpl template.txt ${fn#.il}.smv
+ "
+ nuXmv -dynamic ${fn#.il}.smv > ${fn#.il}.out
+done
+
+grep '^-- invariant .* is false' *.out || echo 'All OK.'
+
diff --git a/backends/spice/spice.cc b/backends/spice/spice.cc
index 2c614178b..4101cbf98 100644
--- a/backends/spice/spice.cc
+++ b/backends/spice/spice.cc
@@ -2,11 +2,11 @@
* 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
@@ -27,13 +27,33 @@
USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN
-static void print_spice_net(std::ostream &f, RTLIL::SigBit s, std::string &neg, std::string &pos, std::string &ncpf, int &nc_counter)
+static string spice_id2str(IdString id)
+{
+ static const char *escape_chars = "$\\[]()<>=";
+ string s = RTLIL::unescape_id(id);
+
+ for (auto &ch : s)
+ if (strchr(escape_chars, ch) != nullptr) ch = '_';
+
+ return s;
+}
+
+static string spice_id2str(IdString id, bool use_inames, idict<IdString, 1> &inums)
+{
+ if (!use_inames && *id.c_str() == '$')
+ return stringf("%d", inums(id));
+ return spice_id2str(id);
+}
+
+static void print_spice_net(std::ostream &f, RTLIL::SigBit s, std::string &neg, std::string &pos, std::string &ncpf, int &nc_counter, bool use_inames, idict<IdString, 1> &inums)
{
if (s.wire) {
+ if (s.wire->port_id)
+ use_inames = true;
if (s.wire->width > 1)
- f << stringf(" %s[%d]", RTLIL::id2cstr(s.wire->name), s.offset);
+ f << stringf(" %s.%d", spice_id2str(s.wire->name, use_inames, inums).c_str(), s.offset);
else
- f << stringf(" %s", RTLIL::id2cstr(s.wire->name));
+ f << stringf(" %s", spice_id2str(s.wire->name, use_inames, inums).c_str());
} else {
if (s == RTLIL::State::S0)
f << stringf(" %s", neg.c_str());
@@ -44,9 +64,10 @@ static void print_spice_net(std::ostream &f, RTLIL::SigBit s, std::string &neg,
}
}
-static void print_spice_module(std::ostream &f, RTLIL::Module *module, RTLIL::Design *design, std::string &neg, std::string &pos, std::string &ncpf, bool big_endian)
+static void print_spice_module(std::ostream &f, RTLIL::Module *module, RTLIL::Design *design, std::string &neg, std::string &pos, std::string &ncpf, bool big_endian, bool use_inames)
{
SigMap sigmap(module);
+ idict<IdString, 1> inums;
int cell_counter = 0, conn_counter = 0, nc_counter = 0;
for (auto &cell_it : module->cells_)
@@ -59,7 +80,7 @@ static void print_spice_module(std::ostream &f, RTLIL::Module *module, RTLIL::De
if (design->modules_.count(cell->type) == 0)
{
log_warning("no (blackbox) module for cell type `%s' (%s.%s) found! Guessing order of ports.\n",
- RTLIL::id2cstr(cell->type), RTLIL::id2cstr(module->name), RTLIL::id2cstr(cell->name));
+ log_id(cell->type), log_id(module), log_id(cell));
for (auto &conn : cell->connections()) {
RTLIL::SigSpec sig = sigmap(conn.second);
port_sigs.push_back(sig);
@@ -93,18 +114,18 @@ static void print_spice_module(std::ostream &f, RTLIL::Module *module, RTLIL::De
for (auto &sig : port_sigs) {
for (int i = 0; i < sig.size(); i++) {
RTLIL::SigSpec s = sig.extract(big_endian ? sig.size() - 1 - i : i, 1);
- print_spice_net(f, s, neg, pos, ncpf, nc_counter);
+ print_spice_net(f, s, neg, pos, ncpf, nc_counter, use_inames, inums);
}
}
- f << stringf(" %s\n", RTLIL::id2cstr(cell->type));
+ f << stringf(" %s\n", spice_id2str(cell->type).c_str());
}
for (auto &conn : module->connections())
for (int i = 0; i < conn.first.size(); i++) {
f << stringf("V%d", conn_counter++);
- print_spice_net(f, conn.first.extract(i, 1), neg, pos, ncpf, nc_counter);
- print_spice_net(f, conn.second.extract(i, 1), neg, pos, ncpf, nc_counter);
+ print_spice_net(f, conn.first.extract(i, 1), neg, pos, ncpf, nc_counter, use_inames, inums);
+ print_spice_net(f, conn.second.extract(i, 1), neg, pos, ncpf, nc_counter, use_inames, inums);
f << stringf(" DC 0\n");
}
}
@@ -120,7 +141,7 @@ struct SpiceBackend : public Backend {
log("Write the current design to an SPICE netlist file.\n");
log("\n");
log(" -big_endian\n");
- log(" generate multi-bit ports in MSB first order \n");
+ log(" generate multi-bit ports in MSB first order\n");
log(" (default is LSB first)\n");
log("\n");
log(" -neg net_name\n");
@@ -132,6 +153,10 @@ struct SpiceBackend : public Backend {
log(" -nc_prefix\n");
log(" prefix for not-connected nets (default: _NC)\n");
log("\n");
+ log(" -inames\n");
+ log(" include names of internal ($-prefixed) nets in outputs\n");
+ log(" (default is to use net numbers instead)\n");
+ log("\n");
log(" -top top_module\n");
log(" set the specified module as design top module\n");
log("\n");
@@ -140,10 +165,10 @@ struct SpiceBackend : public Backend {
{
std::string top_module_name;
RTLIL::Module *top_module = NULL;
- bool big_endian = false;
+ bool big_endian = false, use_inames = false;
std::string neg = "Vss", pos = "Vdd", ncpf = "_NC";
- log_header("Executing SPICE backend.\n");
+ log_header(design, "Executing SPICE backend.\n");
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++)
@@ -152,6 +177,10 @@ struct SpiceBackend : public Backend {
big_endian = true;
continue;
}
+ if (args[argidx] == "-inames") {
+ use_inames = true;
+ continue;
+ }
if (args[argidx] == "-neg" && argidx+1 < args.size()) {
neg = args[++argidx];
continue;
@@ -187,9 +216,9 @@ struct SpiceBackend : public Backend {
continue;
if (module->processes.size() != 0)
- log_error("Found unmapped processes in module %s: unmapped processes are not supported in SPICE backend!\n", RTLIL::id2cstr(module->name));
+ log_error("Found unmapped processes in module %s: unmapped processes are not supported in SPICE backend!\n", log_id(module));
if (module->memories.size() != 0)
- log_error("Found munmapped emories in module %s: unmapped memories are not supported in SPICE backend!\n", RTLIL::id2cstr(module->name));
+ log_error("Found unmapped memories in module %s: unmapped memories are not supported in SPICE backend!\n", log_id(module));
if (module->name == RTLIL::escape_id(top_module_name)) {
top_module = module;
@@ -206,24 +235,24 @@ struct SpiceBackend : public Backend {
ports.at(wire->port_id-1) = wire;
}
- *f << stringf(".SUBCKT %s", RTLIL::id2cstr(module->name));
+ *f << stringf(".SUBCKT %s", spice_id2str(module->name).c_str());
for (RTLIL::Wire *wire : ports) {
log_assert(wire != NULL);
if (wire->width > 1) {
for (int i = 0; i < wire->width; i++)
- *f << stringf(" %s[%d]", RTLIL::id2cstr(wire->name), big_endian ? wire->width - 1 - i : i);
+ *f << stringf(" %s.%d", spice_id2str(wire->name).c_str(), big_endian ? wire->width - 1 - i : i);
} else
- *f << stringf(" %s", RTLIL::id2cstr(wire->name));
+ *f << stringf(" %s", spice_id2str(wire->name).c_str());
}
*f << stringf("\n");
- print_spice_module(*f, module, design, neg, pos, ncpf, big_endian);
- *f << stringf(".ENDS %s\n\n", RTLIL::id2cstr(module->name));
+ print_spice_module(*f, module, design, neg, pos, ncpf, big_endian, use_inames);
+ *f << stringf(".ENDS %s\n\n", spice_id2str(module->name).c_str());
}
if (!top_module_name.empty()) {
if (top_module == NULL)
log_error("Can't find top module `%s'!\n", top_module_name.c_str());
- print_spice_module(*f, top_module, design, neg, pos, ncpf, big_endian);
+ print_spice_module(*f, top_module, design, neg, pos, ncpf, big_endian, use_inames);
*f << stringf("\n");
}
diff --git a/backends/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc
index ab0844d72..c5c6b5a08 100644
--- a/backends/verilog/verilog_backend.cc
+++ b/backends/verilog/verilog_backend.cc
@@ -2,11 +2,11 @@
* 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
@@ -17,18 +17,14 @@
*
* ---
*
- * A simple and straightforward verilog backend.
- *
- * Note that RTLIL processes can't always be mapped easily to a Verilog
- * process. Therefore this frontend should only be used to export a
- * Verilog netlist (i.e. after the "proc" pass has converted all processes
- * to logic networks and registers).
+ * A simple and straightforward Verilog backend.
*
*/
#include "kernel/register.h"
#include "kernel/celltypes.h"
#include "kernel/log.h"
+#include "kernel/sigtools.h"
#include <string>
#include <sstream>
#include <set>
@@ -93,16 +89,18 @@ void reset_auto_counter(RTLIL::Module *module)
log(" renaming `%s' to `_%0*d_'.\n", it->first.c_str(), auto_name_digits, auto_name_offset + it->second);
}
+std::string next_auto_id()
+{
+ return stringf("_%0*d_", auto_name_digits, auto_name_offset + auto_name_counter++);
+}
+
std::string id(RTLIL::IdString internal_id, bool may_rename = true)
{
const char *str = internal_id.c_str();
bool do_escape = false;
- if (may_rename && auto_name_map.count(internal_id) != 0) {
- char buffer[100];
- snprintf(buffer, 100, "_%0*d_", auto_name_digits, auto_name_offset + auto_name_map[internal_id]);
- return std::string(buffer);
- }
+ if (may_rename && auto_name_map.count(internal_id) != 0)
+ return stringf("_%0*d_", auto_name_digits, auto_name_offset + auto_name_map[internal_id]);
if (*str == '\\')
str++;
@@ -151,7 +149,7 @@ bool is_reg_wire(RTLIL::SigSpec sig, std::string &reg_name)
return true;
}
-void dump_const(std::ostream &f, const RTLIL::Const &data, int width = -1, int offset = 0, bool no_decimal = false, bool set_signed = false)
+void dump_const(std::ostream &f, const RTLIL::Const &data, int width = -1, int offset = 0, bool no_decimal = false, bool set_signed = false, bool escape_comment = false)
{
if (width < 0)
width = data.bits.size() - offset;
@@ -162,12 +160,13 @@ void dump_const(std::ostream &f, const RTLIL::Const &data, int width = -1, int o
log_assert(i < (int)data.bits.size());
if (data.bits[i] != RTLIL::S0 && data.bits[i] != RTLIL::S1)
goto dump_bits;
- if (data.bits[i] == RTLIL::S1 && (i - offset) == 31)
- goto dump_bits;
if (data.bits[i] == RTLIL::S1)
val |= 1 << (i - offset);
}
- f << stringf("32'%sd %d", set_signed ? "s" : "", val);
+ if (set_signed && val < 0)
+ f << stringf("-32'sd %u", -val);
+ else
+ f << stringf("32'%sd %u", set_signed ? "s" : "", val);
} else {
dump_bits:
f << stringf("%d'%sb", width, set_signed ? "s" : "");
@@ -199,6 +198,8 @@ void dump_const(std::ostream &f, const RTLIL::Const &data, int width = -1, int o
f << stringf("\\\"");
else if (str[i] == '\\')
f << stringf("\\\\");
+ else if (str[i] == '/' && escape_comment && i > 0 && str[i-1] == '*')
+ f << stringf("\\/");
else
f << str[i];
}
@@ -258,7 +259,7 @@ void dump_attributes(std::ostream &f, std::string indent, dict<RTLIL::IdString,
else if (modattr && (it->second == Const(1, 1) || it->second == Const(1)))
f << stringf(" 1 ");
else
- dump_const(f, it->second);
+ dump_const(f, it->second, -1, 0, false, false, attr2comment);
f << stringf(" %s%c", attr2comment ? "*/" : "*)", term);
}
}
@@ -279,7 +280,7 @@ void dump_wire(std::ostream &f, std::string indent, RTLIL::Wire *wire)
f << stringf("[%d:%d] ", wire->width - 1 + wire->start_offset, wire->start_offset);
f << stringf("%s;\n", id(wire->name).c_str());
#else
- // do not use Verilog-2k "outut reg" syntax in verilog export
+ // do not use Verilog-2k "output reg" syntax in Verilog export
std::string range = "";
if (wire->width != 1) {
if (wire->upto)
@@ -293,9 +294,14 @@ void dump_wire(std::ostream &f, std::string indent, RTLIL::Wire *wire)
f << stringf("%s" "output%s %s;\n", indent.c_str(), range.c_str(), id(wire->name).c_str());
if (wire->port_input && wire->port_output)
f << stringf("%s" "inout%s %s;\n", indent.c_str(), range.c_str(), id(wire->name).c_str());
- if (reg_wires.count(wire->name))
+ if (reg_wires.count(wire->name)) {
f << stringf("%s" "reg%s %s;\n", indent.c_str(), range.c_str(), id(wire->name).c_str());
- else if (!wire->port_input && !wire->port_output)
+ if (wire->attributes.count("\\init")) {
+ f << stringf("%s" "initial %s = ", indent.c_str(), id(wire->name).c_str());
+ dump_const(f, wire->attributes.at("\\init"));
+ f << stringf(";\n");
+ }
+ } else if (!wire->port_input && !wire->port_output)
f << stringf("%s" "wire%s %s;\n", indent.c_str(), range.c_str(), id(wire->name).c_str());
#endif
}
@@ -669,6 +675,56 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
return true;
}
+ if (cell->type == "$dffsr")
+ {
+ SigSpec sig_clk = cell->getPort("\\CLK");
+ SigSpec sig_set = cell->getPort("\\SET");
+ SigSpec sig_clr = cell->getPort("\\CLR");
+ SigSpec sig_d = cell->getPort("\\D");
+ SigSpec sig_q = cell->getPort("\\Q");
+
+ int width = cell->parameters["\\WIDTH"].as_int();
+ bool pol_clk = cell->parameters["\\CLK_POLARITY"].as_bool();
+ bool pol_set = cell->parameters["\\SET_POLARITY"].as_bool();
+ bool pol_clr = cell->parameters["\\CLR_POLARITY"].as_bool();
+
+ std::string reg_name = cellname(cell);
+ bool out_is_reg_wire = is_reg_wire(sig_q, reg_name);
+
+ if (!out_is_reg_wire)
+ f << stringf("%s" "reg [%d:0] %s;\n", indent.c_str(), width-1, reg_name.c_str());
+
+ for (int i = 0; i < width; i++) {
+ f << stringf("%s" "always @(%sedge ", indent.c_str(), pol_clk ? "pos" : "neg");
+ dump_sigspec(f, sig_clk);
+ f << stringf(", %sedge ", pol_set ? "pos" : "neg");
+ dump_sigspec(f, sig_set);
+ f << stringf(", %sedge ", pol_clr ? "pos" : "neg");
+ dump_sigspec(f, sig_clr);
+ f << stringf(")\n");
+
+ f << stringf("%s" " if (%s", indent.c_str(), pol_clr ? "" : "!");
+ dump_sigspec(f, sig_clr);
+ f << stringf(") %s[%d] <= 1'b0;\n", reg_name.c_str(), i);
+
+ f << stringf("%s" " else if (%s", indent.c_str(), pol_set ? "" : "!");
+ dump_sigspec(f, sig_set);
+ f << stringf(") %s[%d] <= 1'b1;\n", reg_name.c_str(), i);
+
+ f << stringf("%s" " else %s[%d] <= ", indent.c_str(), reg_name.c_str(), i);
+ dump_sigspec(f, sig_d[i]);
+ f << stringf(";\n");
+ }
+
+ if (!out_is_reg_wire) {
+ f << stringf("%s" "assign ", indent.c_str());
+ dump_sigspec(f, sig_q);
+ f << stringf(" = %s;\n", reg_name.c_str());
+ }
+
+ return true;
+ }
+
if (cell->type == "$dff" || cell->type == "$adff" || cell->type == "$dffe")
{
RTLIL::SigSpec sig_clk, sig_arst, sig_en, val_arst;
@@ -731,8 +787,229 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
return true;
}
+ if (cell->type == "$mem")
+ {
+ RTLIL::IdString memid = cell->parameters["\\MEMID"].decode_string();
+ std::string mem_id = id(cell->parameters["\\MEMID"].decode_string());
+ int abits = cell->parameters["\\ABITS"].as_int();
+ int size = cell->parameters["\\SIZE"].as_int();
+ int width = cell->parameters["\\WIDTH"].as_int();
+ bool use_init = !(RTLIL::SigSpec(cell->parameters["\\INIT"]).is_fully_undef());
+
+ // for memory block make something like:
+ // reg [7:0] memid [3:0];
+ // initial begin
+ // memid[0] <= ...
+ // end
+ f << stringf("%s" "reg [%d:%d] %s [%d:%d];\n", indent.c_str(), width-1, 0, mem_id.c_str(), size-1, 0);
+ if (use_init)
+ {
+ f << stringf("%s" "initial begin\n", indent.c_str());
+ for (int i=0; i<size; i++)
+ {
+ f << stringf("%s" " %s[%d] <= ", indent.c_str(), mem_id.c_str(), i);
+ dump_const(f, cell->parameters["\\INIT"].extract(i*width, width));
+ f << stringf(";\n");
+ }
+ f << stringf("%s" "end\n", indent.c_str());
+ }
+
+ // create a map : "edge clk" -> expressions within that clock domain
+ dict<std::string, std::vector<std::string>> clk_to_lof_body;
+ clk_to_lof_body[""] = std::vector<std::string>();
+ std::string clk_domain_str;
+ // create a list of reg declarations
+ std::vector<std::string> lof_reg_declarations;
+
+ int nread_ports = cell->parameters["\\RD_PORTS"].as_int();
+ RTLIL::SigSpec sig_rd_clk, sig_rd_data, sig_rd_addr;
+ bool use_rd_clk, rd_clk_posedge, rd_transparent;
+ // read ports
+ for (int i=0; i < nread_ports; i++)
+ {
+ sig_rd_clk = cell->getPort("\\RD_CLK").extract(i);
+ sig_rd_data = cell->getPort("\\RD_DATA").extract(i*width, width);
+ sig_rd_addr = cell->getPort("\\RD_ADDR").extract(i*abits, abits);
+ use_rd_clk = cell->parameters["\\RD_CLK_ENABLE"].extract(i).as_bool();
+ rd_clk_posedge = cell->parameters["\\RD_CLK_POLARITY"].extract(i).as_bool();
+ rd_transparent = cell->parameters["\\RD_TRANSPARENT"].extract(i).as_bool();
+ {
+ std::ostringstream os;
+ dump_sigspec(os, sig_rd_clk);
+ clk_domain_str = stringf("%sedge %s", rd_clk_posedge ? "pos" : "neg", os.str().c_str());
+ if( clk_to_lof_body.count(clk_domain_str) == 0 )
+ clk_to_lof_body[clk_domain_str] = std::vector<std::string>();
+ }
+ if (use_rd_clk && !rd_transparent)
+ {
+ // for clocked read ports make something like:
+ // reg [..] temp_id;
+ // always @(posedge clk)
+ // temp_id <= array_reg[r_addr];
+ // assign r_data = temp_id;
+ std::string temp_id = next_auto_id();
+ lof_reg_declarations.push_back( stringf("reg [%d:0] %s;\n", sig_rd_data.size() - 1, temp_id.c_str()) );
+ {
+ std::ostringstream os;
+ dump_sigspec(os, sig_rd_addr);
+ std::string line = stringf("%s <= %s[%s];\n", temp_id.c_str(), mem_id.c_str(), os.str().c_str());
+ clk_to_lof_body[clk_domain_str].push_back(line);
+ }
+ {
+ std::ostringstream os;
+ dump_sigspec(os, sig_rd_data);
+ std::string line = stringf("assign %s = %s;\n", os.str().c_str(), temp_id.c_str());
+ clk_to_lof_body[""].push_back(line);
+ }
+ } else {
+ if (rd_transparent) {
+ // for rd-transparent read-ports make something like:
+ // reg [..] temp_id;
+ // always @(posedge clk)
+ // temp_id <= r_addr;
+ // assign r_data = array_reg[temp_id];
+ std::string temp_id = next_auto_id();
+ lof_reg_declarations.push_back( stringf("reg [%d:0] %s;\n", sig_rd_addr.size() - 1, temp_id.c_str()) );
+ {
+ std::ostringstream os;
+ dump_sigspec(os, sig_rd_addr);
+ std::string line = stringf("%s <= %s;\n", temp_id.c_str(), os.str().c_str());
+ clk_to_lof_body[clk_domain_str].push_back(line);
+ }
+ {
+ std::ostringstream os;
+ dump_sigspec(os, sig_rd_data);
+ std::string line = stringf("assign %s = %s[%s];\n", os.str().c_str(), mem_id.c_str(), temp_id.c_str());
+ clk_to_lof_body[""].push_back(line);
+ }
+ } else {
+ // for non-clocked read-ports make something like:
+ // assign r_data = array_reg[r_addr];
+ std::ostringstream os, os2;
+ dump_sigspec(os, sig_rd_data);
+ dump_sigspec(os2, sig_rd_addr);
+ std::string line = stringf("assign %s = %s[%s];\n", os.str().c_str(), mem_id.c_str(), os2.str().c_str());
+ clk_to_lof_body[""].push_back(line);
+ }
+ }
+ }
+
+ int nwrite_ports = cell->parameters["\\WR_PORTS"].as_int();
+ RTLIL::SigSpec sig_wr_clk, sig_wr_data, sig_wr_addr, sig_wr_en, sig_wr_en_bit;
+ RTLIL::SigBit last_bit;
+ bool wr_clk_posedge;
+ RTLIL::SigSpec lof_wen;
+ dict<RTLIL::SigSpec, int> wen_to_width;
+ SigMap sigmap(active_module);
+ int n, wen_width;
+ // write ports
+ for (int i=0; i < nwrite_ports; i++)
+ {
+ sig_wr_clk = cell->getPort("\\WR_CLK").extract(i);
+ sig_wr_data = cell->getPort("\\WR_DATA").extract(i*width, width);
+ sig_wr_addr = cell->getPort("\\WR_ADDR").extract(i*abits, abits);
+ sig_wr_en = cell->getPort("\\WR_EN").extract(i*width, width);
+ sig_wr_en_bit = sig_wr_en.extract(0);
+ wr_clk_posedge = cell->parameters["\\WR_CLK_POLARITY"].extract(i).as_bool();
+ {
+ std::ostringstream os;
+ dump_sigspec(os, sig_wr_clk);
+ clk_domain_str = stringf("%sedge %s", wr_clk_posedge ? "pos" : "neg", os.str().c_str());
+ if( clk_to_lof_body.count(clk_domain_str) == 0 )
+ clk_to_lof_body[clk_domain_str] = std::vector<std::string>();
+ }
+ // group the wen bits
+ last_bit = sig_wr_en.extract(0);
+ lof_wen = RTLIL::SigSpec(last_bit);
+ wen_to_width.clear();
+ wen_to_width[last_bit] = 0;
+ for (auto &current_bit : sig_wr_en.bits())
+ {
+ if (sigmap(current_bit) == sigmap(last_bit)){
+ wen_to_width[current_bit] += 1;
+ } else {
+ lof_wen.append_bit(current_bit);
+ wen_to_width[current_bit] = 1;
+ }
+ last_bit = current_bit;
+ }
+ // make something like:
+ // always @(posedge clk)
+ // if (wr_en_bit) memid[w_addr][??] <= w_data[??];
+ // ...
+ n = 0;
+ for (auto &wen_bit : lof_wen) {
+ wen_width = wen_to_width[wen_bit];
+ if (!(wen_bit == RTLIL::SigBit(false)))
+ {
+ std::ostringstream os;
+ if (!(wen_bit == RTLIL::SigBit(true)))
+ {
+ os << stringf("if (");
+ dump_sigspec(os, wen_bit);
+ os << stringf(") ");
+ }
+ os << stringf("%s[", mem_id.c_str());
+ dump_sigspec(os, sig_wr_addr);
+ if (wen_width == width)
+ os << stringf("] <= ");
+ else
+ os << stringf("][%d:%d] <= ", n+wen_width-1, n);
+ dump_sigspec(os, sig_wr_data.extract(n, wen_width));
+ os << stringf(";\n");
+ clk_to_lof_body[clk_domain_str].push_back(os.str());
+ }
+ n += wen_width;
+ }
+ }
+ // Output Verilog that looks something like this:
+ // reg [..] _3_;
+ // always @(posedge CLK2) begin
+ // _3_ <= memory[D1ADDR];
+ // if (A1EN)
+ // memory[A1ADDR] <= A1DATA;
+ // if (A2EN)
+ // memory[A2ADDR] <= A2DATA;
+ // ...
+ // end
+ // always @(negedge CLK1) begin
+ // if (C1EN)
+ // memory[C1ADDR] <= C1DATA;
+ // end
+ // ...
+ // assign D1DATA = _3_;
+ // assign D2DATA <= memory[D2ADDR];
+
+ // the reg ... definitions
+ for(auto &reg : lof_reg_declarations)
+ {
+ f << stringf("%s" "%s", indent.c_str(), reg.c_str());
+ }
+ // the block of expressions by clock domain
+ for(auto &pair : clk_to_lof_body)
+ {
+ std::string clk_domain = pair.first;
+ std::vector<std::string> lof_lines = pair.second;
+ if( clk_domain != "")
+ {
+ f << stringf("%s" "always @(%s) begin\n", indent.c_str(), clk_domain.c_str());
+ for(auto &line : lof_lines)
+ f << stringf("%s%s" "%s", indent.c_str(), indent.c_str(), line.c_str());
+ f << stringf("%s" "end\n", indent.c_str());
+ }
+ else
+ {
+ // the non-clocked assignments
+ for(auto &line : lof_lines)
+ f << stringf("%s" "%s", indent.c_str(), line.c_str());
+ }
+ }
+
+ return true;
+ }
+
// FIXME: $_SR_[PN][PN]_, $_DLATCH_[PN]_, $_DLATCHSR_[PN][PN][PN]_
- // FIXME: $sr, $dffsr, $dlatch, $memrd, $memwr, $mem, $fsm
+ // FIXME: $sr, $dlatch, $memrd, $memwr, $fsm
return false;
}
@@ -853,11 +1130,15 @@ void dump_proc_switch(std::ostream &f, std::string indent, RTLIL::SwitchRule *sw
dump_sigspec(f, sw->signal);
f << stringf(")\n");
+ bool got_default = false;
for (auto it = sw->cases.begin(); it != sw->cases.end(); ++it) {
- f << stringf("%s ", indent.c_str());
- if ((*it)->compare.size() == 0)
- f << stringf("default");
- else {
+ if ((*it)->compare.size() == 0) {
+ if (got_default)
+ continue;
+ f << stringf("%s default", indent.c_str());
+ got_default = true;
+ } else {
+ f << stringf("%s ", indent.c_str());
for (size_t i = 0; i < (*it)->compare.size(); i++) {
if (i > 0)
f << stringf(", ");
@@ -962,6 +1243,12 @@ void dump_module(std::ostream &f, std::string indent, RTLIL::Module *module)
reset_auto_counter(module);
active_module = module;
+ if (!module->processes.empty())
+ log_warning("Module %s contains unmapped RTLIL proccesses. RTLIL processes\n"
+ "can't always be mapped directly to Verilog always blocks. Unintended\n"
+ "changes in simulation behavior are possible! Use \"proc\" to convert\n"
+ "processes to logic networks and registers.", log_id(module));
+
f << stringf("\n");
for (auto it = module->processes.begin(); it != module->processes.end(); ++it)
dump_process(f, indent + " ", it->second, true);
@@ -1034,14 +1321,14 @@ void dump_module(std::ostream &f, std::string indent, RTLIL::Module *module)
}
struct VerilogBackend : public Backend {
- VerilogBackend() : Backend("verilog", "write design to verilog file") { }
+ VerilogBackend() : Backend("verilog", "write design to Verilog file") { }
virtual void help()
{
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n");
log(" write_verilog [options] [filename]\n");
log("\n");
- log("Write the current design to a verilog file.\n");
+ log("Write the current design to a Verilog file.\n");
log("\n");
log(" -norename\n");
log(" without this option all internal object names (the ones with a dollar\n");
@@ -1055,7 +1342,7 @@ struct VerilogBackend : public Backend {
log(" with this option attributes are included as comments in the output\n");
log("\n");
log(" -noexpr\n");
- log(" without this option all internal cells are converted to verilog\n");
+ log(" without this option all internal cells are converted to Verilog\n");
log(" expressions.\n");
log("\n");
log(" -blackboxes\n");
@@ -1067,10 +1354,16 @@ struct VerilogBackend : public Backend {
log(" only write selected modules. modules must be selected entirely or\n");
log(" not at all.\n");
log("\n");
+ log("Note that RTLIL processes can't always be mapped directly to Verilog\n");
+ log("always blocks. This frontend should only be used to export an RTLIL\n");
+ log("netlist, i.e. after the \"proc\" pass has been used to convert all\n");
+ log("processes to logic networks and registers. A warning is generated when\n");
+ log("this command is called on a design with RTLIL processes.\n");
+ log("\n");
}
virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
{
- log_header("Executing Verilog backend.\n");
+ log_header(design, "Executing Verilog backend.\n");
norename = false;
noattr = false;
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-23 21:39:02 +0000