mirror of
https://github.com/YosysHQ/yosys
synced 2025-04-24 01:25:33 +00:00
Merge branch 'eddie/abc9_refactor' into xaig_dff
This commit is contained in:
commit
24c934f1af
171 changed files with 6745 additions and 4523 deletions
|
@ -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
|
||||
|
@ -392,7 +392,6 @@ struct XAigerWriter
|
|||
#endif
|
||||
log_assert(no_loops);
|
||||
|
||||
pool<IdString> seen_boxes;
|
||||
for (auto cell_name : toposort.sorted) {
|
||||
RTLIL::Cell *cell = module->cell(cell_name);
|
||||
log_assert(cell);
|
||||
|
@ -401,47 +400,6 @@ struct XAigerWriter
|
|||
if (!box_module || !box_module->attributes.count("\\abc_box_id"))
|
||||
continue;
|
||||
|
||||
if (seen_boxes.insert(cell->type).second) {
|
||||
auto it = box_module->attributes.find("\\abc_carry");
|
||||
if (it != box_module->attributes.end()) {
|
||||
RTLIL::Wire *carry_in = nullptr, *carry_out = nullptr;
|
||||
auto carry_in_out = it->second.decode_string();
|
||||
auto tokens = split_tokens(carry_in_out, ",");
|
||||
if (tokens.size() != 2)
|
||||
log_error("'abc_carry' attribute on module '%s' does not contain exactly two comma-separated tokens.\n", log_id(cell->type));
|
||||
auto carry_in_name = RTLIL::escape_id(tokens[0]);
|
||||
carry_in = box_module->wire(carry_in_name);
|
||||
if (!carry_in || !carry_in->port_input)
|
||||
log_error("'abc_carry' on module '%s' contains '%s' which does not exist or is not an input port.\n", log_id(cell->type), carry_in_name.c_str());
|
||||
|
||||
auto carry_out_name = RTLIL::escape_id(tokens[1]);
|
||||
carry_out = box_module->wire(carry_out_name);
|
||||
if (!carry_out || !carry_out->port_output)
|
||||
log_error("'abc_carry' on module '%s' contains '%s' which does not exist or is not an output port.\n", log_id(cell->type), carry_out_name.c_str());
|
||||
|
||||
auto &ports = box_module->ports;
|
||||
for (auto jt = ports.begin(); jt != ports.end(); ) {
|
||||
RTLIL::Wire* w = box_module->wire(*jt);
|
||||
log_assert(w);
|
||||
if (w == carry_in || w == carry_out) {
|
||||
jt = ports.erase(jt);
|
||||
continue;
|
||||
}
|
||||
if (w->port_id > carry_in->port_id)
|
||||
--w->port_id;
|
||||
if (w->port_id > carry_out->port_id)
|
||||
--w->port_id;
|
||||
log_assert(w->port_input || w->port_output);
|
||||
log_assert(ports[w->port_id-1] == w->name);
|
||||
++jt;
|
||||
}
|
||||
ports.push_back(carry_in->name);
|
||||
carry_in->port_id = ports.size();
|
||||
ports.push_back(carry_out->name);
|
||||
carry_out->port_id = ports.size();
|
||||
}
|
||||
}
|
||||
|
||||
// Fully pad all unused input connections of this box cell with S0
|
||||
// Fully pad all undriven output connections of this box cell with anonymous wires
|
||||
// NB: Assume box_module->ports are sorted alphabetically
|
||||
|
@ -454,11 +412,11 @@ struct XAigerWriter
|
|||
RTLIL::SigSpec rhs;
|
||||
if (it != cell->connections_.end()) {
|
||||
if (GetSize(it->second) < GetSize(w))
|
||||
it->second.append(RTLIL::SigSpec(RTLIL::S0, GetSize(w)-GetSize(it->second)));
|
||||
it->second.append(RTLIL::SigSpec(State::S0, GetSize(w)-GetSize(it->second)));
|
||||
rhs = it->second;
|
||||
}
|
||||
else {
|
||||
rhs = RTLIL::SigSpec(RTLIL::S0, GetSize(w));
|
||||
rhs = RTLIL::SigSpec(State::S0, GetSize(w));
|
||||
cell->setPort(port_name, rhs);
|
||||
}
|
||||
|
||||
|
@ -466,10 +424,10 @@ struct XAigerWriter
|
|||
for (auto b : rhs.bits()) {
|
||||
SigBit I = sigmap(b);
|
||||
if (b == RTLIL::Sx)
|
||||
b = RTLIL::S0;
|
||||
b = State::S0;
|
||||
else if (I != b) {
|
||||
if (I == RTLIL::Sx)
|
||||
alias_map[b] = RTLIL::S0;
|
||||
alias_map[b] = State::S0;
|
||||
else
|
||||
alias_map[b] = I;
|
||||
}
|
||||
|
@ -768,19 +726,18 @@ 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() + ff_bits.size() + ci_bits.size());
|
||||
log_debug("ciNum = %d\n", GetSize(input_bits) + GetSize(ff_bits) + GetSize(ci_bits));
|
||||
write_h_buffer(input_bits.size() + ff_bits.size() + ci_bits.size());
|
||||
log_debug("coNum = %zu\n", output_bits.size() + ff_bits.size() + co_bits.size());
|
||||
write_h_buffer(output_bits.size() + ff_bits.size() + co_bits.size());
|
||||
log_debug("piNum = %zu\n", input_bits.size() + ff_bits.size());
|
||||
write_h_buffer(input_bits.size()+ ff_bits.size());
|
||||
log_debug("poNum = %zu\n", output_bits.size() + ff_bits.size());
|
||||
log_debug("coNum = %d\n", GetSize(output_bits) + GetSize(ff_bits) + GetSize(co_bits));
|
||||
write_h_buffer(output_bits.size() + GetSize(ff_bits) + GetSize(co_bits));
|
||||
log_debug("piNum = %d\n", GetSize(input_bits) + GetSize(ff_bits));
|
||||
write_h_buffer(input_bits.size() + ff_bits.size());
|
||||
log_debug("poNum = %d\n", GetSize(output_bits) + GetSize(ff_bits));
|
||||
write_h_buffer(output_bits.size() + ff_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;
|
||||
holes_module = module->design->addModule("$__holes__");
|
||||
RTLIL::Module *holes_module = module->design->addModule("$__holes__");
|
||||
log_assert(holes_module);
|
||||
|
||||
int port_id = 1;
|
||||
|
@ -830,7 +787,7 @@ struct XAigerWriter
|
|||
if (holes_cell)
|
||||
port_wire.append(holes_wire);
|
||||
else
|
||||
holes_module->connect(holes_wire, RTLIL::S0);
|
||||
holes_module->connect(holes_wire, State::S0);
|
||||
}
|
||||
if (!port_wire.empty())
|
||||
holes_cell->setPort(w->name, port_wire);
|
||||
|
@ -901,27 +858,33 @@ struct XAigerWriter
|
|||
Pass::call(holes_module->design, "flatten -wb");
|
||||
|
||||
// TODO: Should techmap/aigmap/check all lib_whitebox-es just once,
|
||||
// instead of per write_xaiger call
|
||||
// instead of per write_xaiger call
|
||||
Pass::call(holes_module->design, "techmap");
|
||||
Pass::call(holes_module->design, "aigmap");
|
||||
for (auto cell : holes_module->cells())
|
||||
if (!cell->type.in("$_NOT_", "$_AND_"))
|
||||
log_error("Whitebox contents cannot be represented as AIG. Please verify whiteboxes are synthesisable.\n");
|
||||
|
||||
Pass::call(holes_module->design, "clean -purge");
|
||||
holes_module->design->selection_stack.pop_back();
|
||||
|
||||
// Move into a new (temporary) design so that "clean" will only
|
||||
// operate (and run checks on) this one module
|
||||
RTLIL::Design *holes_design = new RTLIL::Design;
|
||||
holes_module->design->modules_.erase(holes_module->name);
|
||||
holes_design->add(holes_module);
|
||||
Pass::call(holes_design, "clean -purge");
|
||||
|
||||
std::stringstream a_buffer;
|
||||
XAigerWriter writer(holes_module, false /*zinit_mode*/, true /* holes_mode */);
|
||||
writer.write_aiger(a_buffer, false /*ascii_mode*/);
|
||||
|
||||
holes_module->design->selection_stack.pop_back();
|
||||
delete holes_design;
|
||||
|
||||
f << "a";
|
||||
std::string buffer_str = a_buffer.str();
|
||||
int32_t buffer_size_be = to_big_endian(buffer_str.size());
|
||||
f.write(reinterpret_cast<const char*>(&buffer_size_be), sizeof(buffer_size_be));
|
||||
f.write(buffer_str.data(), buffer_str.size());
|
||||
holes_module->design->remove(holes_module);
|
||||
|
||||
log_pop();
|
||||
}
|
||||
|
@ -960,7 +923,7 @@ struct XAigerWriter
|
|||
auto it = init_map.find(b);
|
||||
if (it != init_map.end())
|
||||
init = it->second ? 1 : 0;
|
||||
output_lines[o] += stringf("output %lu %d %s %d\n", o - co_bits.size(), i, log_id(wire), init);
|
||||
output_lines[o] += stringf("output %d %d %s %d\n", o - GetSize(co_bits), i, log_id(wire), init);
|
||||
continue;
|
||||
}
|
||||
|
||||
|
|
|
@ -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")));
|
||||
|
@ -370,7 +377,7 @@ struct BlifDumper
|
|||
f << stringf("\n");
|
||||
RTLIL::SigSpec mask = cell->parameters.at("\\LUT");
|
||||
for (int i = 0; i < (1 << width); i++)
|
||||
if (mask[i] == RTLIL::S1) {
|
||||
if (mask[i] == State::S1) {
|
||||
for (int j = width-1; j >= 0; j--) {
|
||||
f << ((i>>j)&1 ? '1' : '0');
|
||||
}
|
||||
|
|
|
@ -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;
|
||||
}
|
||||
|
@ -610,8 +616,8 @@ struct BtorWorker
|
|||
if (initstate_nid < 0)
|
||||
{
|
||||
int sid = get_bv_sid(1);
|
||||
int one_nid = get_sig_nid(Const(1, 1));
|
||||
int zero_nid = get_sig_nid(Const(0, 1));
|
||||
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 init %d %d %d\n", next_nid++, sid, initstate_nid, one_nid);
|
||||
|
|
|
@ -122,9 +122,9 @@ struct FirrtlWorker
|
|||
// Current (3/13/2019) conventions:
|
||||
// generate a constant 0 for clock and a constant 1 for enable if they are undefined.
|
||||
if (!clk.is_fully_def())
|
||||
this->clk = SigSpec(RTLIL::Const(0, 1));
|
||||
this->clk = SigSpec(State::S0);
|
||||
if (!ena.is_fully_def())
|
||||
this->ena = SigSpec(RTLIL::Const(1, 1));
|
||||
this->ena = SigSpec(State::S1);
|
||||
}
|
||||
string gen_read(const char * indent) {
|
||||
string addr_expr = make_expr(addr);
|
||||
|
@ -297,7 +297,7 @@ struct FirrtlWorker
|
|||
std::string cell_type = fid(cell->type);
|
||||
std::string instanceOf;
|
||||
// If this is a parameterized module, its parent module is encoded in the cell type
|
||||
if (cell->type.substr(0, 8) == "$paramod")
|
||||
if (cell->type.begins_with("$paramod"))
|
||||
{
|
||||
std::string::iterator it;
|
||||
for (it = cell_type.begin(); it < cell_type.end(); it++)
|
||||
|
@ -363,7 +363,7 @@ struct FirrtlWorker
|
|||
}
|
||||
// Check for subfield assignment.
|
||||
std::string bitsString = "bits(";
|
||||
if (sinkExpr.substr(0, bitsString.length()) == bitsString ) {
|
||||
if (sinkExpr.compare(0, bitsString.length(), bitsString) == 0) {
|
||||
if (sinkSig == nullptr)
|
||||
log_error("Unknown subfield %s.%s\n", cell_type.c_str(), sinkExpr.c_str());
|
||||
// Don't generate the assignment here.
|
||||
|
@ -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());
|
||||
|
||||
// Deal with FIRRTL's "shift widens" semantics
|
||||
if (extract_y_bits) {
|
||||
expr = stringf("bits(%s, %d, 0)", expr.c_str(), y_width - 1);
|
||||
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());
|
||||
}
|
||||
|
||||
if ((is_signed && !always_uint) || cell->type.in("$sub"))
|
||||
// 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 ((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,21 +864,20 @@ 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;
|
||||
}
|
||||
|
||||
// This may be a parameterized module - paramod.
|
||||
if (cell->type.substr(0, 8) == "$paramod")
|
||||
if (cell->type.begins_with("$paramod"))
|
||||
{
|
||||
process_instance(cell, wire_exprs);
|
||||
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,7 +929,21 @@ struct FirrtlWorker
|
|||
register_reverse_wire_map(y_id, cell->getPort("\\Y"));
|
||||
continue;
|
||||
}
|
||||
log_warning("Cell type not supported: %s (%s.%s)\n", log_id(cell->type), log_id(module), log_id(cell));
|
||||
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));
|
||||
}
|
||||
|
||||
for (auto conn : module->connections())
|
||||
|
|
|
@ -40,8 +40,8 @@ void ILANG_BACKEND::dump_const(std::ostream &f, const RTLIL::Const &data, int wi
|
|||
for (int i = 0; i < width; i++) {
|
||||
log_assert(offset+i < (int)data.bits.size());
|
||||
switch (data.bits[offset+i]) {
|
||||
case RTLIL::S0: break;
|
||||
case RTLIL::S1: val |= 1 << i; break;
|
||||
case State::S0: break;
|
||||
case State::S1: val |= 1 << i; break;
|
||||
default: val = -1; break;
|
||||
}
|
||||
}
|
||||
|
@ -54,8 +54,8 @@ void ILANG_BACKEND::dump_const(std::ostream &f, const RTLIL::Const &data, int wi
|
|||
for (int i = offset+width-1; i >= offset; i--) {
|
||||
log_assert(i < (int)data.bits.size());
|
||||
switch (data.bits[i]) {
|
||||
case RTLIL::S0: f << stringf("0"); break;
|
||||
case RTLIL::S1: f << stringf("1"); break;
|
||||
case State::S0: f << stringf("0"); break;
|
||||
case State::S1: f << stringf("1"); break;
|
||||
case RTLIL::Sx: f << stringf("x"); break;
|
||||
case RTLIL::Sz: f << stringf("z"); break;
|
||||
case RTLIL::Sa: f << stringf("-"); break;
|
||||
|
|
|
@ -108,7 +108,7 @@ struct IntersynthBackend : public Backend {
|
|||
if (f.fail())
|
||||
log_error("Can't open lib file `%s'.\n", filename.c_str());
|
||||
RTLIL::Design *lib = new RTLIL::Design;
|
||||
Frontend::frontend_call(lib, &f, filename, (filename.size() > 3 && filename.substr(filename.size()-3) == ".il") ? "ilang" : "verilog");
|
||||
Frontend::frontend_call(lib, &f, filename, (filename.size() > 3 && filename.compare(filename.size()-3, std::string::npos, ".il") == 0 ? "ilang" : "verilog"));
|
||||
libs.push_back(lib);
|
||||
}
|
||||
|
||||
|
@ -183,7 +183,7 @@ struct IntersynthBackend : public Backend {
|
|||
if (param.second.bits.size() != 32) {
|
||||
node_code += stringf(" %s '", RTLIL::id2cstr(param.first));
|
||||
for (int i = param.second.bits.size()-1; i >= 0; i--)
|
||||
node_code += param.second.bits[i] == RTLIL::S1 ? "1" : "0";
|
||||
node_code += param.second.bits[i] == State::S1 ? "1" : "0";
|
||||
} else
|
||||
node_code += stringf(" %s 0x%x", RTLIL::id2cstr(param.first), param.second.as_int());
|
||||
}
|
||||
|
|
|
@ -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> ¶meters, bool for_module=false)
|
||||
{
|
||||
bool first = true;
|
||||
for (auto ¶m : 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");
|
||||
|
|
|
@ -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) +
|
||||
|
|
|
@ -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)))");
|
||||
|
@ -600,7 +601,7 @@ struct Smt2Worker
|
|||
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 (cell->type.in("$mux", "$pmux"))
|
||||
{
|
||||
int width = GetSize(cell->getPort("\\Y"));
|
||||
std::string processed_expr = get_bv(cell->getPort("\\A"));
|
||||
|
@ -1475,7 +1476,7 @@ struct Smt2Backend : public Backend {
|
|||
int indent = 0;
|
||||
while (indent < GetSize(line) && (line[indent] == ' ' || line[indent] == '\t'))
|
||||
indent++;
|
||||
if (line.substr(indent, 2) == "%%")
|
||||
if (line.compare(indent, 2, "%%") == 0)
|
||||
break;
|
||||
*f << line << std::endl;
|
||||
}
|
||||
|
|
|
@ -43,7 +43,11 @@ if os.name == "posix":
|
|||
if current_rlimit_stack[1] != resource.RLIM_INFINITY:
|
||||
smtio_stacksize = min(smtio_stacksize, current_rlimit_stack[1])
|
||||
if current_rlimit_stack[0] < smtio_stacksize:
|
||||
resource.setrlimit(resource.RLIMIT_STACK, (smtio_stacksize, current_rlimit_stack[1]))
|
||||
try:
|
||||
resource.setrlimit(resource.RLIMIT_STACK, (smtio_stacksize, current_rlimit_stack[1]))
|
||||
except ValueError:
|
||||
# couldn't get more stack, just run with what we have
|
||||
pass
|
||||
|
||||
|
||||
# currently running solvers (so we can kill them)
|
||||
|
|
|
@ -61,7 +61,7 @@ struct SmvWorker
|
|||
{
|
||||
string name = stringf("_%s", id.c_str());
|
||||
|
||||
if (name.substr(0, 2) == "_\\")
|
||||
if (name.compare(0, 2, "_\\") == 0)
|
||||
name = "_" + name.substr(2);
|
||||
|
||||
for (auto &c : name) {
|
||||
|
@ -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")),
|
||||
|
|
|
@ -189,7 +189,8 @@ void dump_const(std::ostream &f, const RTLIL::Const &data, int width = -1, int o
|
|||
if (width < 0)
|
||||
width = data.bits.size() - offset;
|
||||
if (width == 0) {
|
||||
f << "\"\"";
|
||||
// See IEEE 1364-2005 Clause 5.1.14.
|
||||
f << "{0{1'b0}}";
|
||||
return;
|
||||
}
|
||||
if (nostr)
|
||||
|
@ -199,9 +200,9 @@ void dump_const(std::ostream &f, const RTLIL::Const &data, int width = -1, int o
|
|||
int32_t val = 0;
|
||||
for (int i = offset+width-1; i >= offset; i--) {
|
||||
log_assert(i < (int)data.bits.size());
|
||||
if (data.bits[i] != RTLIL::S0 && data.bits[i] != RTLIL::S1)
|
||||
if (data.bits[i] != State::S0 && data.bits[i] != State::S1)
|
||||
goto dump_hex;
|
||||
if (data.bits[i] == RTLIL::S1)
|
||||
if (data.bits[i] == State::S1)
|
||||
val |= 1 << (i - offset);
|
||||
}
|
||||
if (decimal)
|
||||
|
@ -218,11 +219,11 @@ void dump_const(std::ostream &f, const RTLIL::Const &data, int width = -1, int o
|
|||
for (int i = offset; i < offset+width; i++) {
|
||||
log_assert(i < (int)data.bits.size());
|
||||
switch (data.bits[i]) {
|
||||
case RTLIL::S0: bin_digits.push_back('0'); break;
|
||||
case RTLIL::S1: bin_digits.push_back('1'); break;
|
||||
case State::S0: bin_digits.push_back('0'); break;
|
||||
case State::S1: bin_digits.push_back('1'); break;
|
||||
case RTLIL::Sx: bin_digits.push_back('x'); break;
|
||||
case RTLIL::Sz: bin_digits.push_back('z'); break;
|
||||
case RTLIL::Sa: bin_digits.push_back('z'); break;
|
||||
case RTLIL::Sa: bin_digits.push_back('?'); break;
|
||||
case RTLIL::Sm: log_error("Found marker state in final netlist.");
|
||||
}
|
||||
}
|
||||
|
@ -251,6 +252,12 @@ void dump_const(std::ostream &f, const RTLIL::Const &data, int width = -1, int o
|
|||
hex_digits.push_back('z');
|
||||
continue;
|
||||
}
|
||||
if (bit_3 == '?' || bit_2 == '?' || bit_1 == '?' || bit_0 == '?') {
|
||||
if (bit_3 != '?' || bit_2 != '?' || bit_1 != '?' || bit_0 != '?')
|
||||
goto dump_bin;
|
||||
hex_digits.push_back('?');
|
||||
continue;
|
||||
}
|
||||
int val = 8*(bit_3 - '0') + 4*(bit_2 - '0') + 2*(bit_1 - '0') + (bit_0 - '0');
|
||||
hex_digits.push_back(val < 10 ? '0' + val : 'a' + val - 10);
|
||||
}
|
||||
|
@ -266,11 +273,11 @@ void dump_const(std::ostream &f, const RTLIL::Const &data, int width = -1, int o
|
|||
for (int i = offset+width-1; i >= offset; i--) {
|
||||
log_assert(i < (int)data.bits.size());
|
||||
switch (data.bits[i]) {
|
||||
case RTLIL::S0: f << stringf("0"); break;
|
||||
case RTLIL::S1: f << stringf("1"); break;
|
||||
case State::S0: f << stringf("0"); break;
|
||||
case State::S1: f << stringf("1"); break;
|
||||
case RTLIL::Sx: f << stringf("x"); break;
|
||||
case RTLIL::Sz: f << stringf("z"); break;
|
||||
case RTLIL::Sa: f << stringf("z"); break;
|
||||
case RTLIL::Sa: f << stringf("?"); break;
|
||||
case RTLIL::Sm: log_error("Found marker state in final netlist.");
|
||||
}
|
||||
}
|
||||
|
@ -373,9 +380,9 @@ void dump_attributes(std::ostream &f, std::string indent, dict<RTLIL::IdString,
|
|||
for (auto it = attributes.begin(); it != attributes.end(); ++it) {
|
||||
f << stringf("%s" "%s %s", indent.c_str(), as_comment ? "/*" : "(*", id(it->first).c_str());
|
||||
f << stringf(" = ");
|
||||
if (modattr && (it->second == Const(0, 1) || it->second == Const(0)))
|
||||
if (modattr && (it->second == State::S0 || it->second == Const(0)))
|
||||
f << stringf(" 0 ");
|
||||
else if (modattr && (it->second == Const(1, 1) || it->second == Const(1)))
|
||||
else if (modattr && (it->second == State::S1 || it->second == Const(1)))
|
||||
f << stringf(" 1 ");
|
||||
else
|
||||
dump_const(f, it->second, -1, 0, false, as_comment);
|
||||
|
@ -551,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"));
|
||||
|
@ -583,7 +604,7 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
|
|||
return true;
|
||||
}
|
||||
|
||||
if (cell->type.substr(0, 6) == "$_DFF_")
|
||||
if (cell->type.begins_with("$_DFF_"))
|
||||
{
|
||||
std::string reg_name = cellname(cell);
|
||||
bool out_is_reg_wire = is_reg_wire(cell->getPort("\\Q"), reg_name);
|
||||
|
@ -624,7 +645,7 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
|
|||
return true;
|
||||
}
|
||||
|
||||
if (cell->type.substr(0, 8) == "$_DFFSR_")
|
||||
if (cell->type.begins_with("$_DFFSR_"))
|
||||
{
|
||||
char pol_c = cell->type[8], pol_s = cell->type[9], pol_r = cell->type[10];
|
||||
|
||||
|
@ -782,7 +803,7 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
|
|||
return true;
|
||||
}
|
||||
|
||||
if (cell->type == "$pmux" || cell->type == "$pmux_safe")
|
||||
if (cell->type == "$pmux")
|
||||
{
|
||||
int width = cell->parameters["\\WIDTH"].as_int();
|
||||
int s_width = cell->getPort("\\S").size();
|
||||
|
@ -794,18 +815,17 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
|
|||
f << stringf("%s" " input [%d:0] s;\n", indent.c_str(), s_width-1);
|
||||
|
||||
dump_attributes(f, indent + " ", cell->attributes);
|
||||
if (cell->type != "$pmux_safe" && !noattr)
|
||||
if (!noattr)
|
||||
f << stringf("%s" " (* parallel_case *)\n", indent.c_str());
|
||||
f << stringf("%s" " casez (s)", indent.c_str());
|
||||
if (cell->type != "$pmux_safe")
|
||||
f << stringf(noattr ? " // synopsys parallel_case\n" : "\n");
|
||||
f << stringf(noattr ? " // synopsys parallel_case\n" : "\n");
|
||||
|
||||
for (int i = 0; i < s_width; i++)
|
||||
{
|
||||
f << stringf("%s" " %d'b", indent.c_str(), s_width);
|
||||
|
||||
for (int j = s_width-1; j >= 0; j--)
|
||||
f << stringf("%c", j == i ? '1' : cell->type == "$pmux_safe" ? '0' : '?');
|
||||
f << stringf("%c", j == i ? '1' : '?');
|
||||
|
||||
f << stringf(":\n");
|
||||
f << stringf("%s" " %s = b[%d:%d];\n", indent.c_str(), func_name.c_str(), (i+1)*width-1, i*width);
|
||||
|
@ -929,7 +949,7 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
|
|||
return true;
|
||||
}
|
||||
|
||||
if (cell->type == "$dff" || cell->type == "$adff" || cell->type == "$dffe")
|
||||
if (cell->type.in("$dff", "$adff", "$dffe"))
|
||||
{
|
||||
RTLIL::SigSpec sig_clk, sig_arst, sig_en, val_arst;
|
||||
bool pol_clk, pol_arst = false, pol_en = false;
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue