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

Merge pull request #5986 from YosysHQ/nella/x-wildcard

fix case item containing x/z treated as wildcard in proc_rmdead
This commit is contained in:
nella 2026-07-07 08:00:02 +00:00 committed by GitHub
commit 8a2499b544
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 68 additions and 0 deletions

View file

@ -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)) {

View file

@ -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

View file

@ -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