aboutsummaryrefslogtreecommitdiffstats
path: root/backends
diff options
context:
space:
mode:
Diffstat (limited to 'backends')
-rw-r--r--backends/aiger/xaiger.cc14
-rw-r--r--backends/blif/blif.cc7
-rw-r--r--backends/btor/btor.cc8
-rw-r--r--backends/firrtl/firrtl.cc296
-rw-r--r--backends/json/json.cc50
-rw-r--r--backends/simplec/simplec.cc6
-rw-r--r--backends/smt2/smt2.cc1
-rw-r--r--backends/smv/smv.cc7
-rw-r--r--backends/verilog/verilog_backend.cc14
9 files changed, 287 insertions, 116 deletions
diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc
index 69f63486c..a3a753912 100644
--- a/backends/aiger/xaiger.cc
+++ b/backends/aiger/xaiger.cc
@@ -53,7 +53,7 @@ PRIVATE_NAMESPACE_BEGIN
inline int32_t to_big_endian(int32_t i32) {
#if __BYTE_ORDER__ == __ORDER_LITTLE_ENDIAN__
- return __builtin_bswap32(i32);
+ return bswap32(i32);
#elif __BYTE_ORDER__ == __ORDER_BIG_ENDIAN__
return i32;
#else
@@ -610,15 +610,15 @@ struct XAigerWriter
std::stringstream h_buffer;
auto write_h_buffer = std::bind(write_buffer, std::ref(h_buffer), std::placeholders::_1);
write_h_buffer(1);
- log_debug("ciNum = %zu\n", input_bits.size() + ci_bits.size());
+ log_debug("ciNum = %d\n", GetSize(input_bits) + GetSize(ci_bits));
write_h_buffer(input_bits.size() + ci_bits.size());
- log_debug("coNum = %zu\n", output_bits.size() + co_bits.size());
+ log_debug("coNum = %d\n", GetSize(output_bits) + GetSize(co_bits));
write_h_buffer(output_bits.size() + co_bits.size());
- log_debug("piNum = %zu\n", input_bits.size());
+ log_debug("piNum = %d\n", GetSize(input_bits));
write_h_buffer(input_bits.size());
- log_debug("poNum = %zu\n", output_bits.size());
+ log_debug("poNum = %d\n", GetSize(output_bits));
write_h_buffer(output_bits.size());
- log_debug("boxNum = %zu\n", box_list.size());
+ log_debug("boxNum = %d\n", GetSize(box_list));
write_h_buffer(box_list.size());
RTLIL::Module *holes_module = nullptr;
@@ -772,7 +772,7 @@ struct XAigerWriter
if (output_bits.count(b)) {
int o = ordered_outputs.at(b);
- output_lines[o] += stringf("output %lu %d %s\n", o - co_bits.size(), i, log_id(wire));
+ output_lines[o] += stringf("output %d %d %s\n", o - GetSize(co_bits), i, log_id(wire));
continue;
}
diff --git a/backends/blif/blif.cc b/backends/blif/blif.cc
index a1761b662..f32b0f533 100644
--- a/backends/blif/blif.cc
+++ b/backends/blif/blif.cc
@@ -327,6 +327,13 @@ struct BlifDumper
goto internal_cell;
}
+ if (!config->icells_mode && cell->type == "$_NMUX_") {
+ f << stringf(".names %s %s %s %s\n0-0 1\n-01 1\n",
+ cstr(cell->getPort("\\A")), cstr(cell->getPort("\\B")),
+ cstr(cell->getPort("\\S")), cstr(cell->getPort("\\Y")));
+ goto internal_cell;
+ }
+
if (!config->icells_mode && cell->type == "$_FF_") {
f << stringf(".latch %s %s%s\n", cstr(cell->getPort("\\D")), cstr(cell->getPort("\\Q")),
cstr_init(cell->getPort("\\Q")));
diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index a507b120b..7bacce2af 100644
--- a/backends/btor/btor.cc
+++ b/backends/btor/btor.cc
@@ -496,7 +496,7 @@ struct BtorWorker
goto okay;
}
- if (cell->type.in("$mux", "$_MUX_"))
+ if (cell->type.in("$mux", "$_MUX_", "$_NMUX_"))
{
SigSpec sig_a = sigmap(cell->getPort("\\A"));
SigSpec sig_b = sigmap(cell->getPort("\\B"));
@@ -511,6 +511,12 @@ struct BtorWorker
int nid = next_nid++;
btorf("%d ite %d %d %d %d\n", nid, sid, nid_s, nid_b, nid_a);
+ if (cell->type == "$_NMUX_") {
+ int tmp = nid;
+ nid = next_nid++;
+ btorf("%d not %d %d\n", nid, sid, tmp);
+ }
+
add_nid_sig(nid, sig_y);
goto okay;
}
diff --git a/backends/firrtl/firrtl.cc b/backends/firrtl/firrtl.cc
index b7a798b85..ad4b37353 100644
--- a/backends/firrtl/firrtl.cc
+++ b/backends/firrtl/firrtl.cc
@@ -381,10 +381,10 @@ struct FirrtlWorker
// Given an expression for a shift amount, and a maximum width,
// generate the FIRRTL expression for equivalent dynamic shift taking into account FIRRTL shift semantics.
- std::string gen_dshl(const string b_expr, const int b_padded_width)
+ std::string gen_dshl(const string b_expr, const int b_width)
{
string result = b_expr;
- if (b_padded_width >= FIRRTL_MAX_DSH_WIDTH_ERROR) {
+ if (b_width >= FIRRTL_MAX_DSH_WIDTH_ERROR) {
int max_shift_width_bits = FIRRTL_MAX_DSH_WIDTH_ERROR - 1;
string max_shift_string = stringf("UInt<%d>(%d)", max_shift_width_bits, (1<<max_shift_width_bits) - 1);
// Deal with the difference in semantics between FIRRTL and verilog
@@ -422,22 +422,33 @@ struct FirrtlWorker
for (auto cell : module->cells())
{
- bool extract_y_bits = false; // Assume no extraction of final bits will be required.
+ static Const ndef(0, 0);
+
// Is this cell is a module instance?
if (cell->type[0] != '$')
{
process_instance(cell, wire_exprs);
continue;
}
+ // Not a module instance. Set up cell properties
+ bool extract_y_bits = false; // Assume no extraction of final bits will be required.
+ int a_width = cell->parameters.at("\\A_WIDTH", ndef).as_int(); // The width of "A"
+ int b_width = cell->parameters.at("\\B_WIDTH", ndef).as_int(); // The width of "A"
+ const int y_width = cell->parameters.at("\\Y_WIDTH", ndef).as_int(); // The width of the result
+ const bool a_signed = cell->parameters.at("\\A_SIGNED", ndef).as_bool();
+ const bool b_signed = cell->parameters.at("\\B_SIGNED", ndef).as_bool();
+ bool firrtl_is_signed = a_signed; // The result is signed (subsequent code may change this).
+ int firrtl_width = 0;
+ string primop;
+ bool always_uint = false;
+ string y_id = make_id(cell->name);
+
if (cell->type.in("$not", "$logic_not", "$neg", "$reduce_and", "$reduce_or", "$reduce_xor", "$reduce_bool", "$reduce_xnor"))
{
- string y_id = make_id(cell->name);
- bool is_signed = cell->parameters.at("\\A_SIGNED").as_bool();
- int y_width = cell->parameters.at("\\Y_WIDTH").as_int();
string a_expr = make_expr(cell->getPort("\\A"));
wire_decls.push_back(stringf(" wire %s: UInt<%d>\n", y_id.c_str(), y_width));
- if (cell->parameters.at("\\A_SIGNED").as_bool()) {
+ if (a_signed) {
a_expr = "asSInt(" + a_expr + ")";
}
@@ -446,12 +457,13 @@ struct FirrtlWorker
a_expr = stringf("pad(%s, %d)", a_expr.c_str(), y_width);
}
- string primop;
- bool always_uint = false;
+ // Assume the FIRRTL width is a single bit.
+ firrtl_width = 1;
if (cell->type == "$not") primop = "not";
else if (cell->type == "$neg") {
primop = "neg";
- is_signed = true; // Result of "neg" is signed (an SInt).
+ firrtl_is_signed = true; // Result of "neg" is signed (an SInt).
+ firrtl_width = a_width;
} else if (cell->type == "$logic_not") {
primop = "eq";
a_expr = stringf("%s, UInt(0)", a_expr.c_str());
@@ -466,14 +478,12 @@ struct FirrtlWorker
else if (cell->type == "$reduce_bool") {
primop = "neq";
// Use the sign of the a_expr and its width as the type (UInt/SInt) and width of the comparand.
- bool a_signed = cell->parameters.at("\\A_SIGNED").as_bool();
- int a_width = cell->parameters.at("\\A_WIDTH").as_int();
a_expr = stringf("%s, %cInt<%d>(0)", a_expr.c_str(), a_signed ? 'S' : 'U', a_width);
}
string expr = stringf("%s(%s)", primop.c_str(), a_expr.c_str());
- if ((is_signed && !always_uint))
+ if ((firrtl_is_signed && !always_uint))
expr = stringf("asUInt(%s)", expr.c_str());
cell_exprs.push_back(stringf(" %s <= %s\n", y_id.c_str(), expr.c_str()));
@@ -481,81 +491,121 @@ struct FirrtlWorker
continue;
}
- if (cell->type.in("$add", "$sub", "$mul", "$div", "$mod", "$xor", "$and", "$or", "$eq", "$eqx",
+ if (cell->type.in("$add", "$sub", "$mul", "$div", "$mod", "$xor", "$xnor", "$and", "$or", "$eq", "$eqx",
"$gt", "$ge", "$lt", "$le", "$ne", "$nex", "$shr", "$sshr", "$sshl", "$shl",
- "$logic_and", "$logic_or"))
+ "$logic_and", "$logic_or", "$pow"))
{
- string y_id = make_id(cell->name);
- bool is_signed = cell->parameters.at("\\A_SIGNED").as_bool();
- int y_width = cell->parameters.at("\\Y_WIDTH").as_int();
string a_expr = make_expr(cell->getPort("\\A"));
string b_expr = make_expr(cell->getPort("\\B"));
- int b_padded_width = cell->parameters.at("\\B_WIDTH").as_int();
wire_decls.push_back(stringf(" wire %s: UInt<%d>\n", y_id.c_str(), y_width));
- if (cell->parameters.at("\\A_SIGNED").as_bool()) {
+ if (a_signed) {
a_expr = "asSInt(" + a_expr + ")";
- }
- // Shift amount is always unsigned, and needn't be padded to result width.
- if (!cell->type.in("$shr", "$sshr", "$shl", "$sshl")) {
- if (cell->parameters.at("\\B_SIGNED").as_bool()) {
- b_expr = "asSInt(" + b_expr + ")";
+ // Expand the "A" operand to the result width
+ if (a_width < y_width) {
+ a_expr = stringf("pad(%s, %d)", a_expr.c_str(), y_width);
+ a_width = y_width;
}
- if (b_padded_width < y_width) {
- auto b_sig = cell->getPort("\\B");
- b_padded_width = y_width;
+ }
+ // Shift amount is always unsigned, and needn't be padded to result width,
+ // otherwise, we need to cast the b_expr appropriately
+ if (b_signed && !cell->type.in("$shr", "$sshr", "$shl", "$sshl", "$pow")) {
+ b_expr = "asSInt(" + b_expr + ")";
+ // Expand the "B" operand to the result width
+ if (b_width < y_width) {
+ b_expr = stringf("pad(%s, %d)", b_expr.c_str(), y_width);
+ b_width = y_width;
}
}
+ // For the arithmetic ops, expand operand widths to result widths befor performing the operation.
+ // This corresponds (according to iverilog) to what verilog compilers implement.
+ if (cell->type.in("$add", "$sub", "$mul", "$div", "$mod", "$xor", "$xnor", "$and", "$or"))
+ {
+ if (a_width < y_width) {
+ a_expr = stringf("pad(%s, %d)", a_expr.c_str(), y_width);
+ a_width = y_width;
+ }
+ if (b_width < y_width) {
+ b_expr = stringf("pad(%s, %d)", b_expr.c_str(), y_width);
+ b_width = y_width;
+ }
+ }
+ // Assume the FIRRTL width is the width of "A"
+ firrtl_width = a_width;
auto a_sig = cell->getPort("\\A");
- if (cell->parameters.at("\\A_SIGNED").as_bool() & (cell->type == "$shr")) {
- a_expr = "asUInt(" + a_expr + ")";
+ if (cell->type == "$add") {
+ primop = "add";
+ firrtl_is_signed = a_signed | b_signed;
+ firrtl_width = max(a_width, b_width);
+ } else if (cell->type == "$sub") {
+ primop = "sub";
+ firrtl_is_signed = true;
+ int a_widthInc = (!a_signed && b_signed) ? 2 : (a_signed && !b_signed) ? 1 : 0;
+ int b_widthInc = (a_signed && !b_signed) ? 2 : (!a_signed && b_signed) ? 1 : 0;
+ firrtl_width = max(a_width + a_widthInc, b_width + b_widthInc);
+ } else if (cell->type == "$mul") {
+ primop = "mul";
+ firrtl_is_signed = a_signed | b_signed;
+ firrtl_width = a_width + b_width;
+ } else if (cell->type == "$div") {
+ primop = "div";
+ firrtl_is_signed = a_signed | b_signed;
+ firrtl_width = a_width;
+ } else if (cell->type == "$mod") {
+ primop = "rem";
+ firrtl_width = min(a_width, b_width);
+ } else if (cell->type == "$and") {
+ primop = "and";
+ always_uint = true;
+ firrtl_width = max(a_width, b_width);
}
-
- string primop;
- bool always_uint = false;
- if (cell->type == "$add") primop = "add";
- else if (cell->type == "$sub") primop = "sub";
- else if (cell->type == "$mul") primop = "mul";
- else if (cell->type == "$div") primop = "div";
- else if (cell->type == "$mod") primop = "rem";
- else if (cell->type == "$and") {
- primop = "and";
- always_uint = true;
- }
else if (cell->type == "$or" ) {
- primop = "or";
- always_uint = true;
- }
+ primop = "or";
+ always_uint = true;
+ firrtl_width = max(a_width, b_width);
+ }
else if (cell->type == "$xor") {
- primop = "xor";
- always_uint = true;
- }
+ primop = "xor";
+ always_uint = true;
+ firrtl_width = max(a_width, b_width);
+ }
+ else if (cell->type == "$xnor") {
+ primop = "xnor";
+ always_uint = true;
+ firrtl_width = max(a_width, b_width);
+ }
else if ((cell->type == "$eq") | (cell->type == "$eqx")) {
- primop = "eq";
- always_uint = true;
- }
+ primop = "eq";
+ always_uint = true;
+ firrtl_width = 1;
+ }
else if ((cell->type == "$ne") | (cell->type == "$nex")) {
- primop = "neq";
- always_uint = true;
- }
+ primop = "neq";
+ always_uint = true;
+ firrtl_width = 1;
+ }
else if (cell->type == "$gt") {
- primop = "gt";
- always_uint = true;
- }
+ primop = "gt";
+ always_uint = true;
+ firrtl_width = 1;
+ }
else if (cell->type == "$ge") {
- primop = "geq";
- always_uint = true;
- }
+ primop = "geq";
+ always_uint = true;
+ firrtl_width = 1;
+ }
else if (cell->type == "$lt") {
- primop = "lt";
- always_uint = true;
- }
+ primop = "lt";
+ always_uint = true;
+ firrtl_width = 1;
+ }
else if (cell->type == "$le") {
- primop = "leq";
- always_uint = true;
- }
+ primop = "leq";
+ always_uint = true;
+ firrtl_width = 1;
+ }
else if ((cell->type == "$shl") | (cell->type == "$sshl")) {
// FIRRTL will widen the result (y) by the amount of the shift.
// We'll need to offset this by extracting the un-widened portion as Verilog would do.
@@ -564,11 +614,14 @@ struct FirrtlWorker
auto b_sig = cell->getPort("\\B");
if (b_sig.is_fully_const()) {
primop = "shl";
- b_expr = std::to_string(b_sig.as_int());
+ int shift_amount = b_sig.as_int();
+ b_expr = std::to_string(shift_amount);
+ firrtl_width = a_width + shift_amount;
} else {
primop = "dshl";
// Convert from FIRRTL left shift semantics.
- b_expr = gen_dshl(b_expr, b_padded_width);
+ b_expr = gen_dshl(b_expr, b_width);
+ firrtl_width = a_width + (1 << b_width) - 1;
}
}
else if ((cell->type == "$shr") | (cell->type == "$sshr")) {
@@ -578,36 +631,86 @@ struct FirrtlWorker
auto b_sig = cell->getPort("\\B");
if (b_sig.is_fully_const()) {
primop = "shr";
- b_expr = std::to_string(b_sig.as_int());
+ int shift_amount = b_sig.as_int();
+ b_expr = std::to_string(shift_amount);
+ firrtl_width = max(1, a_width - shift_amount);
} else {
primop = "dshr";
+ firrtl_width = a_width;
+ }
+ // We'll need to do some special fixups if the source (and thus result) is signed.
+ if (firrtl_is_signed) {
+ // If this is a "logical" shift right, pretend the source is unsigned.
+ if (cell->type == "$shr") {
+ a_expr = "asUInt(" + a_expr + ")";
+ }
}
}
else if ((cell->type == "$logic_and")) {
- primop = "and";
- a_expr = "neq(" + a_expr + ", UInt(0))";
- b_expr = "neq(" + b_expr + ", UInt(0))";
- always_uint = true;
- }
+ primop = "and";
+ a_expr = "neq(" + a_expr + ", UInt(0))";
+ b_expr = "neq(" + b_expr + ", UInt(0))";
+ always_uint = true;
+ firrtl_width = 1;
+ }
else if ((cell->type == "$logic_or")) {
- primop = "or";
- a_expr = "neq(" + a_expr + ", UInt(0))";
- b_expr = "neq(" + b_expr + ", UInt(0))";
- always_uint = true;
- }
+ primop = "or";
+ a_expr = "neq(" + a_expr + ", UInt(0))";
+ b_expr = "neq(" + b_expr + ", UInt(0))";
+ always_uint = true;
+ firrtl_width = 1;
+ }
+ else if ((cell->type == "$pow")) {
+ if (a_sig.is_fully_const() && a_sig.as_int() == 2) {
+ // We'll convert this to a shift. To simplify things, change the a_expr to "1"
+ // so we can use b_expr directly as a shift amount.
+ // Only support 2 ** N (i.e., shift left)
+ // FIRRTL will widen the result (y) by the amount of the shift.
+ // We'll need to offset this by extracting the un-widened portion as Verilog would do.
+ a_expr = firrtl_is_signed ? "SInt(1)" : "UInt(1)";
+ extract_y_bits = true;
+ // Is the shift amount constant?
+ auto b_sig = cell->getPort("\\B");
+ if (b_sig.is_fully_const()) {
+ primop = "shl";
+ int shiftAmount = b_sig.as_int();
+ if (shiftAmount < 0) {
+ log_error("Negative power exponent - %d: %s.%s\n", shiftAmount, log_id(module), log_id(cell));
+ }
+ b_expr = std::to_string(shiftAmount);
+ firrtl_width = a_width + shiftAmount;
+ } else {
+ primop = "dshl";
+ // Convert from FIRRTL left shift semantics.
+ b_expr = gen_dshl(b_expr, b_width);
+ firrtl_width = a_width + (1 << b_width) - 1;
+ }
+ } else {
+ log_error("Non power 2: %s.%s\n", log_id(module), log_id(cell));
+ }
+ }
if (!cell->parameters.at("\\B_SIGNED").as_bool()) {
b_expr = "asUInt(" + b_expr + ")";
}
- string expr = stringf("%s(%s, %s)", primop.c_str(), a_expr.c_str(), b_expr.c_str());
+ string expr;
+ // Deal with $xnor == ~^ (not xor)
+ if (primop == "xnor") {
+ expr = stringf("not(xor(%s, %s))", a_expr.c_str(), b_expr.c_str());
+ } else {
+ expr = stringf("%s(%s, %s)", primop.c_str(), a_expr.c_str(), b_expr.c_str());
+ }
- // Deal with FIRRTL's "shift widens" semantics
+ // Deal with FIRRTL's "shift widens" semantics, or the need to widen the FIRRTL result.
+ // If the operation is signed, the FIRRTL width will be 1 one bit larger.
if (extract_y_bits) {
expr = stringf("bits(%s, %d, 0)", expr.c_str(), y_width - 1);
+ } else if (firrtl_is_signed && (firrtl_width + 1) < y_width) {
+ expr = stringf("pad(%s, %d)", expr.c_str(), y_width);
}
- if ((is_signed && !always_uint) || cell->type.in("$sub"))
+ if ((firrtl_is_signed && !always_uint))
expr = stringf("asUInt(%s)", expr.c_str());
cell_exprs.push_back(stringf(" %s <= %s\n", y_id.c_str(), expr.c_str()));
@@ -618,7 +721,6 @@ struct FirrtlWorker
if (cell->type.in("$mux"))
{
- string y_id = make_id(cell->name);
int width = cell->parameters.at("\\WIDTH").as_int();
string a_expr = make_expr(cell->getPort("\\A"));
string b_expr = make_expr(cell->getPort("\\B"));
@@ -762,15 +864,14 @@ struct FirrtlWorker
if (clkpol == false)
log_error("Negative edge clock on FF %s.%s.\n", log_id(module), log_id(cell));
- string q_id = make_id(cell->name);
int width = cell->parameters.at("\\WIDTH").as_int();
string expr = make_expr(cell->getPort("\\D"));
string clk_expr = "asClock(" + make_expr(cell->getPort("\\CLK")) + ")";
- wire_decls.push_back(stringf(" reg %s: UInt<%d>, %s\n", q_id.c_str(), width, clk_expr.c_str()));
+ wire_decls.push_back(stringf(" reg %s: UInt<%d>, %s\n", y_id.c_str(), width, clk_expr.c_str()));
- cell_exprs.push_back(stringf(" %s <= %s\n", q_id.c_str(), expr.c_str()));
- register_reverse_wire_map(q_id, cell->getPort("\\Q"));
+ cell_exprs.push_back(stringf(" %s <= %s\n", y_id.c_str(), expr.c_str()));
+ register_reverse_wire_map(y_id, cell->getPort("\\Q"));
continue;
}
@@ -785,8 +886,6 @@ struct FirrtlWorker
// assign y = a[b +: y_width];
// We'll extract the correct bits as part of the primop.
- string y_id = make_id(cell->name);
- int y_width = cell->parameters.at("\\Y_WIDTH").as_int();
string a_expr = make_expr(cell->getPort("\\A"));
// Get the initial bit selector
string b_expr = make_expr(cell->getPort("\\B"));
@@ -808,18 +907,15 @@ struct FirrtlWorker
// assign y = a >> b;
// where b may be negative
- string y_id = make_id(cell->name);
- int y_width = cell->parameters.at("\\Y_WIDTH").as_int();
string a_expr = make_expr(cell->getPort("\\A"));
string b_expr = make_expr(cell->getPort("\\B"));
auto b_string = b_expr.c_str();
- int b_padded_width = cell->parameters.at("\\B_WIDTH").as_int();
string expr;
wire_decls.push_back(stringf(" wire %s: UInt<%d>\n", y_id.c_str(), y_width));
if (cell->getParam("\\B_SIGNED").as_bool()) {
// We generate a left or right shift based on the sign of b.
- std::string dshl = stringf("bits(dshl(%s, %s), 0, %d)", a_expr.c_str(), gen_dshl(b_expr, b_padded_width).c_str(), y_width);
+ std::string dshl = stringf("bits(dshl(%s, %s), 0, %d)", a_expr.c_str(), gen_dshl(b_expr, b_width).c_str(), y_width);
std::string dshr = stringf("dshr(%s, %s)", a_expr.c_str(), b_string);
expr = stringf("mux(%s < 0, %s, %s)",
b_string,
@@ -833,6 +929,20 @@ struct FirrtlWorker
register_reverse_wire_map(y_id, cell->getPort("\\Y"));
continue;
}
+ if (cell->type == "$pos") {
+ // assign y = a;
+// printCell(cell);
+ string a_expr = make_expr(cell->getPort("\\A"));
+ // Verilog appears to treat the result as signed, so if the result is wider than "A",
+ // we need to pad.
+ if (a_width < y_width) {
+ a_expr = stringf("pad(%s, %d)", a_expr.c_str(), y_width);
+ }
+ wire_decls.push_back(stringf(" wire %s: UInt<%d>\n", y_id.c_str(), y_width));
+ cell_exprs.push_back(stringf(" %s <= %s\n", y_id.c_str(), a_expr.c_str()));
+ register_reverse_wire_map(y_id, cell->getPort("\\Y"));
+ continue;
+ }
log_error("Cell type not supported: %s (%s.%s)\n", log_id(cell->type), log_id(module), log_id(cell));
}
diff --git a/backends/json/json.cc b/backends/json/json.cc
index dda4dfedd..107009ee4 100644
--- a/backends/json/json.cc
+++ b/backends/json/json.cc
@@ -83,20 +83,43 @@ struct JsonWriter
return str + " ]";
}
+ void write_parameter_value(const Const &value)
+ {
+ if ((value.flags & RTLIL::ConstFlags::CONST_FLAG_STRING) != 0) {
+ string str = value.decode_string();
+ int state = 0;
+ for (char c : str) {
+ if (state == 0) {
+ if (c == '0' || c == '1' || c == 'x' || c == 'z')
+ state = 0;
+ else if (c == ' ')
+ state = 1;
+ else
+ state = 2;
+ } else if (state == 1 && c != ' ')
+ state = 2;
+ }
+ if (state < 2)
+ str += " ";
+ f << get_string(str);
+ } else
+ if (GetSize(value) == 32 && value.is_fully_def()) {
+ if ((value.flags & RTLIL::ConstFlags::CONST_FLAG_SIGNED) != 0)
+ f << stringf("%d", value.as_int());
+ else
+ f << stringf("%u", value.as_int());
+ } else {
+ f << get_string(value.as_string());
+ }
+ }
+
void write_parameters(const dict<IdString, Const> &parameters, bool for_module=false)
{
bool first = true;
for (auto &param : parameters) {
f << stringf("%s\n", first ? "" : ",");
f << stringf(" %s%s: ", for_module ? "" : " ", 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 if ((param.second.flags & RTLIL::ConstFlags::CONST_FLAG_SIGNED) != 0)
- f << stringf("%d", param.second.as_int());
- else
- f << stringf("%u", param.second.as_int());
+ write_parameter_value(param.second);
first = false;
}
}
@@ -342,12 +365,13 @@ struct JsonBackend : public Backend {
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("connected to a constant driver are denoted as string \"0\", \"1\", \"x\", or\n");
+ log("\"z\" instead of a number.\n");
log("\n");
- log("Numeric parameter and attribute values up to 32 bits are written as decimal\n");
- log("values. Numbers larger than that are written as string holding the binary\n");
- log("representation of the value.\n");
+ log("Numeric 32-bit parameter and attribute values are written as decimal values.\n");
+ log("Bit verctors of different sizes, or ones containing 'x' or 'z' bits, are written\n");
+ log("as string holding the binary representation of the value. Strings are written\n");
+ log("as strings, with an appended blank in cases of strings of the form /[01xz]* */.\n");
log("\n");
log("For example the following Verilog code:\n");
log("\n");
diff --git a/backends/simplec/simplec.cc b/backends/simplec/simplec.cc
index 6f2ccbe20..54dbb84af 100644
--- a/backends/simplec/simplec.cc
+++ b/backends/simplec/simplec.cc
@@ -472,7 +472,7 @@ struct SimplecWorker
return;
}
- if (cell->type == "$_MUX_")
+ if (cell->type.in("$_MUX_", "$_NMUX_"))
{
SigBit a = sigmaps.at(work->module)(cell->getPort("\\A"));
SigBit b = sigmaps.at(work->module)(cell->getPort("\\B"));
@@ -484,7 +484,9 @@ struct SimplecWorker
string s_expr = s.wire ? util_get_bit(work->prefix + cid(s.wire->name), s.wire->width, s.offset) : s.data ? "1" : "0";
// casts to bool are a workaround for CBMC bug (https://github.com/diffblue/cbmc/issues/933)
- string expr = stringf("%s ? (bool)%s : (bool)%s", s_expr.c_str(), b_expr.c_str(), a_expr.c_str());
+ string expr = stringf("%s ? %s(bool)%s : %s(bool)%s", s_expr.c_str(),
+ cell->type == "$_NMUX_" ? "!" : "", b_expr.c_str(),
+ cell->type == "$_NMUX_" ? "!" : "", a_expr.c_str());
log_assert(y.wire);
funct_declarations.push_back(util_set_bit(work->prefix + cid(y.wire->name), y.wire->width, y.offset, expr) +
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index e318a4051..ddd680782 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -510,6 +510,7 @@ struct Smt2Worker
if (cell->type == "$_ANDNOT_") return export_gate(cell, "(and A (not B))");
if (cell->type == "$_ORNOT_") return export_gate(cell, "(or A (not B))");
if (cell->type == "$_MUX_") return export_gate(cell, "(ite S B A)");
+ if (cell->type == "$_NMUX_") return export_gate(cell, "(not (ite S B A))");
if (cell->type == "$_AOI3_") return export_gate(cell, "(not (or (and A B) C))");
if (cell->type == "$_OAI3_") return export_gate(cell, "(not (and (or A B) C))");
if (cell->type == "$_AOI4_") return export_gate(cell, "(not (or (and A B) (and C D)))");
diff --git a/backends/smv/smv.cc b/backends/smv/smv.cc
index d75456c1b..e9586fae0 100644
--- a/backends/smv/smv.cc
+++ b/backends/smv/smv.cc
@@ -537,6 +537,13 @@ struct SmvWorker
continue;
}
+ if (cell->type == "$_NMUX_")
+ {
+ definitions.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_")
{
definitions.push_back(stringf("%s := !((%s & %s) | %s);", lvalue(cell->getPort("\\Y")),
diff --git a/backends/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc
index e0b3a6f80..776f4eacb 100644
--- a/backends/verilog/verilog_backend.cc
+++ b/backends/verilog/verilog_backend.cc
@@ -558,6 +558,20 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
return true;
}
+ if (cell->type == "$_NMUX_") {
+ f << stringf("%s" "assign ", indent.c_str());
+ dump_sigspec(f, cell->getPort("\\Y"));
+ f << stringf(" = !(");
+ dump_cell_expr_port(f, cell, "S", false);
+ f << stringf(" ? ");
+ dump_attributes(f, "", cell->attributes, ' ');
+ dump_cell_expr_port(f, cell, "B", false);
+ f << stringf(" : ");
+ dump_cell_expr_port(f, cell, "A", false);
+ f << stringf(");\n");
+ return true;
+ }
+
if (cell->type.in("$_AOI3_", "$_OAI3_")) {
f << stringf("%s" "assign ", indent.c_str());
dump_sigspec(f, cell->getPort("\\Y"));