diff --git a/kernel/bitpattern.h b/kernel/bitpattern.h index e2071436c..848a753a5 100644 --- a/kernel/bitpattern.h +++ b/kernel/bitpattern.h @@ -107,6 +107,18 @@ struct BitPatternPool return bits; } + /** + * A literal x/z bit can never match a 2-valued selector, so a pattern containing + * one covers nothing. + */ + static bool covers_nothing(RTLIL::SigSpec sig) + { + for (auto bit : sig) + if (bit.wire == NULL && (bit.data == RTLIL::State::Sx || bit.data == RTLIL::State::Sz)) + return true; + return false; + } + /** * Two cubes match if their intersection is non-empty. */ @@ -131,6 +143,8 @@ struct BitPatternPool */ bool has_any(RTLIL::SigSpec sig) { + if (covers_nothing(sig)) + return false; bits_t bits = sig2bits(sig); for (auto &it : database) if (match(it, bits)) @@ -149,6 +163,8 @@ struct BitPatternPool */ bool has_all(RTLIL::SigSpec sig) { + if (covers_nothing(sig)) + return true; bits_t bits = sig2bits(sig); for (auto &it : database) if (match(it, bits)) { @@ -170,6 +186,8 @@ struct BitPatternPool bool take(RTLIL::SigSpec sig) { bool status = false; + if (covers_nothing(sig)) + return false; bits_t bits = sig2bits(sig); for (auto it = database.begin(); it != database.end();) if (match(*it, bits)) { diff --git a/tests/proc/rmdead_case_x.ys b/tests/proc/rmdead_case_x.ys new file mode 100644 index 000000000..6a44ec462 --- /dev/null +++ b/tests/proc/rmdead_case_x.ys @@ -0,0 +1,40 @@ +# https://github.com/YosysHQ/yosys/issues/5979 + +read_verilog -sv << EOF +module top ( + input wire [1:0] sel, + input wire [3:0] a, + input wire [3:0] b, + output reg [3:0] y +); + always @* begin + case (sel) + 2'b1x: y = a; + 2'b10: y = b; + default: y = a; + endcase + end +endmodule + +module gold ( + input wire [1:0] sel, + input wire [3:0] a, + input wire [3:0] b, + output reg [3:0] y +); + always @* begin + if (sel == 2'b10) y = b; + else y = a; + end +endmodule +EOF + +proc +opt -full + +select -assert-count 1 top/o:y %ci* top/i:b %i + +equiv_make gold top equiv +cd equiv +equiv_simple +equiv_status -assert diff --git a/tests/unit/kernel/bitpatternTest.cc b/tests/unit/kernel/bitpatternTest.cc index 001d47060..a641b85a3 100644 --- a/tests/unit/kernel/bitpatternTest.cc +++ b/tests/unit/kernel/bitpatternTest.cc @@ -11,6 +11,8 @@ TEST(BitpatternTest, has) SigSpec _01a = {RTLIL::S0, RTLIL::S1, RTLIL::Sa}; SigSpec _011 = {RTLIL::S0, RTLIL::S1, RTLIL::S1}; SigSpec _111 = {RTLIL::S1, RTLIL::S1, RTLIL::S1}; + SigSpec _01x = {RTLIL::S0, RTLIL::S1, RTLIL::Sx}; + SigSpec _01z = {RTLIL::S0, RTLIL::S1, RTLIL::Sz}; EXPECT_TRUE(BitPatternPool(_aaa).has_any(_01a)); EXPECT_TRUE(BitPatternPool(_01a).has_any(_01a)); @@ -19,6 +21,10 @@ TEST(BitpatternTest, has) // overlap is symmetric EXPECT_TRUE(BitPatternPool(_01a).has_any(_011)); EXPECT_FALSE(BitPatternPool(_111).has_any(_01a)); + // overlaps nothing + EXPECT_FALSE(BitPatternPool(_011).has_any(_01x)); + EXPECT_FALSE(BitPatternPool(_011).has_any(_01z)); + EXPECT_FALSE(BitPatternPool(_aaa).has_any(_01x)); EXPECT_TRUE(BitPatternPool(_aaa).has_all(_01a)); EXPECT_TRUE(BitPatternPool(_01a).has_all(_01a)); @@ -27,6 +33,10 @@ TEST(BitpatternTest, has) // 01a is not covered by 011 EXPECT_FALSE(BitPatternPool(_011).has_all(_01a)); EXPECT_FALSE(BitPatternPool(_111).has_all(_01a)); + // trivially covered by any pool + EXPECT_TRUE(BitPatternPool(_011).has_all(_01x)); + EXPECT_TRUE(BitPatternPool(_011).has_all(_01z)); + EXPECT_TRUE(BitPatternPool(_111).has_all(_01x)); } YOSYS_NAMESPACE_END