From: Jannis Harder Date: Fri, 1 Apr 2022 19:03:20 +0000 (+0200) Subject: opt_merge: Add `-keepdc` option required for formal verification X-Git-Tag: yosys-0.16~5^2 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ca5b910296c05c95f3bc7f2d1d2b7db19d6328e2;p=yosys.git opt_merge: Add `-keepdc` option required for formal verification The `-keepdc` option prevents merging flipflops with dont-care bits in their initial value, as, in general, this is not a valid transform for formal verification. The keepdc option of `opt` is passed along to `opt_merge` now. --- diff --git a/passes/opt/opt.cc b/passes/opt/opt.cc index c3e418c07..dc88563c2 100644 --- a/passes/opt/opt.cc +++ b/passes/opt/opt.cc @@ -114,6 +114,7 @@ struct OptPass : public Pass { if (args[argidx] == "-keepdc") { opt_expr_args += " -keepdc"; opt_dff_args += " -keepdc"; + opt_merge_args += " -keepdc"; continue; } if (args[argidx] == "-nodffe") { diff --git a/passes/opt/opt_merge.cc b/passes/opt/opt_merge.cc index 115eb97a9..e9d98cd43 100644 --- a/passes/opt/opt_merge.cc +++ b/passes/opt/opt_merge.cc @@ -219,7 +219,15 @@ struct OptMergeWorker return conn1 == conn2; } - OptMergeWorker(RTLIL::Design *design, RTLIL::Module *module, bool mode_nomux, bool mode_share_all) : + bool has_dont_care_initval(const RTLIL::Cell *cell) + { + if (!RTLIL::builtin_ff_cell_types().count(cell->type)) + return false; + + return !initvals(cell->getPort(ID::Q)).is_fully_def(); + } + + OptMergeWorker(RTLIL::Design *design, RTLIL::Module *module, bool mode_nomux, bool mode_share_all, bool mode_keepdc) : design(design), module(module), assign_map(module), mode_share_all(mode_share_all) { total_count = 0; @@ -253,6 +261,8 @@ struct OptMergeWorker for (auto &it : module->cells_) { if (!design->selected(module, it.second)) continue; + if (mode_keepdc && has_dont_care_initval(it.second)) + continue; if (ct.cell_known(it.second->type) || (mode_share_all && it.second->known())) cells.push_back(it.second); } @@ -319,6 +329,9 @@ struct OptMergePass : public Pass { log(" -share_all\n"); log(" Operate on all cell types, not just built-in types.\n"); log("\n"); + log(" -keepdc\n"); + log(" Do not merge flipflops with don't-care bits in their initial value.\n"); + log("\n"); } void execute(std::vector args, RTLIL::Design *design) override { @@ -326,6 +339,7 @@ struct OptMergePass : public Pass { bool mode_nomux = false; bool mode_share_all = false; + bool mode_keepdc = false; size_t argidx; for (argidx = 1; argidx < args.size(); argidx++) { @@ -338,13 +352,17 @@ struct OptMergePass : public Pass { mode_share_all = true; continue; } + if (arg == "-keepdc") { + mode_keepdc = true; + continue; + } break; } extra_args(args, argidx, design); int total_count = 0; for (auto module : design->selected_modules()) { - OptMergeWorker worker(design, module, mode_nomux, mode_share_all); + OptMergeWorker worker(design, module, mode_nomux, mode_share_all, mode_keepdc); total_count += worker.total_count; } diff --git a/tests/opt/opt_merge_init.ys b/tests/opt/opt_merge_init.ys index 20b6cabee..7ee7d3dd7 100644 --- a/tests/opt/opt_merge_init.ys +++ b/tests/opt/opt_merge_init.ys @@ -75,3 +75,53 @@ EOT opt_merge select -assert-count 2 t:$dff + +design -reset +read_verilog -icells <