Skip to content

Commit 24aa54f

Browse files
copybara-githubcopybara-github
committed
Merge pull request #2251 from xlsynth:cdleary/2025-05-22-array-cmp-check-ir-equivalence
PiperOrigin-RevId: 764813017
2 parents 57016cb + 8179ea8 commit 24aa54f

File tree

3 files changed

+129
-21
lines changed

3 files changed

+129
-21
lines changed

‎xls/ir/verifier_test.cc

Lines changed: 86 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -248,6 +248,86 @@ fn f() -> bits[0] {
248248
XLS_EXPECT_OK(VerifyPackage(p.get()));
249249
}
250250

251+
TEST_F(VerifierTest, NumericCompareArrayOperands) {
252+
std::string input = R"(
253+
package p
254+
255+
fn f(a: bits[32][4], b: bits[32][4]) -> bits[1] {
256+
ret ult.1: bits[1] = ult(a, b)
257+
}
258+
)";
259+
XLS_ASSERT_OK_AND_ASSIGN(auto p, ParsePackageNoVerify(input));
260+
EXPECT_THAT(VerifyPackage(p.get()),
261+
StatusIs(absl::StatusCode::kInternal,
262+
HasSubstr("Expected operand 0 of ult.1 to have Bits "
263+
"type, has type bits[32][4]")));
264+
}
265+
266+
TEST_F(VerifierTest, NumericCompareTupleOperands) {
267+
std::string input = R"(
268+
package p
269+
270+
fn f(a: (bits[32], bits[16]), b: (bits[32], bits[16])) -> bits[1] {
271+
ret sge.1: bits[1] = sge(a, b)
272+
}
273+
)";
274+
XLS_ASSERT_OK_AND_ASSIGN(auto p, ParsePackageNoVerify(input));
275+
EXPECT_THAT(VerifyPackage(p.get()),
276+
StatusIs(absl::StatusCode::kInternal,
277+
HasSubstr("Expected operand 0 of sge.1 to have Bits "
278+
"type, has type (bits[32], bits[16])")));
279+
}
280+
281+
TEST_F(VerifierTest, NumericCompareMismatchedBitWidths) {
282+
std::string input = R"(
283+
package p
284+
285+
fn f(a: bits[32], b: bits[16]) -> bits[1] {
286+
ret ugt.1: bits[1] = ugt(a, b)
287+
}
288+
)";
289+
XLS_ASSERT_OK_AND_ASSIGN(auto p, ParsePackageNoVerify(input));
290+
EXPECT_THAT(
291+
VerifyPackage(p.get()),
292+
StatusIs(absl::StatusCode::kInternal,
293+
HasSubstr("Expected operand 1 of ugt.1 to have bit "
294+
"count 32 (same as operand 0), has bit count 16")));
295+
}
296+
297+
TEST_F(VerifierTest, EqCompareTokenOperands) {
298+
std::string input = R"(
299+
package p
300+
301+
fn f() -> bits[1] {
302+
tok_a: token = literal(value=token, id=1)
303+
tok_b: token = literal(value=token, id=2)
304+
ret eq_val: bits[1] = eq(tok_a, tok_b, id=3)
305+
}
306+
)";
307+
XLS_ASSERT_OK_AND_ASSIGN(auto p, ParsePackageNoVerify(input));
308+
EXPECT_THAT(VerifyPackage(p.get()),
309+
StatusIs(absl::StatusCode::kInternal,
310+
HasSubstr("Operand 0 of eq_val cannot be Token type "
311+
"for this operation")));
312+
}
313+
314+
TEST_F(VerifierTest, NeCompareTokenOperands) {
315+
std::string input = R"(
316+
package p
317+
318+
fn f() -> bits[1] {
319+
tok_a: token = literal(value=token, id=1)
320+
tok_b: token = literal(value=token, id=2)
321+
ret ne_val: bits[1] = ne(tok_a, tok_b, id=3)
322+
}
323+
)";
324+
XLS_ASSERT_OK_AND_ASSIGN(auto p, ParsePackageNoVerify(input));
325+
EXPECT_THAT(VerifyPackage(p.get()),
326+
StatusIs(absl::StatusCode::kInternal,
327+
HasSubstr("Operand 0 of ne_val cannot be Token type "
328+
"for this operation")));
329+
}
330+
251331
TEST_F(VerifierTest, SelectWithTooNarrowSelector) {
252332
std::string input = R"(
253333
package p
@@ -404,11 +484,12 @@ fn main(invariant_1: bits[48], invariant_2: bits[64], stride: bits[16], trip_cou
404484
}
405485
)";
406486
XLS_ASSERT_OK_AND_ASSIGN(auto p, ParsePackageNoVerify(input));
407-
EXPECT_THAT(VerifyPackage(p.get()),
408-
StatusIs(absl::StatusCode::kInternal,
409-
HasSubstr("Parameter 1 (accumulator) of function body "
410-
"used as dynamic_counted_for body should have "
411-
"bits[32] type, got bits[128] instead")));
487+
EXPECT_THAT(
488+
VerifyPackage(p.get()),
489+
StatusIs(absl::StatusCode::kInternal,
490+
HasSubstr("Parameter 1 (accumulator) of function body used as "
491+
"dynamic_counted_for body should have bits[32] type, "
492+
"got bits[128] instead")));
412493
}
413494

