mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-10-31 03:32:29 +00:00
Code Activity

Merge pull request #3264 from jix/invalid_ff_dcinit_merge

Browse source 
opt_merge: Add `-keepdc` option required for formal verification
This commit is contained in:
Jannis Harder 2022-04-02 12:41:28 +02:00 • committed by GitHub
commit 8ca9737180
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
3 changed files with 71 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

1
passes/opt/opt.cc
View file

@ -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") {

22
passes/opt/opt_merge.cc
View file

@ -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<std::string> 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;
}

50
tests/opt/opt_merge_init.ys
View file

@ -75,3 +75,53 @@ EOT
opt_merge
select -assert-count 2 t:$dff
design -reset
read_verilog -icells <<EOT
module top(input clk, i, (* init = 1'b0 *) output o, p);
\$dff #(
.CLK_POLARITY(1'h1),
.WIDTH(32'd1)
) ffo (
.CLK(clk),
.D(i),
.Q(o)
);
\$dff #(
.CLK_POLARITY(1'h1),
.WIDTH(32'd1)
) ffp (
.CLK(clk),
.D(i),
.Q(p)
);
endmodule
EOT
opt_merge -keepdc
select -assert-count 1 t:$dff
design -reset
read_verilog -icells <<EOT
module top(input clk, i, output o, p);
\$dff #(
.CLK_POLARITY(1'h1),
.WIDTH(32'd1)
) ffo (
.CLK(clk),
.D(i),
.Q(o)
);
\$dff #(
.CLK_POLARITY(1'h1),
.WIDTH(32'd1)
) ffp (
.CLK(clk),
.D(i),
.Q(p)
);
endmodule
EOT
opt_merge -keepdc
select -assert-count 2 t:$dff