mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2026-07-09 00:40:16 +00:00
Code Activity

Make opt_dff -sat conflict with -keepdc.

Browse source
This commit is contained in:
nella 2026-07-06 13:47:10 +02:00
parent 46cbeab720
commit 0e56ca02ed
2 changed files with 44 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

13
passes/opt/opt_dff.cc
View file

@ -1071,7 +1071,7 @@ struct OptDffWorker
ff_for_cell.emplace(cell, ff);
for (int i = 0; i < ff.width; i++) {
// Skip bits whose reset drives an undefined (x) value
// Skip bits whose reset value is undefined (x)
if (ff.has_srst && !is_def(ff.val_srst[i])) continue;
if (ff.has_arst && !is_def(ff.val_arst[i])) continue;
@ -1424,7 +1424,9 @@ struct OptDffPass : public Pass {
log("\n");
log(" -sat\n");
log(" additionally invoke SAT solver to detect and remove flip-flops (with\n");
log(" non-constant inputs) that can also be replaced with a constant driver\n");
log(" non-constant inputs) that can also be replaced with a constant driver,\n");
log(" or merged with equivalent flip-flops. this reasons in 2-valued logic\n");
log(" and may resolve don't-care bits, so it is incompatible with -keepdc.\n");
log("\n");
log(" -keepdc\n");
log(" some optimizations change the behavior of the circuit with respect to\n");
@ -1456,6 +1458,13 @@ struct OptDffPass : public Pass {
}
extra_args(args, argidx, design);
// The SAT engine reasons in 2-valued logic (a constant x is treated as
// 0), so it can resolve don't-care bits to concrete values -- exactly
// what -keepdc promises not to do. Refuse the combination rather than
// silently ignore -keepdc.
if (opt.sat && opt.keepdc)
log_cmd_error("The -sat and -keepdc options are mutually exclusive.\n");
bool did_something = false;
for (auto mod : design->selected_modules()) {
OptDffWorker worker(opt, mod);

33
tests/opt/opt_dff_eqbits.ys
View file

@ -54,3 +54,36 @@ design -copy-from gate -as gate test_case
equiv_make gold gate equiv
equiv_induct equiv
equiv_status -assert
# verify keepdc exclusivity
design -reset
read_verilog -sv <<EOT
module test_case(input clk, input d, output reg a, output reg b);
initial a = 1'b0;
initial b = 1'b0;
always @(posedge clk) a <= d;
always @(posedge clk) b <= d | 1'bx;
endmodule
EOT
hierarchy -top test_case
proc
techmap
opt_dff -sat
opt_clean -purge
select -assert-count 1 t:$_DFF_P_
design -reset
read_verilog -sv <<EOT
module test_case(input clk, input d, output reg a, output reg b);
initial a = 1'b0;
initial b = 1'b0;
always @(posedge clk) a <= d;
always @(posedge clk) b <= d | 1'bx;
endmodule
EOT
hierarchy -top test_case
proc
techmap
logger -expect error "The -sat and -keepdc options are mutually exclusive." 1
opt_dff -sat -keepdc