diff options
author | Marcelina KoĆcielnicka <mwk@0x04.net> | 2020-07-15 02:37:43 +0200 |
---|---|---|
committer | Marcelina KoĆcielnicka <mwk@0x04.net> | 2020-08-07 13:21:34 +0200 |
commit | a0e99a9f3f0a52e3a6f2000791d93b54ce116928 (patch) | |
tree | 0c53f762f27d9dc23e3085923ab8798ad02a356e | |
parent | acd8c5c205ca9292ff5e7546cf748cb1715f1ec0 (diff) | |
download | yosys-a0e99a9f3f0a52e3a6f2000791d93b54ce116928.tar.gz yosys-a0e99a9f3f0a52e3a6f2000791d93b54ce116928.tar.bz2 yosys-a0e99a9f3f0a52e3a6f2000791d93b54ce116928.zip |
peepopt: Remove now-redundant dffmux pattern.
-rw-r--r-- | passes/pmgen/Makefile.inc | 1 | ||||
-rw-r--r-- | passes/pmgen/peepopt.cc | 3 | ||||
-rw-r--r-- | passes/pmgen/peepopt_dffmux.pmg | 171 | ||||
-rw-r--r-- | tests/opt/opt_dff_dffmux.ys | 129 | ||||
-rw-r--r-- | tests/various/peepopt.ys | 143 |
5 files changed, 129 insertions, 318 deletions
diff --git a/passes/pmgen/Makefile.inc b/passes/pmgen/Makefile.inc index 1a57bef7d..c6bbc386a 100644 --- a/passes/pmgen/Makefile.inc +++ b/passes/pmgen/Makefile.inc @@ -36,7 +36,6 @@ $(eval $(call add_extra_objs,passes/pmgen/peepopt_pm.h)) PEEPOPT_PATTERN = passes/pmgen/peepopt_shiftmul.pmg PEEPOPT_PATTERN += passes/pmgen/peepopt_muldiv.pmg -PEEPOPT_PATTERN += passes/pmgen/peepopt_dffmux.pmg passes/pmgen/peepopt_pm.h: passes/pmgen/pmgen.py $(PEEPOPT_PATTERN) $(P) mkdir -p passes/pmgen && $(PYTHON_EXECUTABLE) $< -o $@ -p peepopt $(filter-out $<,$^) diff --git a/passes/pmgen/peepopt.cc b/passes/pmgen/peepopt.cc index c16b4486d..a9c62fcf6 100644 --- a/passes/pmgen/peepopt.cc +++ b/passes/pmgen/peepopt.cc @@ -67,8 +67,6 @@ struct PeepoptPass : public Pass { GENERATE_PATTERN(peepopt_pm, shiftmul); else if (genmode == "muldiv") GENERATE_PATTERN(peepopt_pm, muldiv); - else if (genmode == "dffmux") - GENERATE_PATTERN(peepopt_pm, dffmux); else log_abort(); return; @@ -106,7 +104,6 @@ struct PeepoptPass : public Pass { pm.run_shiftmul(); pm.run_muldiv(); - pm.run_dffmux(); for (auto w : module->wires()) { auto it = w->attributes.find(ID::init); diff --git a/passes/pmgen/peepopt_dffmux.pmg b/passes/pmgen/peepopt_dffmux.pmg deleted file mode 100644 index 0069b0570..000000000 --- a/passes/pmgen/peepopt_dffmux.pmg +++ /dev/null @@ -1,171 +0,0 @@ -pattern dffmux - -state <IdString> cemuxAB rstmuxBA -state <SigSpec> sigD - -match dff - select dff->type == $dff - select GetSize(port(dff, \D)) > 1 -endmatch - -code sigD - sigD = port(dff, \D); -endcode - -match rstmux - select rstmux->type == $mux - select GetSize(port(rstmux, \Y)) > 1 - index <SigSpec> port(rstmux, \Y) === sigD - choice <IdString> BA {\B, \A} - select port(rstmux, BA).is_fully_const() - set rstmuxBA BA - semioptional -endmatch - -code sigD - if (rstmux) - sigD = port(rstmux, rstmuxBA == \B ? \A : \B); -endcode - -match cemux - select cemux->type == $mux - select GetSize(port(cemux, \Y)) > 1 - index <SigSpec> port(cemux, \Y) === sigD - choice <IdString> AB {\A, \B} - index <SigSpec> port(cemux, AB) === port(dff, \Q) - set cemuxAB AB - semioptional -endmatch - -code - if (!cemux && !rstmux) - reject; -endcode - -code - Const rst; - SigSpec D; - if (cemux) { - D = port(cemux, cemuxAB == \A ? \B : \A); - if (rstmux) - rst = port(rstmux, rstmuxBA).as_const(); - else - rst = Const(State::Sx, GetSize(D)); - } - else { - log_assert(rstmux); - D = port(rstmux, rstmuxBA == \B ? \A : \B); - rst = port(rstmux, rstmuxBA).as_const(); - } - SigSpec Q = port(dff, \Q); - int width = GetSize(D); - - SigSpec dffD = dff->getPort(\D); - SigSpec dffQ = dff->getPort(\Q); - - Const initval; - for (auto b : Q) { - auto it = initbits.find(b); - initval.bits.push_back(it == initbits.end() ? State::Sx : it->second); - } - - auto cmpx = [=](State lhs, State rhs) { - if (lhs == State::Sx || rhs == State::Sx) - return true; - return lhs == rhs; - }; - - int i = width-1; - while (i > 1) { - if (D[i] != D[i-1]) - break; - if (!cmpx(rst[i], rst[i-1])) - break; - if (!cmpx(initval[i], initval[i-1])) - break; - if (!cmpx(rst[i], initval[i])) - break; - rminitbits.insert(Q[i]); - module->connect(Q[i], Q[i-1]); - i--; - } - if (i < width-1) { - did_something = true; - if (cemux) { - SigSpec ceA = cemux->getPort(\A); - SigSpec ceB = cemux->getPort(\B); - SigSpec ceY = cemux->getPort(\Y); - ceA.remove(i, width-1-i); - ceB.remove(i, width-1-i); - ceY.remove(i, width-1-i); - cemux->setPort(\A, ceA); - cemux->setPort(\B, ceB); - cemux->setPort(\Y, ceY); - cemux->fixup_parameters(); - blacklist(cemux); - } - if (rstmux) { - SigSpec rstA = rstmux->getPort(\A); - SigSpec rstB = rstmux->getPort(\B); - SigSpec rstY = rstmux->getPort(\Y); - rstA.remove(i, width-1-i); - rstB.remove(i, width-1-i); - rstY.remove(i, width-1-i); - rstmux->setPort(\A, rstA); - rstmux->setPort(\B, rstB); - rstmux->setPort(\Y, rstY); - rstmux->fixup_parameters(); - blacklist(rstmux); - } - dffD.remove(i, width-1-i); - dffQ.remove(i, width-1-i); - dff->setPort(\D, dffD); - dff->setPort(\Q, dffQ); - dff->fixup_parameters(); - blacklist(dff); - - log("dffcemux pattern in %s: dff=%s, cemux=%s, rstmux=%s; removed top %d bits.\n", log_id(module), log_id(dff), log_id(cemux, "n/a"), log_id(rstmux, "n/a"), width-1-i); - width = i+1; - } - if (cemux) { - SigSpec ceA = cemux->getPort(\A); - SigSpec ceB = cemux->getPort(\B); - SigSpec ceY = cemux->getPort(\Y); - - int count = 0; - for (int i = width-1; i >= 0; i--) { - if (D[i].wire) - continue; - if (cmpx(rst[i], D[i].data) && cmpx(initval[i], D[i].data)) { - count++; - rminitbits.insert(Q[i]); - module->connect(Q[i], D[i]); - ceA.remove(i); - ceB.remove(i); - ceY.remove(i); - dffD.remove(i); - dffQ.remove(i); - } - } - if (count > 0) - { - did_something = true; - - cemux->setPort(\A, ceA); - cemux->setPort(\B, ceB); - cemux->setPort(\Y, ceY); - cemux->fixup_parameters(); - blacklist(cemux); - - dff->setPort(\D, dffD); - dff->setPort(\Q, dffQ); - dff->fixup_parameters(); - blacklist(dff); - - log("dffcemux pattern in %s: dff=%s, cemux=%s, rstmux=%s; removed %d constant bits.\n", log_id(module), log_id(dff), log_id(cemux), log_id(rstmux, "n/a"), count); - } - } - - if (did_something) - accept; -endcode diff --git a/tests/opt/opt_dff_dffmux.ys b/tests/opt/opt_dff_dffmux.ys new file mode 100644 index 000000000..43190cc31 --- /dev/null +++ b/tests/opt/opt_dff_dffmux.ys @@ -0,0 +1,129 @@ +design -reset +read_verilog <<EOT +module opt_dffmuxext_unsigned(input clk, ce, input [1:0] i, output reg [3:0] o); + always @(posedge clk) if (ce) o <= i; +endmodule +EOT + +proc +equiv_opt -assert opt +design -load postopt +select -assert-count 1 t:$dffe r:WIDTH=2 %i +select -assert-count 0 t:$dffe %% t:* %D + +#################### + +design -reset +read_verilog <<EOT +module opt_dffmuxext_signed(input clk, ce, input signed [1:0] i, output reg signed [3:0] o); + always @(posedge clk) if (ce) o <= i; +endmodule +EOT + +proc +equiv_opt -assert opt +design -load postopt +wreduce +select -assert-count 1 t:$dffe r:WIDTH=2 %i +select -assert-count 0 t:$dffe %% t:* %D + +################### + +design -reset +read_verilog <<EOT +module opt_dffmuxext_const(input clk, ce, input [1:0] i, output reg [5:0] o); + always @(posedge clk) if (ce) o <= {1'b0, i[1], 2'b1x, i[0], 1'bz}; +endmodule +EOT + +proc +equiv_opt -assert opt +design -load postopt +select -assert-count 1 t:$dffe r:WIDTH=2 %i +select -assert-count 0 t:$dffe %% t:* %D + +################### + +design -reset +read_verilog <<EOT +module opt_dffmuxext_const_init(input clk, ce, input [1:0] i, (* init=6'b0x00x1 *) output reg [5:0] o); + always @(posedge clk) if (ce) o <= {1'b0, i[1], 2'b1x, i[0], 1'bz}; +endmodule +EOT + +proc +equiv_opt -assert opt +design -load postopt +select -assert-count 1 t:$dffe r:WIDTH=4 %i +select -assert-count 0 t:$dffe %% t:* %D + +#################### + +design -reset +read_verilog <<EOT +module opt_dffmuxext_unsigned_rst(input clk, ce, rst, input [1:0] i, output reg [3:0] o); + always @(posedge clk) if (rst) o <= 0; else if (ce) o <= i; +endmodule +EOT + +proc +equiv_opt -assert opt +design -load postopt +wreduce +select -assert-count 1 t:$sdffe r:WIDTH=2 %i +select -assert-count 0 t:$sdffe %% t:* %D + +#################### + +design -reset +read_verilog <<EOT +module opt_dffmuxext_signed_rst(input clk, ce, rstn, input signed [1:0] i, output reg signed [3:0] o); + always @(posedge clk) begin + if (ce) o <= i; + if (!rstn) o <= 4'b1111; + end +endmodule +EOT + +proc +equiv_opt -assert opt +design -load postopt +wreduce +select -assert-count 1 t:$sdffe r:WIDTH=2 %i +select -assert-count 0 t:$sdffe %% t:* %D + +#################### + +design -reset +read_verilog <<EOT +module opt_dffmuxext_signed_rst_init(input clk, ce, rstn, input signed [1:0] i, output reg signed [3:0] o); + initial o <= 4'b0010; + always @(posedge clk) begin + if (ce) o <= i; + if (!rstn) o <= 4'b1111; + end +endmodule +EOT + +proc +# NB: equiv_opt uses equiv_induct which covers +# only the induction half of temporal induction +# --- missing the base-case half +# This makes it akin to `sat -tempinduct-inductonly` +# instead of `sat -tempinduct-baseonly` or +# `sat -tempinduct` which is necessary for this +# testcase +#equiv_opt -assert opt + +design -save gold +opt +wreduce +design -stash gate +design -import gold -as gold +design -import gate -as gate +miter -equiv -flatten -make_assert -make_outputs gold gate miter +sat -tempinduct -verify -prove-asserts -show-ports miter + +design -load gate +select -assert-count 1 t:$sdffe r:WIDTH=3 %i +select -assert-count 0 t:$sdffe %% t:* %D diff --git a/tests/various/peepopt.ys b/tests/various/peepopt.ys index ee5ad8a1a..45e936a21 100644 --- a/tests/various/peepopt.ys +++ b/tests/various/peepopt.ys @@ -68,146 +68,3 @@ equiv_opt -assert peepopt design -load postopt clean select -assert-count 0 t:* - -#################### - -design -reset -read_verilog <<EOT -module peepopt_dffmuxext_unsigned(input clk, ce, input [1:0] i, output reg [3:0] o); - always @(posedge clk) if (ce) o <= i; -endmodule -EOT - -proc -equiv_opt -assert peepopt -design -load postopt -clean -select -assert-count 1 t:$dff r:WIDTH=2 %i -select -assert-count 1 t:$mux r:WIDTH=2 %i -select -assert-count 0 t:$dff t:$mux %% t:* %D - -#################### - -design -reset -read_verilog <<EOT -module peepopt_dffmuxext_signed(input clk, ce, input signed [1:0] i, output reg signed [3:0] o); - always @(posedge clk) if (ce) o <= i; -endmodule -EOT - -proc -equiv_opt -assert peepopt -design -load postopt -clean -select -assert-count 1 t:$dff r:WIDTH=2 %i -select -assert-count 1 t:$mux r:WIDTH=2 %i -select -assert-count 0 t:$dff t:$mux %% t:* %D - -################### - -design -reset -read_verilog <<EOT -module peepopt_dffmuxext_const(input clk, ce, input [1:0] i, output reg [5:0] o); - always @(posedge clk) if (ce) o <= {1'b0, i[1], 2'b1x, i[0], 1'bz}; -endmodule -EOT - -proc -equiv_opt -assert peepopt -design -load postopt -select -assert-count 1 t:$dff r:WIDTH=2 %i -select -assert-count 1 t:$mux r:WIDTH=2 %i -select -assert-count 0 t:$dff t:$mux %% t:* %D - -################### - -design -reset -read_verilog <<EOT -module peepopt_dffmuxext_const_init(input clk, ce, input [1:0] i, (* init=6'b0x00x1 *) output reg [5:0] o); - always @(posedge clk) if (ce) o <= {1'b0, i[1], 2'b1x, i[0], 1'bz}; -endmodule -EOT - -proc -equiv_opt -assert peepopt -design -load postopt -select -assert-count 1 t:$dff r:WIDTH=4 %i -select -assert-count 1 t:$mux r:WIDTH=4 %i -select -assert-count 0 t:$dff t:$mux %% t:* %D - -#################### - -design -reset -read_verilog <<EOT -module peepopt_dffmuxext_unsigned_rst(input clk, ce, rst, input [1:0] i, output reg [3:0] o); - always @(posedge clk) if (rst) o <= 0; else if (ce) o <= i; -endmodule -EOT - -proc -equiv_opt -assert peepopt -design -load postopt -wreduce -select -assert-count 1 t:$dff r:WIDTH=2 %i -select -assert-count 2 t:$mux -select -assert-count 2 t:$mux r:WIDTH=2 %i -select -assert-count 0 t:$dff t:$mux %% t:* %D - -#################### - -design -reset -read_verilog <<EOT -module peepopt_dffmuxext_signed_rst(input clk, ce, rstn, input signed [1:0] i, output reg signed [3:0] o); - always @(posedge clk) begin - if (ce) o <= i; - if (!rstn) o <= 4'b1111; - end -endmodule -EOT - -proc -equiv_opt -assert peepopt -design -load postopt -wreduce -select -assert-count 1 t:$dff r:WIDTH=2 %i -select -assert-count 2 t:$mux -select -assert-count 2 t:$mux r:WIDTH=2 %i -select -assert-count 0 t:$logic_not t:$dff t:$mux %% t:* %D - -#################### - -design -reset -read_verilog <<EOT -module peepopt_dffmuxext_signed_rst_init(input clk, ce, rstn, input signed [1:0] i, output reg signed [3:0] o); - initial o <= 4'b0010; - always @(posedge clk) begin - if (ce) o <= i; - if (!rstn) o <= 4'b1111; - end -endmodule -EOT - -proc -# NB: equiv_opt uses equiv_induct which covers -# only the induction half of temporal induction -# --- missing the base-case half -# This makes it akin to `sat -tempinduct-inductonly` -# instead of `sat -tempinduct-baseonly` or -# `sat -tempinduct` which is necessary for this -# testcase -#equiv_opt -assert peepopt - -design -save gold -peepopt -wreduce -design -stash gate -design -import gold -as gold -design -import gate -as gate -miter -equiv -flatten -make_assert -make_outputs gold gate miter -sat -tempinduct -verify -prove-asserts -show-ports miter - -design -load gate -select -assert-count 1 t:$dff r:WIDTH=4 %i -select -assert-count 2 t:$mux -select -assert-count 2 t:$mux r:WIDTH=4 %i -select -assert-count 0 t:$logic_not t:$dff t:$mux %% t:* %D |