aboutsummaryrefslogtreecommitdiffstats
path: root/backends
diff options
context:
space:
mode:
Diffstat (limited to 'backends')
-rw-r--r--backends/aiger/aiger.cc25
-rw-r--r--backends/btor/btor.cc9
-rw-r--r--backends/cxxrtl/cxxrtl.h36
-rw-r--r--backends/cxxrtl/cxxrtl_backend.cc18
-rw-r--r--backends/firrtl/firrtl.cc6
-rw-r--r--backends/json/json.cc19
-rw-r--r--backends/smt2/smt2.cc11
-rw-r--r--backends/smt2/smtbmc.py7
-rw-r--r--backends/smt2/smtio.py10
-rw-r--r--backends/smv/smv.cc5
-rw-r--r--backends/verilog/verilog_backend.cc6
11 files changed, 132 insertions, 20 deletions
diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc
index 35935b847..547d131ee 100644
--- a/backends/aiger/aiger.cc
+++ b/backends/aiger/aiger.cc
@@ -606,7 +606,7 @@ struct AigerWriter
f << stringf("c\nGenerated by %s\n", yosys_version_str);
}
- void write_map(std::ostream &f, bool verbose_map)
+ void write_map(std::ostream &f, bool verbose_map, bool no_startoffset)
{
dict<int, string> input_lines;
dict<int, string> init_lines;
@@ -627,32 +627,33 @@ struct AigerWriter
continue;
int a = aig_map.at(sig[i]);
+ int index = no_startoffset ? i : (wire->start_offset+i);
if (verbose_map)
- wire_lines[a] += stringf("wire %d %d %s\n", a, wire->start_offset+i, log_id(wire));
+ wire_lines[a] += stringf("wire %d %d %s\n", a, index, log_id(wire));
if (wire->port_input) {
log_assert((a & 1) == 0);
- input_lines[a] += stringf("input %d %d %s\n", (a >> 1)-1, wire->start_offset+i, log_id(wire));
+ input_lines[a] += stringf("input %d %d %s\n", (a >> 1)-1, index, log_id(wire));
}
if (wire->port_output) {
int o = ordered_outputs.at(sig[i]);
- output_lines[o] += stringf("output %d %d %s\n", o, wire->start_offset+i, log_id(wire));
+ output_lines[o] += stringf("output %d %d %s\n", o, index, log_id(wire));
}
if (init_inputs.count(sig[i])) {
int a = init_inputs.at(sig[i]);
log_assert((a & 1) == 0);
- init_lines[a] += stringf("init %d %d %s\n", (a >> 1)-1, wire->start_offset+i, log_id(wire));
+ init_lines[a] += stringf("init %d %d %s\n", (a >> 1)-1, index, log_id(wire));
}
if (ordered_latches.count(sig[i])) {
int l = ordered_latches.at(sig[i]);
if (zinit_mode && (aig_latchinit.at(l) == 1))
- latch_lines[l] += stringf("invlatch %d %d %s\n", l, wire->start_offset+i, log_id(wire));
+ latch_lines[l] += stringf("invlatch %d %d %s\n", l, index, log_id(wire));
else
- latch_lines[l] += stringf("latch %d %d %s\n", l, wire->start_offset+i, log_id(wire));
+ latch_lines[l] += stringf("latch %d %d %s\n", l, index, log_id(wire));
}
}
}
@@ -713,6 +714,9 @@ struct AigerBackend : public Backend {
log(" -vmap <filename>\n");
log(" like -map, but more verbose\n");
log("\n");
+ log(" -no-startoffset\n");
+ log(" make indexes zero based, enable using map files with smt solvers.\n");
+ log("\n");
log(" -I, -O, -B, -L\n");
log(" If the design contains no input/output/assert/flip-flop then create one\n");
log(" dummy input/output/bad_state-pin or latch to make the tools reading the\n");
@@ -730,6 +734,7 @@ struct AigerBackend : public Backend {
bool omode = false;
bool bmode = false;
bool lmode = false;
+ bool no_startoffset = false;
std::string map_filename;
log_header(design, "Executing AIGER backend.\n");
@@ -762,6 +767,10 @@ struct AigerBackend : public Backend {
verbose_map = true;
continue;
}
+ if (args[argidx] == "-no-startoffset") {
+ no_startoffset = true;
+ continue;
+ }
if (args[argidx] == "-I") {
imode = true;
continue;
@@ -804,7 +813,7 @@ struct AigerBackend : public Backend {
mapf.open(map_filename.c_str(), std::ofstream::trunc);
if (mapf.fail())
log_error("Can't open file `%s' for writing: %s\n", map_filename.c_str(), strerror(errno));
- writer.write_map(mapf, verbose_map);
+ writer.write_map(mapf, verbose_map, no_startoffset);
}
}
} AigerBackend;
diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index 96df54a2c..73e88c049 100644
--- a/backends/btor/btor.cc
+++ b/backends/btor/btor.cc
@@ -678,7 +678,7 @@ struct BtorWorker
int sid = get_bv_sid(GetSize(sig_y));
int nid = next_nid++;
- btorf("%d state %d\n", nid, sid);
+ btorf("%d state %d%s\n", nid, sid, getinfo(cell).c_str());
if (cell->type == ID($anyconst)) {
int nid2 = next_nid++;
@@ -699,7 +699,7 @@ struct BtorWorker
int one_nid = get_sig_nid(State::S1);
int zero_nid = get_sig_nid(State::S0);
initstate_nid = next_nid++;
- btorf("%d state %d\n", initstate_nid, sid);
+ btorf("%d state %d%s\n", initstate_nid, sid, getinfo(cell).c_str());
btorf("%d init %d %d %d\n", next_nid++, sid, initstate_nid, one_nid);
btorf("%d next %d %d %d\n", next_nid++, sid, initstate_nid, zero_nid);
}
@@ -1399,6 +1399,11 @@ struct BtorBackend : public Backend {
log_header(design, "Executing BTOR backend.\n");
+ log_push();
+ Pass::call(design, "bmuxmap");
+ Pass::call(design, "demuxmap");
+ log_pop();
+
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++)
{
diff --git a/backends/cxxrtl/cxxrtl.h b/backends/cxxrtl/cxxrtl.h
index 3e1357498..b4ffa87cd 100644
--- a/backends/cxxrtl/cxxrtl.h
+++ b/backends/cxxrtl/cxxrtl.h
@@ -457,6 +457,42 @@ struct value : public expr_base<value<Bits>> {
return shr<AmountBits, /*Signed=*/true>(amount);
}
+ template<size_t ResultBits, size_t SelBits>
+ value<ResultBits> bmux(const value<SelBits> &sel) const {
+ static_assert(ResultBits << SelBits == Bits, "invalid sizes used in bmux()");
+ size_t amount = sel.data[0] * ResultBits;
+ size_t shift_chunks = amount / chunk::bits;
+ size_t shift_bits = amount % chunk::bits;
+ value<ResultBits> result;
+ chunk::type carry = 0;
+ if (ResultBits % chunk::bits + shift_bits > chunk::bits)
+ carry = data[result.chunks + shift_chunks] << (chunk::bits - shift_bits);
+ for (size_t n = 0; n < result.chunks; n++) {
+ result.data[result.chunks - 1 - n] = carry | (data[result.chunks + shift_chunks - 1 - n] >> shift_bits);
+ carry = (shift_bits == 0) ? 0
+ : data[result.chunks + shift_chunks - 1 - n] << (chunk::bits - shift_bits);
+ }
+ return result;
+ }
+
+ template<size_t ResultBits, size_t SelBits>
+ value<ResultBits> demux(const value<SelBits> &sel) const {
+ static_assert(Bits << SelBits == ResultBits, "invalid sizes used in demux()");
+ size_t amount = sel.data[0] * Bits;
+ size_t shift_chunks = amount / chunk::bits;
+ size_t shift_bits = amount % chunk::bits;
+ value<ResultBits> result;
+ chunk::type carry = 0;
+ for (size_t n = 0; n < chunks; n++) {
+ result.data[shift_chunks + n] = (data[n] << shift_bits) | carry;
+ carry = (shift_bits == 0) ? 0
+ : data[n] >> (chunk::bits - shift_bits);
+ }
+ if (Bits % chunk::bits + shift_bits > chunk::bits)
+ result.data[shift_chunks + chunks] = carry;
+ return result;
+ }
+
size_t ctpop() const {
size_t count = 0;
for (size_t n = 0; n < chunks; n++) {
diff --git a/backends/cxxrtl/cxxrtl_backend.cc b/backends/cxxrtl/cxxrtl_backend.cc
index 7a336f8c1..404755b1e 100644
--- a/backends/cxxrtl/cxxrtl_backend.cc
+++ b/backends/cxxrtl/cxxrtl_backend.cc
@@ -198,7 +198,7 @@ bool is_extending_cell(RTLIL::IdString type)
bool is_inlinable_cell(RTLIL::IdString type)
{
return is_unary_cell(type) || is_binary_cell(type) || type.in(
- ID($mux), ID($concat), ID($slice), ID($pmux));
+ ID($mux), ID($concat), ID($slice), ID($pmux), ID($bmux), ID($demux));
}
bool is_ff_cell(RTLIL::IdString type)
@@ -1154,6 +1154,22 @@ struct CxxrtlWorker {
for (int part = 0; part < s_width; part++) {
f << ")";
}
+ // Big muxes
+ } else if (cell->type == ID($bmux)) {
+ dump_sigspec_rhs(cell->getPort(ID::A), for_debug);
+ f << ".bmux<";
+ f << cell->getParam(ID::WIDTH).as_int();
+ f << ">(";
+ dump_sigspec_rhs(cell->getPort(ID::S), for_debug);
+ f << ").val()";
+ // Demuxes
+ } else if (cell->type == ID($demux)) {
+ dump_sigspec_rhs(cell->getPort(ID::A), for_debug);
+ f << ".demux<";
+ f << GetSize(cell->getPort(ID::Y));
+ f << ">(";
+ dump_sigspec_rhs(cell->getPort(ID::S), for_debug);
+ f << ").val()";
// Concats
} else if (cell->type == ID($concat)) {
dump_sigspec_rhs(cell->getPort(ID::B), for_debug);
diff --git a/backends/firrtl/firrtl.cc b/backends/firrtl/firrtl.cc
index 7abe584c9..85c44824f 100644
--- a/backends/firrtl/firrtl.cc
+++ b/backends/firrtl/firrtl.cc
@@ -1188,6 +1188,8 @@ struct FirrtlBackend : public Backend {
log("Write a FIRRTL netlist of the current design.\n");
log("The following commands are executed by this command:\n");
log(" pmuxtree\n");
+ log(" bmuxmap\n");
+ log(" demuxmap\n");
log("\n");
}
void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) override
@@ -1210,7 +1212,9 @@ struct FirrtlBackend : public Backend {
log_header(design, "Executing FIRRTL backend.\n");
log_push();
- Pass::call(design, stringf("pmuxtree"));
+ Pass::call(design, "pmuxtree");
+ Pass::call(design, "bmuxmap");
+ Pass::call(design, "demuxmap");
namecache.clear();
autoid_counter = 0;
diff --git a/backends/json/json.cc b/backends/json/json.cc
index 4aa8046d6..270d762ee 100644
--- a/backends/json/json.cc
+++ b/backends/json/json.cc
@@ -52,8 +52,23 @@ struct JsonWriter
string newstr = "\"";
for (char c : str) {
if (c == '\\')
+ newstr += "\\\\";
+ else if (c == '"')
+ newstr += "\\\"";
+ else if (c == '\b')
+ newstr += "\\b";
+ else if (c == '\f')
+ newstr += "\\f";
+ else if (c == '\n')
+ newstr += "\\n";
+ else if (c == '\r')
+ newstr += "\\r";
+ else if (c == '\t')
+ newstr += "\\t";
+ else if (c < 0x20)
+ newstr += stringf("\\u%04X", c);
+ else
newstr += c;
- newstr += c;
}
return newstr + "\"";
}
@@ -379,6 +394,7 @@ struct JsonBackend : public Backend {
log(" \"bits\": <bit_vector>\n");
log(" \"offset\": <the lowest bit index in use, if non-0>\n");
log(" \"upto\": <1 if the port bit indexing is MSB-first>\n");
+ log(" \"signed\": <1 if the port is signed>\n");
log(" }\n");
log("\n");
log("The \"offset\" and \"upto\" fields are skipped if their value would be 0.");
@@ -428,6 +444,7 @@ struct JsonBackend : public Backend {
log(" \"bits\": <bit_vector>\n");
log(" \"offset\": <the lowest bit index in use, if non-0>\n");
log(" \"upto\": <1 if the port bit indexing is MSB-first>\n");
+ log(" \"signed\": <1 if the port is signed>\n");
log(" }\n");
log("\n");
log("The \"hide_name\" fields are set to 1 when the name of this cell or net is\n");
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index f2fa003bc..9bf0de03e 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -985,8 +985,10 @@ struct Smt2Worker
string name_a = get_bool(cell->getPort(ID::A));
string name_en = get_bool(cell->getPort(ID::EN));
- string infostr = (cell->name[0] == '$' && cell->attributes.count(ID::src)) ? cell->attributes.at(ID::src).decode_string() : get_id(cell);
- decls.push_back(stringf("; yosys-smt2-%s %d %s\n", cell->type.c_str() + 1, id, infostr.c_str()));
+ if (cell->name[0] == '$' && cell->attributes.count(ID::src))
+ decls.push_back(stringf("; yosys-smt2-%s %d %s %s\n", cell->type.c_str() + 1, id, get_id(cell), cell->attributes.at(ID::src).decode_string().c_str()));
+ else
+ decls.push_back(stringf("; yosys-smt2-%s %d %s\n", cell->type.c_str() + 1, id, get_id(cell)));
if (cell->type == ID($cover))
decls.push_back(stringf("(define-fun |%s_%c %d| ((state |%s_s|)) Bool (and %s %s)) ; %s\n",
@@ -1531,6 +1533,11 @@ struct Smt2Backend : public Backend {
log_header(design, "Executing SMT2 backend.\n");
+ log_push();
+ Pass::call(design, "bmuxmap");
+ Pass::call(design, "demuxmap");
+ log_pop();
+
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++)
{
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index e5cfcdc08..7527f4105 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -492,7 +492,7 @@ if aimfile is not None:
got_state = True
for entry in f.read().splitlines():
- if len(entry) == 0 or entry[0] in "bcjfu.":
+ if len(entry) == 0 or entry[0] in "bcjfu.#":
continue
if not got_state:
@@ -583,7 +583,10 @@ if aimfile is not None:
if not got_topt:
skip_steps = max(skip_steps, step)
- num_steps = max(num_steps, step+1)
+ # some solvers optimize the properties so that they fail one cycle early,
+ # thus we check the properties in the cycle the aiger witness ends, and
+ # if that doesn't work, we check the cycle after that as well.
+ num_steps = max(num_steps, step+2)
step += 1
if btorwitfile is not None:
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index d73a875ba..3d458e6cf 100644
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -536,10 +536,16 @@ class SmtIo:
self.modinfo[self.curmod].clocks[fields[2]] = "event"
if fields[1] == "yosys-smt2-assert":
- self.modinfo[self.curmod].asserts["%s_a %s" % (self.curmod, fields[2])] = fields[3]
+ if len(fields) > 4:
+ self.modinfo[self.curmod].asserts["%s_a %s" % (self.curmod, fields[2])] = f'{fields[4]} ({fields[3]})'
+ else:
+ self.modinfo[self.curmod].asserts["%s_a %s" % (self.curmod, fields[2])] = fields[3]
if fields[1] == "yosys-smt2-cover":
- self.modinfo[self.curmod].covers["%s_c %s" % (self.curmod, fields[2])] = fields[3]
+ if len(fields) > 4:
+ self.modinfo[self.curmod].covers["%s_c %s" % (self.curmod, fields[2])] = f'{fields[4]} ({fields[3]})'
+ else:
+ self.modinfo[self.curmod].covers["%s_c %s" % (self.curmod, fields[2])] = fields[3]
if fields[1] == "yosys-smt2-maximize":
self.modinfo[self.curmod].maximize.add(fields[2])
diff --git a/backends/smv/smv.cc b/backends/smv/smv.cc
index 7bace6912..7d4f94adc 100644
--- a/backends/smv/smv.cc
+++ b/backends/smv/smv.cc
@@ -741,6 +741,11 @@ struct SmvBackend : public Backend {
log_header(design, "Executing SMV backend.\n");
+ log_push();
+ Pass::call(design, "bmuxmap");
+ Pass::call(design, "demuxmap");
+ log_pop();
+
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++)
{
diff --git a/backends/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc
index e4781ef3e..aa1d4558c 100644
--- a/backends/verilog/verilog_backend.cc
+++ b/backends/verilog/verilog_backend.cc
@@ -432,7 +432,7 @@ void dump_wire(std::ostream &f, std::string indent, RTLIL::Wire *wire)
dump_const(f, wire->attributes.at(ID::init));
}
f << stringf(";\n");
- } else if (!wire->port_input && !wire->port_output)
+ } else
f << stringf("%s" "wire%s %s;\n", indent.c_str(), range.c_str(), id(wire->name).c_str());
#endif
}
@@ -2300,7 +2300,11 @@ struct VerilogBackend : public Backend {
extmem_prefix = filename.substr(0, filename.rfind('.'));
}
+ log_push();
+ Pass::call(design, "bmuxmap");
+ Pass::call(design, "demuxmap");
Pass::call(design, "clean_zerowidth");
+ log_pop();
design->sort();
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-27 21:06:03 +0000