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 $<,$^)
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;
pm.run_shiftmul();
pm.run_muldiv();
- pm.run_dffmux();
for (auto w : module->wires()) {
auto it = w->attributes.find(ID::init);
+++ /dev/null
-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
--- /dev/null
+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
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
projects / yosys.git / commitdiff