diff options
author | Jannis Harder <me@jix.one> | 2022-08-16 14:18:35 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2022-08-16 14:18:35 +0200 |
commit | 556d008ed3c2db351e93e0075ccd47bdfb634fd9 (patch) | |
tree | ab23fa7355df8f8ead24839ee7846e68cdbfb935 /passes/cmds | |
parent | c26b2bf543a226e65a3fb07040bb278d668accf2 (diff) | |
parent | f7023d06a2bda56467c8f07cc44d3b92f0eab2ba (diff) | |
download | yosys-556d008ed3c2db351e93e0075ccd47bdfb634fd9.tar.gz yosys-556d008ed3c2db351e93e0075ccd47bdfb634fd9.tar.bz2 yosys-556d008ed3c2db351e93e0075ccd47bdfb634fd9.zip |
Merge pull request #3434 from jix/witness_flow
Updated formal flow with new witness format
Diffstat (limited to 'passes/cmds')
-rw-r--r-- | passes/cmds/rename.cc | 81 | ||||
-rw-r--r-- | passes/cmds/setundef.cc | 24 | ||||
-rw-r--r-- | passes/cmds/show.cc | 1 |
3 files changed, 106 insertions, 0 deletions
diff --git a/passes/cmds/rename.cc b/passes/cmds/rename.cc index b49d5cdc2..45576c91c 100644 --- a/passes/cmds/rename.cc +++ b/passes/cmds/rename.cc @@ -106,6 +106,60 @@ static IdString derive_name_from_cell_output_wire(const RTLIL::Cell *cell, strin return name + suffix; } +static bool rename_witness(RTLIL::Design *design, dict<RTLIL::Module *, int> &cache, RTLIL::Module *module) +{ + auto cached = cache.find(module); + if (cached != cache.end()) { + if (cached->second == -1) + log_error("Cannot rename witness signals in a design containing recursive instantiations.\n"); + return cached->second; + } + cache.emplace(module, -1); + + bool has_witness_signals = false; + for (auto cell : module->cells()) + { + RTLIL::Module *impl = design->module(cell->type); + if (impl != nullptr) { + bool witness_in_cell = rename_witness(design, cache, impl); + has_witness_signals |= witness_in_cell; + if (witness_in_cell && !cell->name.isPublic()) { + std::string name = cell->name.c_str() + 1; + for (auto &c : name) + if ((c < 'a' || c > 'z') && (c < 'A' || c > 'Z') && (c < '0' || c > '9') && c != '_') + c = '_'; + auto new_id = module->uniquify("\\_witness_." + name); + cell->set_hdlname_attribute({ "_witness_", strstr(new_id.c_str(), ".") + 1 }); + module->rename(cell, new_id); + } + } + + if (cell->type.in(ID($anyconst), ID($anyseq), ID($anyinit), ID($allconst), ID($allseq))) { + has_witness_signals = true; + auto QY = cell->type == ID($anyinit) ? ID::Q : ID::Y; + auto sig_out = cell->getPort(QY); + + for (auto chunk : sig_out.chunks()) { + if (chunk.is_wire() && !chunk.wire->name.isPublic()) { + std::string name = stringf("%s_%s", cell->type.c_str() + 1, cell->name.c_str() + 1); + for (auto &c : name) + if ((c < 'a' || c > 'z') && (c < 'A' || c > 'Z') && (c < '0' || c > '9') && c != '_') + c = '_'; + auto new_id = module->uniquify("\\_witness_." + name); + auto new_wire = module->addWire(new_id, GetSize(sig_out)); + new_wire->set_hdlname_attribute({ "_witness_", strstr(new_id.c_str(), ".") + 1 }); + module->connect({sig_out, new_wire}); + cell->setPort(QY, new_wire); + break; + } + } + } + } + + cache[module] = has_witness_signals; + return has_witness_signals; +} + struct RenamePass : public Pass { RenamePass() : Pass("rename", "rename object in the design") { } void help() override @@ -147,6 +201,14 @@ struct RenamePass : public Pass { log("pattern is '_%%_'.\n"); log("\n"); log("\n"); + log(" rename -witness\n"); + log("\n"); + log("Assigns auto-generated names to all $any*/$all* output wires and containing\n"); + log("cells that do not have a public name. This ensures that, during formal\n"); + log("verification, a solver-found trace can be fully specified using a public\n"); + log("hierarchical names.\n"); + log("\n"); + log("\n"); log(" rename -hide [selection]\n"); log("\n"); log("Assign private names (the ones with $-prefix) to all selected wires and cells\n"); @@ -172,6 +234,7 @@ struct RenamePass : public Pass { bool flag_src = false; bool flag_wire = false; bool flag_enumerate = false; + bool flag_witness = false; bool flag_hide = false; bool flag_top = false; bool flag_output = false; @@ -203,6 +266,11 @@ struct RenamePass : public Pass { got_mode = true; continue; } + if (arg == "-witness" && !got_mode) { + flag_witness = true; + got_mode = true; + continue; + } if (arg == "-hide" && !got_mode) { flag_hide = true; got_mode = true; @@ -309,6 +377,19 @@ struct RenamePass : public Pass { } } else + if (flag_witness) + { + extra_args(args, argidx, design, false); + + RTLIL::Module *module = design->top_module(); + + if (module == nullptr) + log_cmd_error("No top module found!\n"); + + dict<RTLIL::Module *, int> cache; + rename_witness(design, cache, module); + } + else if (flag_hide) { extra_args(args, argidx, design); diff --git a/passes/cmds/setundef.cc b/passes/cmds/setundef.cc index a078b0b1c..590a7eb1d 100644 --- a/passes/cmds/setundef.cc +++ b/passes/cmds/setundef.cc @@ -20,6 +20,7 @@ #include "kernel/register.h" #include "kernel/celltypes.h" #include "kernel/sigtools.h" +#include "kernel/mem.h" #include "kernel/rtlil.h" #include "kernel/log.h" @@ -478,6 +479,29 @@ struct SetundefPass : public Pass { log_assert(ffbits.empty()); } + if (worker.next_bit_mode == MODE_ANYSEQ || worker.next_bit_mode == MODE_ANYCONST) + { + // Do not add anyseq / anyconst to unused memory port clocks + std::vector<Mem> memories = Mem::get_selected_memories(module); + for (auto &mem : memories) { + bool changed = false; + for (auto &rd_port : mem.rd_ports) { + if (!rd_port.clk_enable && rd_port.clk.is_fully_undef()) { + changed = true; + rd_port.clk = State::S0; + } + } + for (auto &wr_port : mem.rd_ports) { + if (!wr_port.clk_enable && wr_port.clk.is_fully_undef()) { + changed = true; + wr_port.clk = State::S0; + } + } + if (changed) + mem.emit(); + } + } + module->rewrite_sigspecs(worker); if (worker.next_bit_mode == MODE_ANYSEQ || worker.next_bit_mode == MODE_ANYCONST) diff --git a/passes/cmds/show.cc b/passes/cmds/show.cc index 43deba47b..4d5605932 100644 --- a/passes/cmds/show.cc +++ b/passes/cmds/show.cc @@ -574,6 +574,7 @@ struct ShowWorker { ct.setup_internals(); ct.setup_internals_mem(); + ct.setup_internals_anyinit(); ct.setup_stdcells(); ct.setup_stdcells_mem(); ct.setup_design(design); |