aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorEddie Hung <eddie@fpgeh.com>2019-08-08 07:58:11 -0700
committerGitHub <noreply@github.com>2019-08-08 07:58:11 -0700
commit61d7f1997ba7e3098acc25694accdd0ff25b8ab1 (patch)
tree9f61784ace2ff54c0f6cd3705804f13af41f964c
parent3414ee1e3fe37d4bf383621542828d4fc8fc987f (diff)
parent8bf45f34c4d7143c58acde2544603cde443ad142 (diff)
downloadyosys-61d7f1997ba7e3098acc25694accdd0ff25b8ab1.tar.gz
yosys-61d7f1997ba7e3098acc25694accdd0ff25b8ab1.tar.bz2
yosys-61d7f1997ba7e3098acc25694accdd0ff25b8ab1.zip
Merge pull request #1266 from YosysHQ/eddie/ice40_full_adder
Wrap SB_LUT+SB_CARRY into $__ICE40_CARRY_WRAPPER
-rw-r--r--CHANGELOG2
-rw-r--r--frontends/ast/ast.cc2
-rw-r--r--passes/pmgen/Makefile.inc10
-rw-r--r--passes/pmgen/ice40_wrapcarry.cc90
-rw-r--r--passes/pmgen/ice40_wrapcarry.pmg11
-rw-r--r--techlibs/ice40/Makefile.inc1
-rw-r--r--techlibs/ice40/arith_map.v30
-rw-r--r--techlibs/ice40/cells_map.v23
-rw-r--r--techlibs/ice40/ice40_unlut.cc106
-rw-r--r--techlibs/ice40/synth_ice40.cc13
-rw-r--r--techlibs/ice40/tests/test_arith.ys9
-rw-r--r--tests/opt/opt_expr.ys (renamed from tests/various/opt_expr.ys)0
-rw-r--r--tests/opt/opt_ff.v21
-rw-r--r--tests/opt/opt_ff.ys3
-rw-r--r--tests/opt/opt_lut.ys4
-rw-r--r--tests/opt/opt_rmdff.v (renamed from tests/various/opt_rmdff.v)0
-rw-r--r--tests/opt/opt_rmdff.ys (renamed from tests/various/opt_rmdff.ys)0
-rw-r--r--tests/opt/opt_rmdff_sat.v (renamed from tests/opt/opt_ff_sat.v)0
-rw-r--r--tests/opt/opt_rmdff_sat.ys (renamed from tests/opt/opt_ff_sat.ys)2
-rw-r--r--tests/various/wreduce.ys33
20 files changed, 180 insertions, 180 deletions
diff --git a/CHANGELOG b/CHANGELOG
index 638c36121..21fb8a3f5 100644
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -19,6 +19,8 @@ Yosys 0.9 .. Yosys 0.9-dev
- Added automatic gzip compression (based on filename extension) for backends
- Improve attribute and parameter encoding in JSON to avoid ambiguities between
bit vectors and strings containing [01xz]*
+ - Added "ice40_wrapcarry" to encapsulate SB_LUT+SB_CARRY pairs for techmapping
+ - Removed "ice40_unlut"
Yosys 0.8 .. Yosys 0.8-dev
--------------------------
diff --git a/frontends/ast/ast.cc b/frontends/ast/ast.cc
index 943466ee3..c8ca6d164 100644
--- a/frontends/ast/ast.cc
+++ b/frontends/ast/ast.cc
@@ -1172,7 +1172,7 @@ void AST::process(RTLIL::Design *design, AstNode *ast, bool dump_ast1, bool dump
if (design->has((*it)->str)) {
RTLIL::Module *existing_mod = design->module((*it)->str);
- if (!nooverwrite && !overwrite && !existing_mod->get_bool_attribute("\\blackbox")) {
+ if (!nooverwrite && !overwrite && !existing_mod->get_blackbox_attribute()) {
log_file_error((*it)->filename, (*it)->linenum, "Re-definition of module `%s'!\n", (*it)->str.c_str());
} else if (nooverwrite) {
log("Ignoring re-definition of module `%s' at %s:%d.\n",
diff --git a/passes/pmgen/Makefile.inc b/passes/pmgen/Makefile.inc
index 7911132db..c03606152 100644
--- a/passes/pmgen/Makefile.inc
+++ b/passes/pmgen/Makefile.inc
@@ -1,4 +1,5 @@
OBJS += passes/pmgen/ice40_dsp.o
+OBJS += passes/pmgen/ice40_wrapcarry.o
OBJS += passes/pmgen/peepopt.o
# --------------------------------------
@@ -12,6 +13,15 @@ passes/pmgen/ice40_dsp_pm.h: passes/pmgen/pmgen.py passes/pmgen/ice40_dsp.pmg
# --------------------------------------
+passes/pmgen/ice40_wrapcarry.o: passes/pmgen/ice40_wrapcarry_pm.h
+EXTRA_OBJS += passes/pmgen/ice40_wrapcarry_pm.h
+.SECONDARY: passes/pmgen/ice40_wrapcarry_pm.h
+
+passes/pmgen/ice40_wrapcarry_pm.h: passes/pmgen/pmgen.py passes/pmgen/ice40_wrapcarry.pmg
+ $(P) mkdir -p passes/pmgen && python3 $< -o $@ -p ice40_wrapcarry $(filter-out $<,$^)
+
+# --------------------------------------
+
passes/pmgen/peepopt.o: passes/pmgen/peepopt_pm.h
EXTRA_OBJS += passes/pmgen/peepopt_pm.h
.SECONDARY: passes/pmgen/peepopt_pm.h
diff --git a/passes/pmgen/ice40_wrapcarry.cc b/passes/pmgen/ice40_wrapcarry.cc
new file mode 100644
index 000000000..69ef3cd82
--- /dev/null
+++ b/passes/pmgen/ice40_wrapcarry.cc
@@ -0,0 +1,90 @@
+/*
+ * yosys -- Yosys Open SYnthesis Suite
+ *
+ * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
+ *
+ * Permission to use, copy, modify, and/or distribute this software for any
+ * purpose with or without fee is hereby granted, provided that the above
+ * copyright notice and this permission notice appear in all copies.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+ * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+ * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
+ * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+ * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+ * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
+ * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
+ *
+ */
+
+#include "kernel/yosys.h"
+#include "kernel/sigtools.h"
+
+USING_YOSYS_NAMESPACE
+PRIVATE_NAMESPACE_BEGIN
+
+#include "passes/pmgen/ice40_wrapcarry_pm.h"
+
+void create_ice40_wrapcarry(ice40_wrapcarry_pm &pm)
+{
+ auto &st = pm.st_ice40_wrapcarry;
+
+#if 0
+ log("\n");
+ log("carry: %s\n", log_id(st.carry, "--"));
+ log("lut: %s\n", log_id(st.lut, "--"));
+#endif
+
+ log(" replacing SB_LUT + SB_CARRY with $__ICE40_CARRY_WRAPPER cell.\n");
+
+ Cell *cell = pm.module->addCell(NEW_ID, "$__ICE40_CARRY_WRAPPER");
+ pm.module->swap_names(cell, st.carry);
+
+ cell->setPort("\\A", st.carry->getPort("\\I0"));
+ cell->setPort("\\B", st.carry->getPort("\\I1"));
+ cell->setPort("\\CI", st.carry->getPort("\\CI"));
+ cell->setPort("\\CO", st.carry->getPort("\\CO"));
+
+ cell->setPort("\\I0", st.lut->getPort("\\I0"));
+ cell->setPort("\\I3", st.lut->getPort("\\I3"));
+ cell->setPort("\\O", st.lut->getPort("\\O"));
+ cell->setParam("\\LUT", st.lut->getParam("\\LUT_INIT"));
+
+ pm.autoremove(st.carry);
+ pm.autoremove(st.lut);
+}
+
+struct Ice40WrapCarryPass : public Pass {
+ Ice40WrapCarryPass() : Pass("ice40_wrapcarry", "iCE40: wrap carries") { }
+ void help() YS_OVERRIDE
+ {
+ // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+ log("\n");
+ log(" ice40_wrapcarry [selection]\n");
+ log("\n");
+ log("Wrap manually instantiated SB_CARRY cells, along with their associated SB_LUTs,\n");
+ log("into an internal $__ICE40_CARRY_WRAPPER cell for preservation across technology\n");
+ log("mapping.");
+ log("\n");
+ }
+ void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
+ {
+ log_header(design, "Executing ICE40_WRAPCARRY pass (wrap carries).\n");
+
+ size_t argidx;
+ for (argidx = 1; argidx < args.size(); argidx++)
+ {
+ // if (args[argidx] == "-singleton") {
+ // singleton_mode = true;
+ // continue;
+ // }
+ break;
+ }
+ extra_args(args, argidx, design);
+
+ for (auto module : design->selected_modules())
+ ice40_wrapcarry_pm(module, module->selected_cells()).run_ice40_wrapcarry(create_ice40_wrapcarry);
+ }
+} Ice40WrapCarryPass;
+
+PRIVATE_NAMESPACE_END
diff --git a/passes/pmgen/ice40_wrapcarry.pmg b/passes/pmgen/ice40_wrapcarry.pmg
new file mode 100644
index 000000000..9e64c7467
--- /dev/null
+++ b/passes/pmgen/ice40_wrapcarry.pmg
@@ -0,0 +1,11 @@
+pattern ice40_wrapcarry
+
+match carry
+ select carry->type.in(\SB_CARRY)
+endmatch
+
+match lut
+ select lut->type.in(\SB_LUT4)
+ index <SigSpec> port(lut, \I1) === port(carry, \I0)
+ index <SigSpec> port(lut, \I2) === port(carry, \I1)
+endmatch
diff --git a/techlibs/ice40/Makefile.inc b/techlibs/ice40/Makefile.inc
index d258d5a5d..76a89b107 100644
--- a/techlibs/ice40/Makefile.inc
+++ b/techlibs/ice40/Makefile.inc
@@ -4,7 +4,6 @@ OBJS += techlibs/ice40/ice40_braminit.o
OBJS += techlibs/ice40/ice40_ffssr.o
OBJS += techlibs/ice40/ice40_ffinit.o
OBJS += techlibs/ice40/ice40_opt.o
-OBJS += techlibs/ice40/ice40_unlut.o
GENFILES += techlibs/ice40/brams_init1.vh
GENFILES += techlibs/ice40/brams_init2.vh
diff --git a/techlibs/ice40/arith_map.v b/techlibs/ice40/arith_map.v
index fe83a8e38..26b24db9e 100644
--- a/techlibs/ice40/arith_map.v
+++ b/techlibs/ice40/arith_map.v
@@ -44,35 +44,21 @@ module _80_ice40_alu (A, B, CI, BI, X, Y, CO);
genvar i;
generate for (i = 0; i < Y_WIDTH; i = i + 1) begin:slice
-`ifdef _ABC
- \$__ICE40_FULL_ADDER carry (
+ \$__ICE40_CARRY_WRAPPER #(
+ // A[0]: 1010 1010 1010 1010
+ // A[1]: 1100 1100 1100 1100
+ // A[2]: 1111 0000 1111 0000
+ // A[3]: 1111 1111 0000 0000
+ .LUT(16'b 0110_1001_1001_0110)
+ ) fadd (
.A(AA[i]),
.B(BB[i]),
.CI(C[i]),
- .CO(CO[i]),
- .O(Y[i])
- );
-`else
- SB_CARRY carry (
- .I0(AA[i]),
- .I1(BB[i]),
- .CI(C[i]),
- .CO(CO[i])
- );
- SB_LUT4 #(
- // I0: 1010 1010 1010 1010
- // I1: 1100 1100 1100 1100
- // I2: 1111 0000 1111 0000
- // I3: 1111 1111 0000 0000
- .LUT_INIT(16'b 0110_1001_1001_0110)
- ) adder (
.I0(1'b0),
- .I1(AA[i]),
- .I2(BB[i]),
.I3(C[i]),
+ .CO(CO[i]),
.O(Y[i])
);
-`endif
end endgenerate
assign X = AA ^ BB;
diff --git a/techlibs/ice40/cells_map.v b/techlibs/ice40/cells_map.v
index b4b831165..0c10c9ac4 100644
--- a/techlibs/ice40/cells_map.v
+++ b/techlibs/ice40/cells_map.v
@@ -62,26 +62,21 @@ module \$lut (A, Y);
endmodule
`endif
-`ifdef _ABC
-module \$__ICE40_FULL_ADDER (output CO, O, input A, B, CI);
+`ifndef NO_ADDER
+module \$__ICE40_CARRY_WRAPPER (output CO, O, input A, B, CI, I0, I3);
+ parameter LUT = 0;
SB_CARRY carry (
.I0(A),
.I1(B),
.CI(CI),
.CO(CO)
);
- SB_LUT4 #(
- // I0: 1010 1010 1010 1010
- // I1: 1100 1100 1100 1100
- // I2: 1111 0000 1111 0000
- // I3: 1111 1111 0000 0000
- .LUT_INIT(16'b 0110_1001_1001_0110)
- ) adder (
- .I0(1'b0),
- .I1(A),
- .I2(B),
- .I3(CI),
- .O(O)
+ \$lut #(
+ .WIDTH(4),
+ .LUT(LUT)
+ ) lut (
+ .A({I3,B,A,I0}),
+ .Y(O)
);
endmodule
`endif
diff --git a/techlibs/ice40/ice40_unlut.cc b/techlibs/ice40/ice40_unlut.cc
deleted file mode 100644
index f3f70ac1f..000000000
--- a/techlibs/ice40/ice40_unlut.cc
+++ /dev/null
@@ -1,106 +0,0 @@
-/*
- * yosys -- Yosys Open SYnthesis Suite
- *
- * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
- *
- * Permission to use, copy, modify, and/or distribute this software for any
- * purpose with or without fee is hereby granted, provided that the above
- * copyright notice and this permission notice appear in all copies.
- *
- * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
- * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
- * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
- * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
- * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
- * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
- * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
- *
- */
-
-#include "kernel/yosys.h"
-#include "kernel/sigtools.h"
-#include <stdlib.h>
-#include <stdio.h>
-
-USING_YOSYS_NAMESPACE
-PRIVATE_NAMESPACE_BEGIN
-
-static SigBit get_bit_or_zero(const SigSpec &sig)
-{
- if (GetSize(sig) == 0)
- return State::S0;
- return sig[0];
-}
-
-static void run_ice40_unlut(Module *module)
-{
- SigMap sigmap(module);
-
- for (auto cell : module->selected_cells())
- {
- if (cell->type == "\\SB_LUT4")
- {
- SigSpec inbits;
-
- inbits.append(get_bit_or_zero(cell->getPort("\\I0")));
- inbits.append(get_bit_or_zero(cell->getPort("\\I1")));
- inbits.append(get_bit_or_zero(cell->getPort("\\I2")));
- inbits.append(get_bit_or_zero(cell->getPort("\\I3")));
- sigmap.apply(inbits);
-
- log("Mapping SB_LUT4 cell %s.%s to $lut.\n", log_id(module), log_id(cell));
-
- cell->type ="$lut";
- cell->setParam("\\WIDTH", 4);
- cell->setParam("\\LUT", cell->getParam("\\LUT_INIT"));
- cell->unsetParam("\\LUT_INIT");
-
- cell->setPort("\\A", SigSpec({
- get_bit_or_zero(cell->getPort("\\I0")),
- get_bit_or_zero(cell->getPort("\\I1")),
- get_bit_or_zero(cell->getPort("\\I2")),
- get_bit_or_zero(cell->getPort("\\I3"))
- }));
- cell->setPort("\\Y", cell->getPort("\\O")[0]);
- cell->unsetPort("\\I0");
- cell->unsetPort("\\I1");
- cell->unsetPort("\\I2");
- cell->unsetPort("\\I3");
- cell->unsetPort("\\O");
-
- cell->check();
- }
- }
-}
-
-struct Ice40UnlutPass : public Pass {
- Ice40UnlutPass() : Pass("ice40_unlut", "iCE40: transform SB_LUT4 cells to $lut cells") { }
- void help() YS_OVERRIDE
- {
- // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
- log("\n");
- log(" ice40_unlut [options] [selection]\n");
- log("\n");
- log("This command transforms all SB_LUT4 cells to generic $lut cells.\n");
- log("\n");
- }
- void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
- {
- log_header(design, "Executing ICE40_UNLUT pass (convert SB_LUT4 to $lut).\n");
- log_push();
-
- size_t argidx;
- for (argidx = 1; argidx < args.size(); argidx++) {
- // if (args[argidx] == "-???") {
- // continue;
- // }
- break;
- }
- extra_args(args, argidx, design);
-
- for (auto module : design->selected_modules())
- run_ice40_unlut(module);
- }
-} Ice40UnlutPass;
-
-PRIVATE_NAMESPACE_END
diff --git a/techlibs/ice40/synth_ice40.cc b/techlibs/ice40/synth_ice40.cc
index be60a0071..8f4a0f377 100644
--- a/techlibs/ice40/synth_ice40.cc
+++ b/techlibs/ice40/synth_ice40.cc
@@ -238,7 +238,7 @@ struct SynthIce40Pass : public ScriptPass
{
if (check_label("begin"))
{
- run("read_verilog -icells -lib -D_ABC +/ice40/cells_sim.v");
+ run("read_verilog -icells -lib +/ice40/cells_sim.v");
run(stringf("hierarchy -check %s", help_mode ? "-top <top>" : top_opt.c_str()));
run("proc");
}
@@ -293,8 +293,10 @@ struct SynthIce40Pass : public ScriptPass
{
if (nocarry)
run("techmap");
- else
- run("techmap -map +/techmap.v -map +/ice40/arith_map.v" + std::string(abc == "abc9" ? " -D _ABC" : ""));
+ else {
+ run("ice40_wrapcarry");
+ run("techmap -map +/techmap.v -map +/ice40/arith_map.v");
+ }
if (retime || help_mode)
run(abc + " -dff", "(only if -retime)");
run("ice40_opt");
@@ -309,7 +311,7 @@ struct SynthIce40Pass : public ScriptPass
run("opt_merge");
run(stringf("dff2dffe -unmap-mince %d", min_ce_use));
}
- run("techmap -D NO_LUT -map +/ice40/cells_map.v");
+ run("techmap -D NO_LUT -D NO_ADDER -map +/ice40/cells_map.v");
run("opt_expr -mux_undef");
run("simplemap");
run("ice40_ffinit");
@@ -338,13 +340,12 @@ struct SynthIce40Pass : public ScriptPass
else
wire_delay = 250;
run(abc + stringf(" -W %d -lut +/ice40/abc_%s.lut -box +/ice40/abc_%s.box", wire_delay, device_opt.c_str(), device_opt.c_str()), "(skip if -noabc)");
- run("techmap -D NO_LUT -D _ABC -map +/ice40/cells_map.v");
}
else
run(abc + " -dress -lut 4", "(skip if -noabc)");
}
+ run("techmap -D NO_LUT -map +/ice40/cells_map.v");
run("clean");
- run("ice40_unlut");
run("opt_lut -dlogic SB_CARRY:I0=2:I1=1:CI=0");
}
diff --git a/techlibs/ice40/tests/test_arith.ys b/techlibs/ice40/tests/test_arith.ys
index 160c767fb..ddb80b700 100644
--- a/techlibs/ice40/tests/test_arith.ys
+++ b/techlibs/ice40/tests/test_arith.ys
@@ -1,6 +1,5 @@
read_verilog test_arith.v
synth_ice40
-techmap -map ../cells_sim.v
rename test gate
read_verilog test_arith.v
@@ -8,3 +7,11 @@ rename test gold
miter -equiv -flatten -make_outputs gold gate miter
sat -verify -prove trigger 0 -show-ports miter
+
+synth_ice40 -top gate
+
+read_verilog test_arith.v
+rename test gold
+
+miter -equiv -flatten -make_outputs gold gate miter
+sat -verify -prove trigger 0 -show-ports miter
diff --git a/tests/various/opt_expr.ys b/tests/opt/opt_expr.ys
index 0c61ac881..0c61ac881 100644
--- a/tests/various/opt_expr.ys
+++ b/tests/opt/opt_expr.ys
diff --git a/tests/opt/opt_ff.v b/tests/opt/opt_ff.v
deleted file mode 100644
index a01b64b61..000000000
--- a/tests/opt/opt_ff.v
+++ /dev/null
@@ -1,21 +0,0 @@
-module top(
- input clk,
- input rst,
- input [2:0] a,
- output [1:0] b
-);
- reg [2:0] b_reg;
- initial begin
- b_reg <= 3'b0;
- end
-
- assign b = b_reg[1:0];
- always @(posedge clk or posedge rst) begin
- if(rst) begin
- b_reg <= 3'b0;
- end else begin
- b_reg <= a;
- end
- end
-endmodule
-
diff --git a/tests/opt/opt_ff.ys b/tests/opt/opt_ff.ys
deleted file mode 100644
index 704c7acf3..000000000
--- a/tests/opt/opt_ff.ys
+++ /dev/null
@@ -1,3 +0,0 @@
-read_verilog opt_ff.v
-synth_ice40
-ice40_unlut
diff --git a/tests/opt/opt_lut.ys b/tests/opt/opt_lut.ys
index 59b12c351..a9fccbb62 100644
--- a/tests/opt/opt_lut.ys
+++ b/tests/opt/opt_lut.ys
@@ -1,4 +1,2 @@
read_verilog opt_lut.v
-synth_ice40
-ice40_unlut
-equiv_opt -map +/ice40/cells_sim.v -assert opt_lut -dlogic SB_CARRY:I0=1:I1=2:CI=3
+equiv_opt -map +/ice40/cells_sim.v -assert synth_ice40
diff --git a/tests/various/opt_rmdff.v b/tests/opt/opt_rmdff.v
index b1c06703c..b1c06703c 100644
--- a/tests/various/opt_rmdff.v
+++ b/tests/opt/opt_rmdff.v
diff --git a/tests/various/opt_rmdff.ys b/tests/opt/opt_rmdff.ys
index 081f81782..081f81782 100644
--- a/tests/various/opt_rmdff.ys
+++ b/tests/opt/opt_rmdff.ys
diff --git a/tests/opt/opt_ff_sat.v b/tests/opt/opt_rmdff_sat.v
index 5a0a6fe37..5a0a6fe37 100644
--- a/tests/opt/opt_ff_sat.v
+++ b/tests/opt/opt_rmdff_sat.v
diff --git a/tests/opt/opt_ff_sat.ys b/tests/opt/opt_rmdff_sat.ys
index 4e7cc6ca4..1c3dd9c05 100644
--- a/tests/opt/opt_ff_sat.ys
+++ b/tests/opt/opt_rmdff_sat.ys
@@ -1,4 +1,4 @@
-read_verilog opt_ff_sat.v
+read_verilog opt_rmdff_sat.v
prep -flatten
opt_rmdff -sat
synth
diff --git a/tests/various/wreduce.ys b/tests/various/wreduce.ys
index 4257292f5..2e0812c48 100644
--- a/tests/various/wreduce.ys
+++ b/tests/various/wreduce.ys
@@ -36,7 +36,6 @@ design -save gold
opt_expr
wreduce
-dump
select -assert-count 1 t:$sub r:A_WIDTH=4 r:B_WIDTH=4 r:Y_WIDTH=5 %i %i %i
design -stash gate
@@ -46,3 +45,35 @@ design -import gate -as gate
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -show-ports miter
+
+##########
+
+# Testcase from: https://github.com/YosysHQ/yosys/commit/25680f6a078bb32f157bd580705656496717bafb
+design -reset
+read_verilog <<EOT
+module top(
+ input clk,
+ input rst,
+ input [2:0] a,
+ output [1:0] b
+);
+ reg [2:0] b_reg;
+ initial begin
+ b_reg <= 3'b0;
+ end
+
+ assign b = b_reg[1:0];
+ always @(posedge clk or posedge rst) begin
+ if(rst) begin
+ b_reg <= 3'b0;
+ end else begin
+ b_reg <= a;
+ end
+ end
+endmodule
+EOT
+
+proc
+wreduce
+
+select -assert-count 1 t:$adff r:ARST_VALUE=2'b00 %i