diff --git a/Makefile b/Makefile index 51ef2ec3b..42f534a71 100644 --- a/Makefile +++ b/Makefile @@ -180,7 +180,7 @@ ifeq ($(OS), Haiku) CXXFLAGS += -D_DEFAULT_SOURCE endif -YOSYS_VER := 0.57+218 +YOSYS_VER := 0.57+244 YOSYS_MAJOR := $(shell echo $(YOSYS_VER) | cut -d'.' -f1) YOSYS_MINOR := $(shell echo $(YOSYS_VER) | cut -d'.' -f2) YOSYS_COMMIT := $(shell echo $(YOSYS_VER) | cut -d'.' -f3) diff --git a/backends/aiger2/aiger.cc b/backends/aiger2/aiger.cc index 87cdc17c3..7af6c23cb 100644 --- a/backends/aiger2/aiger.cc +++ b/backends/aiger2/aiger.cc @@ -105,6 +105,13 @@ struct Index { if (allow_blackboxes) { info.found_blackboxes.insert(cell); } else { + // Even if we don't allow blackboxes these might still be + // present outside of any traversed input cones, so we + // can't bail at this point. If they are hit by a traversal + // (which can only really happen with $tribuf not + // $connect), we can still detect this as an error later. + if (cell->type == ID($connect) || (cell->type == ID($tribuf) && cell->has_attribute(ID(aiger2_zbuf)))) + continue; if (!submodule || submodule->get_blackbox_attribute()) log_warning("Unsupported cell type: %s (%s in %s)\n", log_id(cell->type), log_id(cell), log_id(m)); @@ -483,7 +490,8 @@ struct Index { { Design *design = index.design; auto &minfo = leaf_minfo(index); - log_assert(minfo.suboffsets.count(cell)); + if (!minfo.suboffsets.count(cell)) + log_error("Reached unsupport cell %s (%s in %s)\n", log_id(cell->type), log_id(cell), log_id(cell->module)); Module *def = design->module(cell->type); log_assert(def); levels.push_back(Level(index.modules.at(def), cell)); diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index 48ab2590d..c25401e9c 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -205,8 +205,8 @@ YosysStreamCallBackHandler verific_read_cb; // ================================================================== -VerificImporter::VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_names, bool mode_verific, bool mode_autocover, bool mode_fullinit) : - mode_gates(mode_gates), mode_keep(mode_keep), mode_nosva(mode_nosva), +VerificImporter::VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_sva_continue, bool mode_names, bool mode_verific, bool mode_autocover, bool mode_fullinit) : + mode_gates(mode_gates), mode_keep(mode_keep), mode_nosva(mode_nosva), mode_sva_continue(mode_sva_continue), mode_names(mode_names), mode_verific(mode_verific), mode_autocover(mode_autocover), mode_fullinit(mode_fullinit) { @@ -2374,6 +2374,12 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::ma wire->attributes.erase(ID::init); } } + + if (num_sva_continue) { + log_warning("Encountered %d items containing unsupported SVA!\n", num_sva_continue); + log_warning("Unsupported SVA imported as 'x and marked using the `unsupported_sva' attribute due to -sva-continue-on-err.\n"); + } + num_sva_continue = 0; } // ================================================================== @@ -3132,7 +3138,7 @@ std::string verific_import(Design *design, const std::mapfirst) == 0) { - VerificImporter importer(false, false, false, false, false, false, false); + VerificImporter importer(false, false, false, false, false, false, false, false); nl_done[it->first] = it->second; importer.import_netlist(design, nl, nl_todo, top_mod_names.count(nl->CellBaseName())); } @@ -3369,6 +3375,11 @@ struct VerificPass : public Pass { log(" -nosva\n"); log(" Ignore SVA properties, do not infer checker logic.\n"); log("\n"); + log(" -sva-continue-on-err\n"); + log(" Turns unsupported SVA from an error into a warning. Properties are imported\n"); + log(" with their trigger condition replaced with 'x and with an `unsupported_sva'\n"); + log(" attribute to produce a later error in SBY if they remain in the design.\n"); + log("\n"); log(" -L \n"); log(" Maximum number of ctrl bits for SVA checker FSMs (default=16).\n"); log("\n"); @@ -4234,7 +4245,8 @@ struct VerificPass : public Pass { { std::map nl_todo, nl_done; bool mode_all = false, mode_gates = false, mode_keep = false; - bool mode_nosva = false, mode_names = false, mode_verific = false; + bool mode_nosva = false, mode_sva_continue = false; + bool mode_names = false, mode_verific = false; bool mode_autocover = false, mode_fullinit = false; bool flatten = false, extnets = false, mode_cells = false; bool split_complex_ports = true; @@ -4272,6 +4284,10 @@ struct VerificPass : public Pass { mode_nosva = true; continue; } + if (args[argidx] == "-sva-continue-on-err") { + mode_sva_continue = true; + continue; + } if (args[argidx] == "-L" && argidx+1 < GetSize(args)) { verific_sva_fsm_limit = atoi(args[++argidx].c_str()); continue; @@ -4402,7 +4418,7 @@ struct VerificPass : public Pass { auto it = nl_todo.begin(); Netlist *nl = it->second; if (nl_done.count(it->first) == 0) { - VerificImporter importer(mode_gates, mode_keep, mode_nosva, + VerificImporter importer(mode_gates, mode_keep, mode_nosva, mode_sva_continue, mode_names, mode_verific, mode_autocover, mode_fullinit); nl_done[it->first] = it->second; importer.import_netlist(design, nl, nl_todo, top_mod_names.count(nl->CellBaseName())); diff --git a/frontends/verific/verific.h b/frontends/verific/verific.h index 6c05ad837..3d7e9c241 100644 --- a/frontends/verific/verific.h +++ b/frontends/verific/verific.h @@ -77,10 +77,12 @@ struct VerificImporter std::map sva_posedge_map; pool any_all_nets; - bool mode_gates, mode_keep, mode_nosva, mode_names, mode_verific; + bool mode_gates, mode_keep, mode_nosva, mode_sva_continue, mode_names, mode_verific; bool mode_autocover, mode_fullinit; - VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_names, bool mode_verific, bool mode_autocover, bool mode_fullinit); + int num_sva_continue = 0; + + VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_sva_continue, bool mode_names, bool mode_verific, bool mode_autocover, bool mode_fullinit); RTLIL::SigBit net_map_at(Verific::Net *net); diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc index 3908947eb..50e0049ae 100644 --- a/frontends/verific/verificsva.cc +++ b/frontends/verific/verificsva.cc @@ -124,6 +124,7 @@ struct SvaFsm { Module *module; VerificClocking clocking; + std::function parser_error; SigBit trigger_sig = State::S1, disable_sig; SigBit throughout_sig = State::S1; @@ -148,6 +149,7 @@ struct SvaFsm module = clking.module; clocking = clking; trigger_sig = trig; + parser_error = [](std::string msg){ log_error("%s", msg); }; startNode = createNode(); acceptNode = createNode(); @@ -475,8 +477,8 @@ struct SvaFsm dump(); log(" ctrl signal: %s\n", log_signal(dnode.ctrl)); } - log_error("SVA DFSM state ctrl signal has %d (>%d) bits. Stopping to prevent exponential design size explosion.\n", - GetSize(dnode.ctrl), verific_sva_fsm_limit); + parser_error(stringf("SVA DFSM state ctrl signal has %d (>%d) bits. Stopping to prevent exponential design size explosion.\n", + GetSize(dnode.ctrl), verific_sva_fsm_limit)); } for (unsigned long long i = 0; i < (1ull << GetSize(dnode.ctrl)); i++) @@ -1023,7 +1025,7 @@ struct VerificSvaImporter [[noreturn]] void parser_error(std::string errmsg) { - if (!importer->mode_keep) + if (!importer->mode_keep && !importer->mode_sva_continue) log_error("%s", errmsg); log_warning("%s", errmsg); throw ParserErrorException(); @@ -1260,6 +1262,7 @@ struct VerificSvaImporter if (inst->Type() == PRIM_SVA_FIRST_MATCH) { SvaFsm match_fsm(clocking); + match_fsm.parser_error = [&](std::string msg) { this->parser_error(msg); }; match_fsm.createLink(parse_sequence(match_fsm, match_fsm.createStartNode(), inst->GetInput()), match_fsm.acceptNode); int node = fsm.createNode(); @@ -1426,12 +1429,15 @@ struct VerificSvaImporter if (inst->Type() == PRIM_SVA_SEQ_AND || inst->Type() == PRIM_SVA_AND) { SvaFsm fsm1(clocking); + fsm1.parser_error = [&](std::string msg) { this->parser_error(msg); }; fsm1.createLink(parse_sequence(fsm1, fsm1.createStartNode(), inst->GetInput1()), fsm1.acceptNode); SvaFsm fsm2(clocking); + fsm2.parser_error = [&](std::string msg) { this->parser_error(msg); }; fsm2.createLink(parse_sequence(fsm2, fsm2.createStartNode(), inst->GetInput2()), fsm2.acceptNode); SvaFsm combined_fsm(clocking); + combined_fsm.parser_error = [&](std::string msg) { this->parser_error(msg); }; fsm1.getDFsm(combined_fsm, combined_fsm.createStartNode(), -1, combined_fsm.acceptNode); fsm2.getDFsm(combined_fsm, combined_fsm.createStartNode(), -1, combined_fsm.acceptNode); @@ -1456,6 +1462,7 @@ struct VerificSvaImporter if (inst->Type() == PRIM_SVA_INTERSECT || inst->Type() == PRIM_SVA_WITHIN) { SvaFsm intersect_fsm(clocking); + intersect_fsm.parser_error = [&](std::string msg) { this->parser_error(msg); }; if (inst->Type() == PRIM_SVA_INTERSECT) { @@ -1562,6 +1569,7 @@ struct VerificSvaImporter int node; SvaFsm antecedent_fsm(clocking, trig); + antecedent_fsm.parser_error = [&](std::string msg) { this->parser_error(msg); }; node = parse_sequence(antecedent_fsm, antecedent_fsm.createStartNode(), antecedent_net); if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION) { int next_node = antecedent_fsm.createNode(); @@ -1623,6 +1631,7 @@ struct VerificSvaImporter int node; SvaFsm antecedent_fsm(clocking, trig); + antecedent_fsm.parser_error = [&](std::string msg) { this->parser_error(msg); }; node = parse_sequence(antecedent_fsm, antecedent_fsm.createStartNode(), antecedent_net); if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION || inst->Type() == PRIM_SVA_NON_OVERLAPPED_FOLLOWED_BY) { int next_node = antecedent_fsm.createNode(); @@ -1677,6 +1686,7 @@ struct VerificSvaImporter } SvaFsm consequent_fsm(clocking, antecedent_match); + consequent_fsm.parser_error = [&](std::string msg) { this->parser_error(msg); }; node = parse_sequence(consequent_fsm, consequent_fsm.createStartNode(), consequent_net); consequent_fsm.createLink(node, consequent_fsm.acceptNode); @@ -1696,6 +1706,7 @@ struct VerificSvaImporter } SvaFsm fsm(clocking, trig); + fsm.parser_error = [&](std::string msg) { this->parser_error(msg); }; int node = parse_sequence(fsm, fsm.createStartNode(), net); fsm.createLink(node, fsm.acceptNode); @@ -1710,30 +1721,34 @@ struct VerificSvaImporter void import() { - try - { - module = importer->module; - netlist = root->Owner(); + module = importer->module; + netlist = root->Owner(); - if (verific_verbose) - log(" importing SVA property at root cell %s (%s) at %s:%d.\n", root->Name(), root->View()->Owner()->Name(), - LineFile::GetFileName(root->Linefile()), LineFile::GetLineNo(root->Linefile())); + int initial_cell_count = GetSize(module->cells_); + int initial_wire_count = GetSize(module->wires_); + int initial_connection_count = GetSize(module->connections_); - bool is_user_declared = root->IsUserDeclared(); + if (verific_verbose) + log(" importing SVA property at root cell %s (%s) at %s:%d.\n", root->Name(), root->View()->Owner()->Name(), + LineFile::GetFileName(root->Linefile()), LineFile::GetLineNo(root->Linefile())); - // FIXME - if (!is_user_declared) { - const char *name = root->Name(); - for (int i = 0; name[i]; i++) { - if (i ? (name[i] < '0' || name[i] > '9') : (name[i] != 'i')) { - is_user_declared = true; - break; - } + bool is_user_declared = root->IsUserDeclared(); + + // FIXME + if (!is_user_declared) { + const char *name = root->Name(); + for (int i = 0; name[i]; i++) { + if (i ? (name[i] < '0' || name[i] > '9') : (name[i] != 'i')) { + is_user_declared = true; + break; } } + } - RTLIL::IdString root_name = module->uniquify(importer->mode_names || is_user_declared ? RTLIL::escape_id(root->Name()) : NEW_ID); + RTLIL::IdString root_name = module->uniquify(importer->mode_names || is_user_declared ? RTLIL::escape_id(root->Name()) : NEW_ID); + try + { // parse SVA sequence into trigger signal clocking = VerificClocking(importer, root->GetInput(), true); @@ -1836,6 +1851,36 @@ struct VerificSvaImporter } catch (ParserErrorException) { + if (importer->mode_sva_continue) { + + std::vector remove_cells; + pool remove_wires; + + for (int i = 0, end = GetSize(module->cells_) - initial_cell_count; i != end; ++i) + remove_cells.push_back(module->cells_.element(i)->second); + + for (int i = 0, end = GetSize(module->wires_) - initial_wire_count; i != end; ++i) + remove_wires.emplace(module->wires_.element(i)->second); + + for (auto cell : remove_cells) + module->remove(cell); + module->remove(remove_wires); + + module->connections_.resize(initial_connection_count); + + RTLIL::Cell *c = nullptr; + + if (mode_assert) c = module->addAssert(root_name, State::Sx, State::Sx); + if (mode_assume) c = module->addAssume(root_name, State::Sx, State::Sx); + if (mode_cover) c = module->addCover(root_name, State::Sx, State::Sx); + + if (c) { + importer->import_attributes(c->attributes, root); + c->set_bool_attribute(ID(unsupported_sva)); + } + + importer->num_sva_continue++; + } } } }; diff --git a/kernel/rtlil.cc b/kernel/rtlil.cc index 1be54dca1..4525d7a44 100644 --- a/kernel/rtlil.cc +++ b/kernel/rtlil.cc @@ -2845,6 +2845,13 @@ void RTLIL::Module::remove(const pool &wires) delete_wire_worker.wires_p = &wires; rewrite_sigspecs2(delete_wire_worker); + if (design->flagBufferedNormalized) { + for (auto wire : wires) { + buf_norm_wire_queue.erase(wire); + buf_norm_connect_index.erase(wire); + } + } + for (auto &it : wires) { log_assert(wires_.count(it->name) != 0); wires_.erase(it->name); diff --git a/kernel/rtlil_bufnorm.cc b/kernel/rtlil_bufnorm.cc index 6d619d9e6..d0561f880 100644 --- a/kernel/rtlil_bufnorm.cc +++ b/kernel/rtlil_bufnorm.cc @@ -43,6 +43,7 @@ void RTLIL::Design::bufNormalize(bool enable) wire->driverCell_ = nullptr; wire->driverPort_ = IdString(); } + module->buf_norm_connect_index.clear(); } flagBufferedNormalized = false; @@ -126,15 +127,19 @@ void RTLIL::Module::bufNormalize() idict wire_queue_entries; // Ordered queue of wires to process int wire_queue_pos = 0; // Index up to which we processed the wires - // Wires with their unique driving cell port. If we know a wire is - // driven by multiple (potential) drivers, this is indicated by a - // nullptr as cell. + // Wires with their unique driving cell port. We pick the first driver + // we encounter, with the exception that we ensure that a module input + // port can only get $input_port drivers and that $input_port drivers + // cannot drive any other modules. If we reject an $input_port driver + // because it's not driving an input port or because there already is + // another $input_port driver for the same port, we also delete that + // $input_port cell. dict> direct_driven_wires; - // Set of non-unique or driving cell ports for each processed wire. - dict>> direct_driven_wires_conflicts; - - // Set of cell ports that need a fresh intermediate wire. + // Set of cell ports that need a fresh intermediate wire. These are all + // cell ports that drive non-full-wire sigspecs, cell ports driving + // module input ports, and cell ports driving wires that are already + // driven. pool> pending_ports; // This helper will be called for every output/inout cell port that is @@ -149,27 +154,14 @@ void RTLIL::Module::bufNormalize() SigSpec const &sig = cell->getPort(port); - if (cell->type == ID($input_port)) { - // If an `$input_port` cell isn't fully connected to a full - // input port wire, we remove it since the wires are still the - // canonical source of module ports and the `$input_port` cells - // are just helpers to simplfiy the bufnorm invariant. - log_assert(port == ID::Y); - if (!sig.is_wire()) { - buf_norm_cell_queue.insert(cell); - remove(cell); - return; - } - Wire *w = sig.as_wire(); - if (!w->port_input || w->port_output) { - buf_norm_cell_queue.insert(cell); - remove(cell); - return; - } - w->driverCell_ = cell; - w->driverPort_ = ID::Y; - } else if (cell->type == ID($buf) && cell->attributes.empty() && !cell->name.isPublic()) { + // Make sure all wires of the cell port are enqueued, ensuring we + // detect other connected drivers (output and inout). + for (auto chunk : sig.chunks()) + if (chunk.is_wire()) + wire_queue_entries(chunk.wire); + + if (cell->type == ID($buf) && cell->attributes.empty() && !cell->name.isPublic()) { // For a plain `$buf` cell, we enqueue all wires on its input // side, bypass it using module level connections (skipping 'z // bits) and then remove the cell. Eventually the module level @@ -206,47 +198,40 @@ void RTLIL::Module::bufNormalize() if (!sig_y.empty()) connect(sig_y, sig_a); + remove(cell); + log_assert(GetSize(buf_norm_wire_queue) <= 1); + buf_norm_wire_queue.clear(); + return; + } else if (cell->type == ID($input_port)) { + log_assert(port == ID::Y); + if (sig.is_wire()) { + Wire *w = sig.as_wire(); + if (w->port_input && !w->port_output) { + // An $input_port cell can only drive a full wire module input port + auto [found, inserted] = direct_driven_wires.emplace(w, {cell, port}); + if (!inserted || (found->second.first == cell && found->second.second == port)) + return; + } + } + + // If an `$input_port` cell isn't driving a full + // input port wire, we remove it since the wires are still the + // canonical source of module ports + buf_norm_cell_queue.insert(cell); remove(cell); + log_assert(GetSize(buf_norm_wire_queue) <= 1); + buf_norm_wire_queue.clear(); return; } - // Make sure all wires of the cell port are enqueued, ensuring we - // detect other connected drivers (output and inout). - for (auto const &chunk : sig.chunks()) - if (chunk.wire) - wire_queue_entries(chunk.wire); - if (sig.is_wire()) { - // If the full cell port is connected to a full wire, we might be - // able to keep that connection if this is a unique output port driving that wire Wire *w = sig.as_wire(); - - // We try to store the current port as unique driver, if this - // succeeds we're done with the port. - auto [found, inserted] = direct_driven_wires.emplace(w, {cell, port}); - if (inserted || (found->second.first == cell && found->second.second == port)) - return; - - // When this failed, we store this port as a conflict. If we - // had already stored a candidate for a unique driver, we also - // move it to the conflicts, leaving a nullptr marker. - - auto &conflicts = direct_driven_wires_conflicts[w]; - if (Cell *other_cell = found->second.first) { - if (other_cell->type == ID($input_port)) { - // Multiple input port cells - log_assert(cell->type != ID($input_port)); - } else { - pending_ports.insert(found->second); - conflicts.emplace(found->second); - found->second = {nullptr, {}}; - } - } - if (cell->type == ID($input_port)) { - found->second = {cell, port}; - } else { - conflicts.emplace(cell, port); + if (!w->port_input || w->port_output) { + // If the full cell port is connected to a full non-input-port wire, pick it as driver + auto [found, inserted] = direct_driven_wires.emplace(w, {cell, port}); + if (inserted || (found->second.first == cell && found->second.second == port)) + return; } } @@ -256,16 +241,22 @@ void RTLIL::Module::bufNormalize() pending_ports.emplace(cell, port); }; + // We enqueue all enqueued wires for `$buf`/`$connect` processing (clearing the module level queue). + for (auto wire : buf_norm_wire_queue) + wire_queue_entries(wire); + buf_norm_wire_queue.clear(); + + // Only after clearing the `buf_norm_wire_queue` are we allowed to call + // enqueue_cell_port, since we're using assertions to check against + // unintended wires being enqueued into `buf_norm_wire_queue` that + // would prevent us from restoring the bufnorm invariants in a single + // pass. + // We process all explicitly enqueued cell ports (clearing the module level queue). for (auto const &[cell, port_name] : buf_norm_cell_port_queue) enqueue_cell_port(cell, port_name); buf_norm_cell_port_queue.clear(); - // And enqueue all wires for `$buf`/`$connect` processing (clearing the module level queue). - for (auto wire : buf_norm_wire_queue) - wire_queue_entries(wire); - buf_norm_wire_queue.clear(); - // We also enqueue all wires that saw newly added module level connections. for (auto &[a, b] : connections_) for (auto &sig : {a, b}) @@ -302,8 +293,11 @@ void RTLIL::Module::bufNormalize() if (chunk.wire) wire_queue_entries(chunk.wire); connect(sig_a, sig_b); + buf_norm_cell_queue.insert(connect_cell); remove(connect_cell); + log_assert(GetSize(buf_norm_wire_queue) <= 2); + buf_norm_wire_queue.clear(); } } } @@ -315,6 +309,9 @@ void RTLIL::Module::bufNormalize() // As a first step for re-normalization we add all require intermediate // wires for cell output and inout ports. for (auto &[cell, port] : pending_ports) { + log_assert(cell->type != ID($input_port)); + log_assert(!cell->type.empty()); + log_assert(!pending_deleted_cells.count(cell)); SigSpec const &sig = cell->getPort(port); Wire *w = addWire(NEW_ID, GetSize(sig)); @@ -323,16 +320,9 @@ void RTLIL::Module::bufNormalize() // correspond to what you would get if the intermediate wires had // been in place from the beginning. connect(sig, w); - auto port_dir = cell->port_dir(port); - if (port_dir == RTLIL::PD_INOUT || port_dir == RTLIL::PD_UNKNOWN) { - direct_driven_wires.emplace(w, {nullptr, {}}); - direct_driven_wires_conflicts[w].emplace(cell, port); - } else { - direct_driven_wires.emplace(w, {cell, port}); - } - - cell->setPort(port, w); - wire_queue_entries(w); + direct_driven_wires.emplace(w, {cell, port}); + cell->setPort(port, w); // Hits the fast path that doesn't enqueue w + wire_queue_entries(w); // Needed so we pick up the sig <-> w connection } // At this point we're done with creating wires and know which ones are @@ -346,7 +336,7 @@ void RTLIL::Module::bufNormalize() wire->driverPort_.clear(); } - // For the unique output cell ports fully connected to a full wire, we + // For the unique driving cell ports fully connected to a full wire, we // can update the bufnorm data right away. For all other wires we will // have to create new `$buf` cells. for (auto const &[wire, cellport] : direct_driven_wires) { @@ -373,54 +363,55 @@ void RTLIL::Module::bufNormalize() SigMap sigmap(this); new_connections({}); - pool conflicted; - pool driven; - - // We iterate over all direct driven wires and try to make that wire's - // sigbits the representative sigbit for the net. We do a second pass - // to detect conflicts to then remove the conflicts from `driven`. - for (bool check : {false, true}) { + // We pick SigMap representatives by prioritizing input ports over + // driven wires over other/unknown wires. + for (bool input_ports : {false, true}) { for (auto const &[wire, cellport] : direct_driven_wires) { - if (cellport.first == nullptr) - continue; - auto const &[cell, port] = cellport; - - SigSpec z_mask; - if (cell->type == ID($buf)) - z_mask = cell->getPort(ID::A); - - for (int i = 0; i != GetSize(wire); ++i) { - SigBit driver = SigBit(wire, i); - if (!z_mask.empty() && z_mask[i] == State::Sz) - continue; - if (check) { - SigBit repr = sigmap(driver); - if (repr != driver) - conflicted.insert(repr); - else - driven.insert(repr); - } else { + if ((wire->port_input && !wire->port_output) == input_ports) { + for (int i = 0; i != GetSize(wire); ++i) { + SigBit driver = SigBit(wire, i); sigmap.database.promote(driver); } } } } - // Ensure that module level inout ports are directly driven or - // connected using `$connect` cells and never `$buf`fered. - for (auto wire : wire_queue_entries) { - if (!wire->port_input || !wire->port_output) - continue; + // All three pool below are in terms of sigmapped bits + // Bits that are known to have a unique driver that is an unconditional driver or one or more inout drivers + pool driven; + // Bits that have multiple unconditional drivers, this forces the use of `$connect` + pool conflicted; + // Bits that are driven by an inout driver + pool weakly_driven; + + for (auto const &[wire, cellport] : direct_driven_wires) { + auto const &[cell, port] = cellport; for (int i = 0; i != GetSize(wire); ++i) { - SigBit driver = SigBit(wire, i); - SigBit repr = sigmap(driver); - if (driver != repr) - driven.erase(repr); + SigBit driver = sigmap(SigBit(wire, i)); + if (cell->type == ID($tribuf) || cell->port_dir(port) == RTLIL::PD_INOUT) { + // We add inout drivers to `driven` in a separate loop below + weakly_driven.insert(driver); + } else { + // We remove driver conflicts from `driven` in a separate loop below + bool inserted = driven.insert(driver).second; + if (!inserted) + conflicted.insert(driver); + } } } - for (auto &bit : conflicted) - driven.erase(bit); + // If a wire has one or more inout drivers and an unconditional driver, that's still a conflict + for (auto driver : weakly_driven) + if (!driven.insert(driver).second) + conflicted.insert(driver); + + // This only leaves the drivers matching `driven`'s definition above + for (auto driver : conflicted) + driven.erase(driver); + + // Having picked representatives and checked whether they are unique + // drivers, we can turn the connecitivty of our sigmap back into $buf + // and $connect cells. // Module level bitwise connections not representable by `$buf` cells pool> undirected_connections; @@ -561,6 +552,8 @@ void RTLIL::Cell::unsetPort(const RTLIL::IdString& portname) w->driverCell_ = nullptr; w->driverPort_ = IdString(); module->buf_norm_wire_queue.insert(w); + } else if (w->driverCell_) { + log_assert(w->driverCell_->getPort(w->driverPort_) == w); } } @@ -630,7 +623,8 @@ void RTLIL::Cell::setPort(const RTLIL::IdString& portname, RTLIL::SigSpec signal // bufNormalize call if ((dir == RTLIL::PD_OUTPUT || dir == RTLIL::PD_INOUT) && signal.is_wire()) { Wire *w = signal.as_wire(); - if (w->driverCell_ == nullptr) { + if (w->driverCell_ == nullptr && ( + (w->port_input && !w->port_output) == (type == ID($input_port)))) { w->driverCell_ = this; w->driverPort_ = portname; diff --git a/passes/cmds/portarcs.cc b/passes/cmds/portarcs.cc index 36870489a..8cc5d1236 100644 --- a/passes/cmds/portarcs.cc +++ b/passes/cmds/portarcs.cc @@ -124,7 +124,8 @@ struct PortarcsPass : Pass { TopoSort sort; for (auto cell : m->cells()) - if (cell->type != ID($buf)) { + // Ignore all bufnorm helper cells + if (!cell->type.in(ID($buf), ID($input_port), ID($connect))) { auto tdata = tinfo.find(cell->type); if (tdata == tinfo.end()) log_cmd_error("Missing timing data for module '%s'.\n", log_id(cell->type)); diff --git a/passes/hierarchy/hierarchy.cc b/passes/hierarchy/hierarchy.cc index 2faeb25d0..6edcf7617 100644 --- a/passes/hierarchy/hierarchy.cc +++ b/passes/hierarchy/hierarchy.cc @@ -1149,6 +1149,25 @@ struct HierarchyPass : public Pass { } } + if (flag_simcheck || flag_smtcheck) { + for (auto mod : design->modules()) { + for (auto cell : mod->cells()) { + if (!cell->type.in(ID($check), ID($assert), ID($assume), ID($live), ID($fair), ID($cover))) + continue; + if (!cell->has_attribute(ID(unsupported_sva))) + continue; + + auto src = cell->get_src_attribute(); + + if (!src.empty()) + src += ": "; + + log_error("%sProperty `%s' in module `%s' uses unsupported SVA constructs. See frontend warnings for details, run `chformal -remove a:unsupported_sva' to ignore.\n", + src, log_id(cell->name), log_id(mod->name)); + } + } + } + if (!keep_positionals) { std::set pos_mods; diff --git a/passes/opt/opt_clean.cc b/passes/opt/opt_clean.cc index f3554e4de..acec20e17 100644 --- a/passes/opt/opt_clean.cc +++ b/passes/opt/opt_clean.cc @@ -635,9 +635,17 @@ void rmunused_module(RTLIL::Module *module, bool purge_mode, bool unusedbitsattr } } for (auto cell : delcells) { - if (verbose) - log_debug(" removing buffer cell `%s': %s = %s\n", cell->name, - log_signal(cell->getPort(ID::Y)), log_signal(cell->getPort(ID::A))); + if (verbose) { + if (cell->type == ID($connect)) + log_debug(" removing connect cell `%s': %s <-> %s\n", cell->name, + log_signal(cell->getPort(ID::A)), log_signal(cell->getPort(ID::B))); + else if (cell->type == ID($input_port)) + log_debug(" removing input port marker cell `%s': %s\n", cell->name, + log_signal(cell->getPort(ID::Y))); + else + log_debug(" removing buffer cell `%s': %s = %s\n", cell->name, + log_signal(cell->getPort(ID::Y)), log_signal(cell->getPort(ID::A))); + } module->remove(cell); } if (!delcells.empty()) diff --git a/passes/opt/opt_hier.cc b/passes/opt/opt_hier.cc index a8df78dc1..5c3b09b31 100644 --- a/passes/opt/opt_hier.cc +++ b/passes/opt/opt_hier.cc @@ -144,12 +144,12 @@ struct ModuleIndex { } if (nunused > 0) { - log("Disconnected %d input bits of instance '%s' of '%s' in '%s'\n", + log("Disconnected %d input bits of instance '%s' (type '%s') in '%s'\n", nunused, log_id(instantiation), log_id(instantiation->type), log_id(parent.module)); changed = true; } if (nconstants > 0) { - log("Substituting constant for %d output bits of instance '%s' of '%s' in '%s'\n", + log("Substituting constant for %d output bits of instance '%s' (type '%s') in '%s'\n", nconstants, log_id(instantiation), log_id(instantiation->type), log_id(parent.module)); changed = true; } @@ -310,7 +310,7 @@ struct UsageData { refine_tie_togethers(inputs); } - bool apply_changes() { + bool apply_changes(ModuleIndex &index) { bool did_something = false; if (module->get_blackbox_attribute()) { @@ -374,8 +374,16 @@ struct UsageData { // Propagate tied-together inputs dict ties; for (auto group : tie_together_inputs) { - for (int i = 1; i < group.size(); i++) - ties[group[i]] = group[0]; + // Only consider used inputs for a tie-together group. + // ModuleIndex::apply_changes might have disconnected + // unused inputs. + SigSpec filtered_group; + for (auto bit : group) { + if (index.used.check(bit)) + filtered_group.append(bit); + } + for (int i = 1; i < filtered_group.size(); i++) + ties[filtered_group[i]] = filtered_group[0]; } SigPool applied_ties; auto ties_rewrite = [&](SigSpec &signal) { @@ -449,12 +457,13 @@ struct OptHierPass : Pass { bool did_something = false; for (auto module : d->selected_modules(RTLIL::SELECT_WHOLE_ONLY, RTLIL::SB_UNBOXED_CMDERR)) { + ModuleIndex &parent_index = indices.at(module->name); + if (usage_datas.count(module->name)) { log_debug("Applying usage data changes to %s\n", log_id(module)); - did_something |= usage_datas.at(module->name).apply_changes(); + did_something |= usage_datas.at(module->name).apply_changes(parent_index); } - ModuleIndex &parent_index = indices.at(module->name); for (auto cell : module->cells()) { if (indices.count(cell->type)) { log_debug("Applying changes to instance %s of %s in %s\n", log_id(cell), log_id(cell->type), log_id(module)); diff --git a/passes/opt/opt_merge.cc b/passes/opt/opt_merge.cc index 13b1cb293..bcde1e173 100644 --- a/passes/opt/opt_merge.cc +++ b/passes/opt/opt_merge.cc @@ -246,10 +246,15 @@ struct OptMergeWorker // mem can have an excessively large parameter holding the init data continue; } + if (cell->type == ID($scopeinfo)) + continue; if (mode_keepdc && has_dont_care_initval(cell)) continue; - if (ct.cell_known(cell->type) || (mode_share_all && cell->known())) - cells.push_back(cell); + if (!cell->known()) + continue; + if (!mode_share_all && !ct.cell_known(cell->type)) + continue; + cells.push_back(cell); } did_something = false; @@ -278,12 +283,6 @@ struct OptMergeWorker for (auto cell : cells) { - if ((!mode_share_all && !ct.cell_known(cell->type)) || !cell->known()) - continue; - - if (cell->type == ID($scopeinfo)) - continue; - auto [cell_in_map, inserted] = known_cells.insert(cell); if (!inserted) { // We've failed to insert since we already have an equivalent cell diff --git a/tests/opt/bug5398.ys b/tests/opt/bug5398.ys new file mode 100644 index 000000000..93c5a2d52 --- /dev/null +++ b/tests/opt/bug5398.ys @@ -0,0 +1,23 @@ +read_verilog < b); + prop_unsupported1: assert property (@(posedge clk) a ##1 b #=# b); + prop_unsupported2: assert property (@(posedge clk) a ##1 @(posedge b) ##1 a); + + sequence local_var_seq; + logic v; + (1, v = a) ##1 b ##1 (v == a); + endsequence + + prop_unsupported3: assert property (@(posedge clk) local_var_seq); + +endmodule +EOF + +logger -expect warning "Mixed clocking is currently not supported" 1 +logger -expect warning "Verific SVA primitive sva_non_overlapped_followed_by .* is currently unsupported in this context" 1 +logger -expect warning "SVA sequences with local variable assignments are currently not supported" 1 +logger -expect warning "Encountered 3 items containing unsupported SVA" 1 +verific -import -sva-continue-on-err top +logger -check-expected + +select -assert-count 4 top/t:$assert +select -assert-count 4 top/a:unsupported_sva top/prop_supported %% top/t:$assert %i + +select -assert-count 3 top/a:unsupported_sva +select -assert-count 3 top/a:unsupported_sva top/prop_unsupported* %i +select -assert-count 1 top/a:unsupported_sva top/prop_unsupported1 %i +select -assert-count 1 top/a:unsupported_sva top/prop_unsupported2 %i +select -assert-count 1 top/a:unsupported_sva top/prop_unsupported3 %i +select -assert-count 0 top/a:unsupported_sva top/prop_supported %i +select -assert-count 1 top/prop_supported + +logger -expect error "uses unsupported SVA constructs." 1 +hierarchy -smtcheck -top top +logger -check-expected diff --git a/tests/verific/sva_continue_on_err_explosion.ys b/tests/verific/sva_continue_on_err_explosion.ys new file mode 100644 index 000000000..c96ad0140 --- /dev/null +++ b/tests/verific/sva_continue_on_err_explosion.ys @@ -0,0 +1,31 @@ +verific -sv < b); + + prop_exploding: assert property (@(posedge clk) + ((a [*7] ##1 b) [*11]) and + ((a [*11] ##1 b) [*7]) and + ((a [*13] ##1 b) [*5]) and + ((a [*5] ##1 b) [*13]) + ); + + prop_supported2: assert property (@(posedge clk) a [*5] ##1 b |=> b); + +endmodule +EOF + +logger -expect warning "Stopping to prevent exponential design size explosion." 1 +verific -import -sva-continue-on-err top +logger -check-expected + +select -assert-count 3 top/t:$assert +select -assert-count 1 top/a:unsupported_sva top/prop_exploding %% top/t:$assert %i + +select -assert-count 0 top/a:unsupported_sva top/prop_supported1 %i +select -assert-count 0 top/a:unsupported_sva top/prop_supported2 %i +select -assert-count 2 top/prop_supported* + +logger -expect error "uses unsupported SVA constructs." 1 +hierarchy -smtcheck -top top +logger -check-expected diff --git a/tests/verific/sva_no_continue_on_err.ys b/tests/verific/sva_no_continue_on_err.ys new file mode 100644 index 000000000..5a0a59a81 --- /dev/null +++ b/tests/verific/sva_no_continue_on_err.ys @@ -0,0 +1,9 @@ + +verific -sv <