aboutsummaryrefslogtreecommitdiffstats
path: root/backends
diff options
context:
space:
mode:
Diffstat (limited to 'backends')
-rw-r--r--backends/aiger/xaiger.cc186
-rw-r--r--backends/cxxrtl/cxxrtl.cc30
-rw-r--r--backends/firrtl/firrtl.cc63
-rw-r--r--backends/smt2/smtbmc.py6
4 files changed, 158 insertions, 127 deletions
diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc
index 1fb7210cb..6b910eecd 100644
--- a/backends/aiger/xaiger.cc
+++ b/backends/aiger/xaiger.cc
@@ -76,9 +76,11 @@ void aiger_encode(std::ostream &f, int x)
struct XAigerWriter
{
+ Design *design;
Module *module;
SigMap sigmap;
+ dict<SigBit, State> init_map;
pool<SigBit> input_bits, output_bits;
dict<SigBit, SigBit> not_map, alias_map;
dict<SigBit, pair<SigBit, SigBit>> and_map;
@@ -137,7 +139,7 @@ struct XAigerWriter
return a;
}
- XAigerWriter(Module *module, bool holes_mode=false) : module(module), sigmap(module)
+ XAigerWriter(Module *module, bool dff_mode) : design(module->design), module(module), sigmap(module)
{
pool<SigBit> undriven_bits;
pool<SigBit> unused_bits;
@@ -157,7 +159,8 @@ struct XAigerWriter
if (wire->get_bool_attribute(ID::keep))
sigmap.add(wire);
- for (auto wire : module->wires())
+ for (auto wire : module->wires()) {
+ auto it = wire->attributes.find(ID::init);
for (int i = 0; i < GetSize(wire); i++)
{
SigBit wirebit(wire, i);
@@ -174,17 +177,27 @@ struct XAigerWriter
undriven_bits.insert(bit);
unused_bits.insert(bit);
- bool scc = wire->attributes.count(ID::abc9_scc);
- if (wire->port_input || scc)
+ bool keep = wire->get_bool_attribute(ID::abc9_keep);
+ if (wire->port_input || keep)
input_bits.insert(bit);
- bool keep = wire->get_bool_attribute(ID::keep);
- if (wire->port_output || keep || scc) {
+ keep = keep || wire->get_bool_attribute(ID::keep);
+ if (wire->port_output || keep) {
if (bit != wirebit)
alias_map[wirebit] = bit;
output_bits.insert(wirebit);
}
+
+ if (it != wire->attributes.end()) {
+ auto s = it->second[i];
+ if (s != State::Sx) {
+ auto r = init_map.insert(std::make_pair(bit, it->second[i]));
+ if (!r.second && r.first->second != it->second[i])
+ log_error("Bit '%s' has a conflicting (* init *) value.\n", log_signal(bit));
+ }
+ }
}
+ }
TimingInfo timing;
@@ -212,10 +225,7 @@ struct XAigerWriter
continue;
}
- if (cell->type == ID($__ABC9_FF_) &&
- // The presence of an abc9_mergeability attribute indicates
- // that we do want to pass this flop to ABC
- cell->attributes.count(ID::abc9_mergeability))
+ if (dff_mode && cell->type.in(ID($_DFF_N_), ID($_DFF_P_)) && !cell->get_bool_attribute(ID::abc9_keep))
{
SigBit D = sigmap(cell->getPort(ID::D).as_bit());
SigBit Q = sigmap(cell->getPort(ID::Q).as_bit());
@@ -231,31 +241,29 @@ struct XAigerWriter
continue;
}
- RTLIL::Module* inst_module = module->design->module(cell->type);
- if (inst_module) {
- IdString derived_type = inst_module->derive(module->design, cell->parameters);
- inst_module = module->design->module(derived_type);
- log_assert(inst_module);
-
+ RTLIL::Module* inst_module = design->module(cell->type);
+ if (inst_module && inst_module->get_blackbox_attribute()) {
bool abc9_flop = false;
- if (!cell->has_keep_attr()) {
- auto it = cell->attributes.find(ID::abc9_box_seq);
- if (it != cell->attributes.end()) {
- int abc9_box_seq = it->second.as_int();
- if (GetSize(box_list) <= abc9_box_seq)
- box_list.resize(abc9_box_seq+1);
- box_list[abc9_box_seq] = cell;
- // Only flop boxes may have arrival times
- // (all others are combinatorial)
- abc9_flop = inst_module->get_bool_attribute(ID::abc9_flop);
- if (!abc9_flop)
- continue;
- }
+
+ auto it = cell->attributes.find(ID::abc9_box_seq);
+ if (it != cell->attributes.end()) {
+ log_assert(!cell->has_keep_attr());
+ log_assert(cell->parameters.empty());
+ int abc9_box_seq = it->second.as_int();
+ if (GetSize(box_list) <= abc9_box_seq)
+ box_list.resize(abc9_box_seq+1);
+ box_list[abc9_box_seq] = cell;
+ // Only flop boxes may have arrival times
+ // (all others are combinatorial)
+ log_assert(cell->parameters.empty());
+ abc9_flop = inst_module->get_bool_attribute(ID::abc9_flop);
+ if (!abc9_flop)
+ continue;
}
- if (!timing.count(derived_type))
+ if (!timing.count(inst_module->name))
timing.setup_module(inst_module);
- auto &t = timing.at(derived_type).arrival;
+ auto &t = timing.at(inst_module->name).arrival;
for (const auto &conn : cell->connections()) {
auto port_wire = inst_module->wire(conn.first);
if (!port_wire->port_output)
@@ -269,7 +277,7 @@ struct XAigerWriter
#ifndef NDEBUG
if (ys_debug(1)) {
static std::set<std::tuple<IdString,IdString,int>> seen;
- if (seen.emplace(derived_type, conn.first, i).second) log("%s.%s[%d] abc9_arrival = %d\n",
+ if (seen.emplace(inst_module->name, conn.first, i).second) log("%s.%s[%d] abc9_arrival = %d\n",
log_id(cell->type), log_id(conn.first), i, d);
}
#endif
@@ -280,10 +288,6 @@ struct XAigerWriter
if (abc9_flop)
continue;
}
- else {
- if (cell->type == ID($__ABC9_DELAY))
- log_error("Cell type '%s' not recognised. Check that '+/abc9_model.v' has been read.\n", cell->type.c_str());
- }
bool cell_known = inst_module || cell->known();
for (const auto &c : cell->connections()) {
@@ -317,9 +321,9 @@ struct XAigerWriter
for (auto cell : box_list) {
log_assert(cell);
- RTLIL::Module* box_module = module->design->module(cell->type);
+ RTLIL::Module* box_module = design->module(cell->type);
log_assert(box_module);
- log_assert(box_module->attributes.count(ID::abc9_box_id) || box_module->get_bool_attribute(ID::abc9_flop));
+ log_assert(box_module->has_attribute(ID::abc9_box_id));
auto r = box_ports.insert(cell->type);
if (r.second) {
@@ -383,27 +387,6 @@ struct XAigerWriter
undriven_bits.erase(O);
}
}
-
- // Connect <cell>.abc9_ff.Q (inserted by abc9_map.v) as the last input to the flop box
- if (box_module->get_bool_attribute(ID::abc9_flop)) {
- SigSpec rhs = module->wire(stringf("%s.abc9_ff.Q", cell->name.c_str()));
- if (rhs.empty())
- log_error("'%s.abc9_ff.Q' is not a wire present in module '%s'.\n", log_id(cell), log_id(module));
-
- for (auto b : rhs) {
- SigBit I = sigmap(b);
- if (b == RTLIL::Sx)
- b = State::S0;
- else if (I != b) {
- if (I == RTLIL::Sx)
- alias_map[b] = State::S0;
- else
- alias_map[b] = I;
- }
- co_bits.emplace_back(b);
- unused_bits.erase(I);
- }
- }
}
for (auto bit : input_bits)
@@ -419,16 +402,14 @@ struct XAigerWriter
undriven_bits.erase(bit);
}
- if (holes_mode) {
- struct sort_by_port_id {
- bool operator()(const RTLIL::SigBit& a, const RTLIL::SigBit& b) const {
- return a.wire->port_id < b.wire->port_id ||
- (a.wire->port_id == b.wire->port_id && a.offset < b.offset);
- }
- };
- input_bits.sort(sort_by_port_id());
- output_bits.sort(sort_by_port_id());
- }
+ struct sort_by_port_id {
+ bool operator()(const RTLIL::SigBit& a, const RTLIL::SigBit& b) const {
+ return a.wire->port_id < b.wire->port_id ||
+ (a.wire->port_id == b.wire->port_id && a.offset < b.offset);
+ }
+ };
+ input_bits.sort(sort_by_port_id());
+ output_bits.sort(sort_by_port_id());
aig_map[State::S0] = 0;
aig_map[State::S1] = 1;
@@ -589,17 +570,14 @@ struct XAigerWriter
int box_count = 0;
for (auto cell : box_list) {
log_assert(cell);
+ log_assert(cell->parameters.empty());
- RTLIL::Module* box_module = module->design->module(cell->type);
- log_assert(box_module);
-
- IdString derived_type = box_module->derive(box_module->design, cell->parameters);
- box_module = box_module->design->module(derived_type);
- log_assert(box_module);
-
- auto r = cell_cache.insert(derived_type);
+ auto r = cell_cache.insert(cell->type);
auto &v = r.first->second;
if (r.second) {
+ RTLIL::Module* box_module = design->module(cell->type);
+ log_assert(box_module);
+
int box_inputs = 0, box_outputs = 0;
for (auto port_name : box_module->ports) {
RTLIL::Wire *w = box_module->wire(port_name);
@@ -610,11 +588,6 @@ struct XAigerWriter
box_outputs += GetSize(w);
}
- // For flops only, create an extra 1-bit input that drives a new wire
- // called "<cell>.abc9_ff.Q" that is used below
- if (box_module->get_bool_attribute(ID::abc9_flop))
- box_inputs++;
-
std::get<0>(v) = box_inputs;
std::get<1>(v) = box_outputs;
std::get<2>(v) = box_module->attributes.at(ID::abc9_box_id).as_int();
@@ -635,23 +608,27 @@ struct XAigerWriter
auto write_s_buffer = std::bind(write_buffer, std::ref(s_buffer), std::placeholders::_1);
write_s_buffer(ff_bits.size());
+ dict<SigSpec, int> clk_to_mergeability;
for (const auto &i : ff_bits) {
const SigBit &d = i.first;
const Cell *cell = i.second;
- int mergeability = cell->attributes.at(ID::abc9_mergeability).as_int();
+ SigSpec clk_and_pol{sigmap(cell->getPort(ID::C)), cell->type[6] == 'P' ? State::S1 : State::S0};
+ auto r = clk_to_mergeability.insert(std::make_pair(clk_and_pol, clk_to_mergeability.size()+1));
+ int mergeability = r.first->second;
log_assert(mergeability > 0);
write_r_buffer(mergeability);
- Const init = cell->attributes.at(ID::abc9_init, State::Sx);
- log_assert(GetSize(init) == 1);
+ SigBit Q = sigmap(cell->getPort(ID::Q));
+ State init = init_map.at(Q, State::Sx);
+ log_debug("Cell '%s' (type %s) has (* init *) value '%s'.\n", log_id(cell), log_id(cell->type), log_signal(init));
if (init == State::S1)
write_s_buffer(1);
else if (init == State::S0)
write_s_buffer(0);
else {
log_assert(init == State::Sx);
- write_s_buffer(0);
+ write_s_buffer(2);
}
// Use arrival time from output of flop box
@@ -671,10 +648,16 @@ struct XAigerWriter
f.write(reinterpret_cast<const char*>(&buffer_size_be), sizeof(buffer_size_be));
f.write(buffer_str.data(), buffer_str.size());
- RTLIL::Module *holes_module = module->design->module(stringf("%s$holes", module->name.c_str()));
+ RTLIL::Design *holes_design;
+ auto it = saved_designs.find("$abc9_holes");
+ if (it != saved_designs.end())
+ holes_design = it->second;
+ else
+ holes_design = nullptr;
+ RTLIL::Module *holes_module = holes_design ? holes_design->module(module->name) : nullptr;
if (holes_module) {
std::stringstream a_buffer;
- XAigerWriter writer(holes_module, true /* holes_mode */);
+ XAigerWriter writer(holes_module, false /* dff_mode */);
writer.write_aiger(a_buffer, false /*ascii_mode*/);
f << "a";
@@ -704,10 +687,10 @@ struct XAigerWriter
f << stringf("Generated by %s\n", yosys_version_str);
- module->design->scratchpad_set_int("write_xaiger.num_ands", and_map.size());
- module->design->scratchpad_set_int("write_xaiger.num_wires", aig_map.size());
- module->design->scratchpad_set_int("write_xaiger.num_inputs", input_bits.size());
- module->design->scratchpad_set_int("write_xaiger.num_outputs", output_bits.size());
+ design->scratchpad_set_int("write_xaiger.num_ands", and_map.size());
+ design->scratchpad_set_int("write_xaiger.num_wires", aig_map.size());
+ design->scratchpad_set_int("write_xaiger.num_inputs", input_bits.size());
+ design->scratchpad_set_int("write_xaiger.num_outputs", output_bits.size());
}
void write_map(std::ostream &f)
@@ -761,10 +744,10 @@ struct XAigerBackend : public Backend {
log(" write_xaiger [options] [filename]\n");
log("\n");
log("Write the top module (according to the (* top *) attribute or if only one module\n");
- log("is currently selected) to an XAIGER file. Any non $_NOT_, $_AND_, $_ABC9_FF_, or");
- log("non (* abc9_box_id *) cells will be converted into psuedo-inputs and\n");
- log("pseudo-outputs. Whitebox contents will be taken from the '<module-name>$holes'\n");
- log("module, if it exists.\n");
+ log("is currently selected) to an XAIGER file. Any non $_NOT_, $_AND_, (optionally\n");
+ log("$_DFF_N_, $_DFF_P_), or non (* abc9_box *) cells will be converted into psuedo-\n");
+ log("inputs and pseudo-outputs. Whitebox contents will be taken from the equivalent\n");
+ log("module in the '$abc9_holes' design, if it exists.\n");
log("\n");
log(" -ascii\n");
log(" write ASCII version of AIGER format\n");
@@ -772,10 +755,13 @@ struct XAigerBackend : public Backend {
log(" -map <filename>\n");
log(" write an extra file with port and box symbols\n");
log("\n");
+ log(" -dff\n");
+ log(" write $_DFF_[NP]_ cells\n");
+ log("\n");
}
void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
{
- bool ascii_mode = false;
+ bool ascii_mode = false, dff_mode = false;
std::string map_filename;
log_header(design, "Executing XAIGER backend.\n");
@@ -791,6 +777,10 @@ struct XAigerBackend : public Backend {
map_filename = args[++argidx];
continue;
}
+ if (args[argidx] == "-dff") {
+ dff_mode = true;
+ continue;
+ }
break;
}
extra_args(f, filename, args, argidx, !ascii_mode);
@@ -808,7 +798,7 @@ struct XAigerBackend : public Backend {
if (!top_module->memories.empty())
log_error("Found unmapped memories in module %s: unmapped memories are not supported in XAIGER backend!\n", log_id(top_module));
- XAigerWriter writer(top_module);
+ XAigerWriter writer(top_module, dff_mode);
writer.write_aiger(*f, ascii_mode);
if (!map_filename.empty()) {
diff --git a/backends/cxxrtl/cxxrtl.cc b/backends/cxxrtl/cxxrtl.cc
index f3ed3f623..0cceecbba 100644
--- a/backends/cxxrtl/cxxrtl.cc
+++ b/backends/cxxrtl/cxxrtl.cc
@@ -513,7 +513,6 @@ struct CxxrtlWorker {
bool elide_public = false;
bool localize_internal = false;
bool localize_public = false;
- bool run_opt_clean_purge = false;
bool run_proc_flatten = false;
bool max_opt_level = false;
@@ -2009,6 +2008,7 @@ struct CxxrtlWorker {
log("Module `%s' contains feedback arcs through wires:\n", log_id(module));
for (auto wire : feedback_wires)
log(" %s\n", log_id(wire));
+ log("\n");
}
for (auto wire : module->wires()) {
@@ -2040,20 +2040,20 @@ struct CxxrtlWorker {
log("Module `%s' contains buffered combinatorial wires:\n", log_id(module));
for (auto wire : buffered_wires)
log(" %s\n", log_id(wire));
+ log("\n");
}
eval_converges[module] = feedback_wires.empty() && buffered_wires.empty();
}
if (has_feedback_arcs || has_buffered_wires) {
// Although both non-feedback buffered combinatorial wires and apparent feedback wires may be eliminated
- // by optimizing the design, if after `opt_clean -purge` there are any feedback wires remaining, it is very
+ // by optimizing the design, if after `proc; flatten` there are any feedback wires remaining, it is very
// likely that these feedback wires are indicative of a true logic loop, so they get emphasized in the message.
const char *why_pessimistic = nullptr;
if (has_feedback_arcs)
why_pessimistic = "feedback wires";
else if (has_buffered_wires)
why_pessimistic = "buffered combinatorial wires";
- log("\n");
log_warning("Design contains %s, which require delta cycles during evaluation.\n", why_pessimistic);
if (!max_opt_level)
log("Increasing the optimization level may eliminate %s from the design.\n", why_pessimistic);
@@ -2087,34 +2087,39 @@ struct CxxrtlWorker {
void prepare_design(RTLIL::Design *design)
{
+ bool did_anything = false;
bool has_sync_init, has_packed_mem;
log_push();
check_design(design, has_sync_init, has_packed_mem);
if (run_proc_flatten) {
Pass::call(design, "proc");
Pass::call(design, "flatten");
+ did_anything = true;
} else if (has_sync_init) {
// We're only interested in proc_init, but it depends on proc_prune and proc_clean, so call those
// in case they weren't already. (This allows `yosys foo.v -o foo.cc` to work.)
Pass::call(design, "proc_prune");
Pass::call(design, "proc_clean");
Pass::call(design, "proc_init");
+ did_anything = true;
}
- if (has_packed_mem)
+ if (has_packed_mem) {
Pass::call(design, "memory_unpack");
+ did_anything = true;
+ }
// Recheck the design if it was modified.
if (has_sync_init || has_packed_mem)
check_design(design, has_sync_init, has_packed_mem);
log_assert(!(has_sync_init || has_packed_mem));
- if (run_opt_clean_purge)
- Pass::call(design, "opt_clean -purge");
log_pop();
+ if (did_anything)
+ log_spacer();
analyze_design(design);
}
};
struct CxxrtlBackend : public Backend {
- static const int DEFAULT_OPT_LEVEL = 6;
+ static const int DEFAULT_OPT_LEVEL = 5;
CxxrtlBackend() : Backend("cxxrtl", "convert design to C++ RTL simulation") { }
void help() YS_OVERRIDE
@@ -2306,10 +2311,7 @@ struct CxxrtlBackend : public Backend {
log(" like -O3, and localize public wires not marked (*keep*) if possible.\n");
log("\n");
log(" -O5\n");
- log(" like -O4, and run `opt_clean -purge` first.\n");
- log("\n");
- log(" -O6\n");
- log(" like -O5, and run `proc; flatten` first.\n");
+ log(" like -O4, and run `proc; flatten` first.\n");
log("\n");
}
void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
@@ -2343,13 +2345,11 @@ struct CxxrtlBackend : public Backend {
extra_args(f, filename, args, argidx);
switch (opt_level) {
- case 6:
+ // the highest level here must match DEFAULT_OPT_LEVEL
+ case 5:
worker.max_opt_level = true;
worker.run_proc_flatten = true;
YS_FALLTHROUGH
- case 5:
- worker.run_opt_clean_purge = true;
- YS_FALLTHROUGH
case 4:
worker.localize_public = true;
YS_FALLTHROUGH
diff --git a/backends/firrtl/firrtl.cc b/backends/firrtl/firrtl.cc
index f6dae1d8c..a90b0b87a 100644
--- a/backends/firrtl/firrtl.cc
+++ b/backends/firrtl/firrtl.cc
@@ -392,7 +392,34 @@ struct FirrtlWorker
return result;
}
- void run()
+ void emit_extmodule()
+ {
+ std::string moduleFileinfo = getFileinfo(module);
+ f << stringf(" extmodule %s: %s\n", make_id(module->name), moduleFileinfo.c_str());
+ vector<std::string> port_decls;
+
+ for (auto wire : module->wires())
+ {
+ const auto wireName = make_id(wire->name);
+ std::string wireFileinfo = getFileinfo(wire);
+
+ if (wire->port_input && wire->port_output)
+ {
+ log_error("Module port %s.%s is inout!\n", log_id(module), log_id(wire));
+ }
+ port_decls.push_back(stringf(" %s %s: UInt<%d> %s\n", wire->port_input ? "input" : "output",
+ wireName, wire->width, wireFileinfo.c_str()));
+ }
+
+ for (auto &str : port_decls)
+ {
+ f << str;
+ }
+
+ f << stringf("\n");
+ }
+
+ void emit_module()
{
std::string moduleFileinfo = getFileinfo(module);
f << stringf(" module %s: %s\n", make_id(module->name), moduleFileinfo.c_str());
@@ -446,7 +473,7 @@ struct FirrtlWorker
string y_id = make_id(cell->name);
std::string cellFileinfo = getFileinfo(cell);
- if (cell->type.in(ID($not), ID($logic_not), ID($neg), ID($reduce_and), ID($reduce_or), ID($reduce_xor), ID($reduce_bool), ID($reduce_xnor)))
+ if (cell->type.in(ID($not), ID($logic_not), ID($_NOT_), ID($neg), ID($reduce_and), ID($reduce_or), ID($reduce_xor), ID($reduce_bool), ID($reduce_xnor)))
{
string a_expr = make_expr(cell->getPort(ID::A));
wire_decls.push_back(stringf(" wire %s: UInt<%d> %s\n", y_id.c_str(), y_width, cellFileinfo.c_str()));
@@ -462,7 +489,7 @@ struct FirrtlWorker
// Assume the FIRRTL width is a single bit.
firrtl_width = 1;
- if (cell->type == ID($not)) primop = "not";
+ if (cell->type.in(ID($not), ID($_NOT_))) primop = "not";
else if (cell->type == ID($neg)) {
primop = "neg";
firrtl_is_signed = true; // Result of "neg" is signed (an SInt).
@@ -494,7 +521,7 @@ struct FirrtlWorker
continue;
}
- if (cell->type.in(ID($add), ID($sub), ID($mul), ID($div), ID($mod), ID($xor), ID($xnor), ID($and), ID($or), ID($eq), ID($eqx),
+ if (cell->type.in(ID($add), ID($sub), ID($mul), ID($div), ID($mod), ID($xor), ID($_XOR_), ID($xnor), ID($and), ID($_AND_), ID($or), ID($_OR_), ID($eq), ID($eqx),
ID($gt), ID($ge), ID($lt), ID($le), ID($ne), ID($nex), ID($shr), ID($sshr), ID($sshl), ID($shl),
ID($logic_and), ID($logic_or), ID($pow)))
{
@@ -524,7 +551,7 @@ struct FirrtlWorker
// 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(ID($add), ID($sub), ID($mul), ID($div), ID($mod), ID($xor), ID($xnor), ID($and), ID($or)))
+ if (cell->type.in(ID($add), ID($sub), ID($mul), ID($div), ID($mod), ID($xor), ID($_XOR_), ID($xnor), ID($and), ID($_AND_), ID($or), ID($_OR_)))
{
if (a_width < y_width) {
a_expr = stringf("pad(%s, %d)", a_expr.c_str(), y_width);
@@ -560,17 +587,17 @@ struct FirrtlWorker
} else if (cell->type == ID($mod)) {
primop = "rem";
firrtl_width = min(a_width, b_width);
- } else if (cell->type == ID($and)) {
+ } else if (cell->type.in(ID($and), ID($_AND_))) {
primop = "and";
always_uint = true;
firrtl_width = max(a_width, b_width);
}
- else if (cell->type == ID($or) ) {
+ else if (cell->type.in(ID($or), ID($_OR_))) {
primop = "or";
always_uint = true;
firrtl_width = max(a_width, b_width);
}
- else if (cell->type == ID($xor)) {
+ else if (cell->type.in(ID($xor), ID($_XOR_))) {
primop = "xor";
always_uint = true;
firrtl_width = max(a_width, b_width);
@@ -694,7 +721,8 @@ struct FirrtlWorker
}
}
- if (!cell->parameters.at(ID::B_SIGNED).as_bool()) {
+ auto it = cell->parameters.find(ID::B_SIGNED);
+ if (it == cell->parameters.end() || !it->second.as_bool()) {
b_expr = "asUInt(" + b_expr + ")";
}
@@ -723,9 +751,10 @@ struct FirrtlWorker
continue;
}
- if (cell->type.in(ID($mux)))
+ if (cell->type.in(ID($mux), ID($_MUX_)))
{
- int width = cell->parameters.at(ID::WIDTH).as_int();
+ auto it = cell->parameters.find(ID::WIDTH);
+ int width = it == cell->parameters.end()? 1 : it->second.as_int();
string a_expr = make_expr(cell->getPort(ID::A));
string b_expr = make_expr(cell->getPort(ID::B));
string s_expr = make_expr(cell->getPort(ID::S));
@@ -1076,6 +1105,18 @@ struct FirrtlWorker
for (auto str : wire_exprs)
f << str;
+
+ f << stringf("\n");
+ }
+
+ void run()
+ {
+ // Blackboxes should be emitted as `extmodule`s in firrtl. Only ports are
+ // emitted in such a case.
+ if (module->get_blackbox_attribute())
+ emit_extmodule();
+ else
+ emit_module();
}
};
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index d3015b066..cc3ebb129 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -1511,7 +1511,7 @@ else: # not tempind, covermode
smt_assert_consequent(get_constr_expr(constr_assumes, i))
print_msg("Re-solving with appended steps..")
if smt_check_sat() == "unsat":
- print("%s Cannot appended steps without violating assumptions!" % smt.timestamp())
+ print("%s Cannot append steps without violating assumptions!" % smt.timestamp())
retstatus = "FAILED"
break
print_anyconsts(step)
@@ -1548,7 +1548,7 @@ else: # not tempind, covermode
break
smt_pop()
- if not retstatus:
+ if retstatus == "FAILED" or retstatus == "PREUNSAT":
break
else: # gentrace
@@ -1568,7 +1568,7 @@ else: # not tempind, covermode
step += step_size
- if gentrace and retstatus:
+ if gentrace and retstatus == "PASSED":
print_anyconsts(0)
write_trace(0, num_steps, '%')
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-06 08:20:51 +0000