414495
TEST_F(VerifierTest, DynamicCountedForInvariantDoesNotMatchBodyParamType) {

‎xls/ir/verify_node.cc

Lines changed: 41 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -551,31 +551,31 @@ class NodeChecker : public DfsVisitor {
551551

552552
absl::Status HandleEq(CompareOp* eq) override {
553553
XLS_RETURN_IF_ERROR(ExpectOperandCount(eq, 2));
554-
XLS_RETURN_IF_ERROR(ExpectOperandsSameBitsType(eq));
554+
XLS_RETURN_IF_ERROR(ExpectOperandsSameTypeNoToken(eq));
555555
return ExpectHasBitsType(eq, /*expected_bit_count=*/1);
556556
}
557557

558558
absl::Status HandleUGe(CompareOp* ge) override {
559559
XLS_RETURN_IF_ERROR(ExpectOperandCount(ge, 2));
560-
XLS_RETURN_IF_ERROR(ExpectOperandsSameBitsType(ge));
560+
XLS_RETURN_IF_ERROR(ExpectOperandsAreBitsAndSameWidth(ge));
561561
return ExpectHasBitsType(ge, /*expected_bit_count=*/1);
562562
}
563563

564564
absl::Status HandleUGt(CompareOp* gt) override {
565565
XLS_RETURN_IF_ERROR(ExpectOperandCount(gt, 2));
566-
XLS_RETURN_IF_ERROR(ExpectOperandsSameBitsType(gt));
566+
XLS_RETURN_IF_ERROR(ExpectOperandsAreBitsAndSameWidth(gt));
567567
return ExpectHasBitsType(gt, /*expected_bit_count=*/1);
568568
}
569569

570570
absl::Status HandleSGe(CompareOp* ge) override {
571571
XLS_RETURN_IF_ERROR(ExpectOperandCount(ge, 2));
572-
XLS_RETURN_IF_ERROR(ExpectOperandsSameBitsType(ge));
572+
XLS_RETURN_IF_ERROR(ExpectOperandsAreBitsAndSameWidth(ge));
573573
return ExpectHasBitsType(ge, /*expected_bit_count=*/1);
574574
}
575575

576576
absl::Status HandleSGt(CompareOp* gt) override {
577577
XLS_RETURN_IF_ERROR(ExpectOperandCount(gt, 2));
578-
XLS_RETURN_IF_ERROR(ExpectOperandsSameBitsType(gt));
578+
XLS_RETURN_IF_ERROR(ExpectOperandsAreBitsAndSameWidth(gt));
579579
return ExpectHasBitsType(gt, /*expected_bit_count=*/1);
580580
}
581581

@@ -715,24 +715,24 @@ class NodeChecker : public DfsVisitor {
715715

716716
absl::Status HandleULe(CompareOp* le) override {
717717
XLS_RETURN_IF_ERROR(ExpectOperandCount(le, 2));
718-
XLS_RETURN_IF_ERROR(ExpectOperandsSameBitsType(le));
718+
XLS_RETURN_IF_ERROR(ExpectOperandsAreBitsAndSameWidth(le));
719719
return ExpectHasBitsType(le, /*expected_bit_count=*/1);
720720
}
721721

722722
absl::Status HandleULt(CompareOp* lt) override {
723723
XLS_RETURN_IF_ERROR(ExpectOperandCount(lt, 2));
724-
XLS_RETURN_IF_ERROR(ExpectOperandsSameBitsType(lt));
724+
XLS_RETURN_IF_ERROR(ExpectOperandsAreBitsAndSameWidth(lt));
725725
return ExpectHasBitsType(lt, /*expected_bit_count=*/1);
726726
}
727727
absl::Status HandleSLe(CompareOp* le) override {
728728
XLS_RETURN_IF_ERROR(ExpectOperandCount(le, 2));
729-
XLS_RETURN_IF_ERROR(ExpectOperandsSameBitsType(le));
729+
XLS_RETURN_IF_ERROR(ExpectOperandsAreBitsAndSameWidth(le));
730730
return ExpectHasBitsType(le, /*expected_bit_count=*/1);
731731
}
732732

733733
absl::Status HandleSLt(CompareOp* lt) override {
734734
XLS_RETURN_IF_ERROR(ExpectOperandCount(lt, 2));
735-
XLS_RETURN_IF_ERROR(ExpectOperandsSameBitsType(lt));
735+
XLS_RETURN_IF_ERROR(ExpectOperandsAreBitsAndSameWidth(lt));
736736
return ExpectHasBitsType(lt, /*expected_bit_count=*/1);
737737
}
738738

@@ -836,7 +836,7 @@ class NodeChecker : public DfsVisitor {
836836

837837
absl::Status HandleNe(CompareOp* ne) override {
838838
XLS_RETURN_IF_ERROR(ExpectOperandCount(ne, 2));
839-
XLS_RETURN_IF_ERROR(ExpectOperandsSameBitsType(ne));
839+
XLS_RETURN_IF_ERROR(ExpectOperandsSameTypeNoToken(ne));
840840
return ExpectHasBitsType(ne, /*expected_bit_count=*/1);
841841
}
842842

@@ -1465,12 +1465,41 @@ class NodeChecker : public DfsVisitor {
14651465
return absl::OkStatus();
14661466
}
14671467

1468-
// Verifies all operands are BitsType with the same bit count.
1469-
absl::Status ExpectOperandsSameBitsType(Node* node) const {
1468+
// Verifies all operands are BitsType with the same bit count as the first
1469+
// operand.
1470+
absl::Status ExpectOperandsAreBitsAndSameWidth(Node* node) const {
14701471
if (node->operand_count() == 0) {
14711472
return absl::OkStatus();
14721473
}
1474+
XLS_RETURN_IF_ERROR(ExpectOperandHasBitsType(node, 0));
14731475
Type* type = node->operand(0)->GetType();
1476+
// Already checked operand 0 is BitsType. Now check other operands.
1477+
for (int64_t i = 1; i < node->operand_count(); ++i) {
1478+
XLS_RETURN_IF_ERROR(ExpectOperandHasBitsType(node, i));
1479+
if (node->operand(i)->GetType()->AsBitsOrDie()->bit_count() !=
1480+
type->AsBitsOrDie()->bit_count()) {
1481+
return absl::InternalError(absl::StrFormat(
1482+
"Expected operand %d of %s to have bit count %d (same as operand "
1483+
"0), has bit count %d: %s",
1484+
i, node->GetName(), type->AsBitsOrDie()->bit_count(),
1485+
node->operand(i)->GetType()->AsBitsOrDie()->bit_count(),
1486+
node->ToString()));
1487+
}
1488+
}
1489+
return absl::OkStatus();
1490+
}
1491+
1492+
// Verifies all operands are the same type, and that type is not Token.
1493+
absl::Status ExpectOperandsSameTypeNoToken(Node* node) const {
1494+
if (node->operand_count() == 0) {
1495+
return absl::OkStatus();
1496+
}
1497+
Type* type = node->operand(0)->GetType();
1498+
if (type->IsToken()) {
1499+
return absl::InternalError(absl::StrFormat(
1500+
"Operand 0 of %s cannot be Token type for this operation: %s",
1501+
node->GetName(), node->ToString()));
1502+
}
14741503
for (int64_t i = 1; i < node->operand_count(); ++i) {
14751504
XLS_RETURN_IF_ERROR(ExpectOperandHasType(node, i, type));
14761505
}

‎xls/jit/function_jit_test.cc

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -899,11 +899,9 @@ TEST(FunctionJitTest, TokenCompareError) {
899899

900900
b.Eq(p0, p0);
901901

902-
XLS_ASSERT_OK_AND_ASSIGN(Function * f, b.Build());
903-
904-
EXPECT_THAT(FunctionJit::Create(f),
902+
EXPECT_THAT(b.Build(),
905903
StatusIs(absl::StatusCode::kInvalidArgument,
906-
HasSubstr("Tokens are incomparable")));
904+
HasSubstr("cannot be Token type for this operation")));
907905
}
908906

909907
// Make sure the token comparison error is still reported when the token is

0 commit comments

Comments
 (0)