Skip to content

Commit

Permalink
[XLS] Remove conditional specialization for operands of Boolean opera…
Browse files Browse the repository at this point in the history 
…tions

It's not safe to specialize all operands of a Boolean operation at the same time based on visibility; this can only be done asymmetrically, or else we risk accidentally excluding cases where all operands are true.

For example, it's true that when considering

    OR(A, B),

we can assume that B is false while simplifying A, since the value of A is irrelevant whenever B is true. We can similarly assume that A is false while simplifying B.

However... we can't do these at the same time. To see why, suppose it turns out that A = X and B = X (i.e., that A and B are logically equivalent). In this case, we might try to simplify

    OR(A, B)

by replacing A with its value whenever B = 0 (i.e., replacing A with 0) and B with its value whenever A = 0 (i.e., replacing B with 0). This means we'd replace the expression with:

    OR(0, 0) = 0.

However, if X is true, OR(A, B) = OR(1, 1) = 1.

PiperOrigin-RevId: 710762944
  • Loading branch information
@ericastor @copybara-github
ericastor authored and copybara-github committed Dec 30, 2024
1 parent 7da9772 commit 4651f2e
Show file tree
Hide file tree
Showing 2 changed files with 0 additions and 130 deletions.
39 changes: 0 additions & 39 deletions xls/passes/conditional_specialization_pass.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -664,45 +664,6 @@ absl::StatusOr<bool> ConditionalSpecializationPass::RunOnFunctionBaseInternal(
std::move(edge_set));
}

// The operands of single-bit logical operations may not be observable
// depending on the value of the *other* operands. For example, given:
//
// OR(X, Y, Z)
//
// The value X is not observable if Y or Z is one, so we can assume in the
// computation of X that Y and Z are zero. Similar assumptions can be made
// for other logical operations (NOR, NAD, NAND).
//
// This can only be used when a (BDD) query engine is *not* used because as
// soon as the graph is transformed the query engine becomes stale. This is
// not the case with the select-based transformations because of the mutual
// exclusion of the assumed conditions.
//
// TODO(b/323003986): Incrementally update the BDD.
if ((node->op() == Op::kOr || node->op() == Op::kNor ||
node->op() == Op::kAnd || node->op() == Op::kNand) &&
node->BitCountOrDie() == 1 && !use_bdd_) {
// The value you can assume other operands have in the computation of this
// operand.
TernaryValue assumed_operand_value =
(node->op() == Op::kOr || node->op() == Op::kNor)
? TernaryValue::kKnownZero
: TernaryValue::kKnownOne;
for (int64_t i = 0; i < node->operand_count(); ++i) {
if (node->operand(i)->Is<Literal>()) {
continue;
}
ConditionSet edge_set = set;
for (int64_t j = 0; j < node->operand_count(); ++j) {
if (i != j && !node->operand(j)->Is<Literal>()) {
edge_set.AddCondition(Condition{.node = node->operand(j),
.value = {assumed_operand_value}});
}
}
condition_map.SetEdgeConditionSet(node, i, std::move(edge_set));
}
}

if (node->Is<Send>()) {
Send* send = node->As<Send>();
if (!send->predicate().has_value()) {
Expand Down
91 changes: 0 additions & 91 deletions xls/passes/conditional_specialization_pass_test.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1072,96 +1072,5 @@ TEST_F(ConditionalSpecializationPassTest, NextValueChange) {
m::StateRead("value2"), m::Eq())));
}

TEST_F(ConditionalSpecializationPassTest, LogicalAndImpliedValue) {
// AND(a, OR(a, b)) => AND(a, OR(1, b))
auto p = CreatePackage();
FunctionBuilder fb(TestName(), p.get());
Type* u1 = p->GetBitsType(1);
BValue a = fb.Param("a", u1);
BValue b = fb.Param("b", u1);
BValue result = fb.And(a, fb.Or(a, b));

XLS_ASSERT_OK_AND_ASSIGN(Function * f, fb.BuildWithReturnValue(result));

EXPECT_THAT(Run(f, /*use_bdd=*/false), IsOkAndHolds(true));

EXPECT_THAT(f->return_value(),
m::And(m::Param("a"), m::Or(m::Literal(1), m::Param("b"))));
}

TEST_F(ConditionalSpecializationPassTest,
LogicalAndImpliedValueWithQueryEngine) {
// Can't perform logical op based specialization if BDDs are used.
auto p = CreatePackage();
FunctionBuilder fb(TestName(), p.get());
Type* u1 = p->GetBitsType(1);
BValue a = fb.Param("a", u1);
BValue b = fb.Param("b", u1);
BValue result = fb.And(a, fb.Or(a, b));

XLS_ASSERT_OK_AND_ASSIGN(Function * f, fb.BuildWithReturnValue(result));

EXPECT_THAT(Run(f, /*use_bdd=*/true), IsOkAndHolds(false));
}

TEST_F(ConditionalSpecializationPassTest, LogicalNorImpliedValue) {
// NOR(a, Add(a, b)) => NOR(a, Add(0, b))
auto p = CreatePackage();
FunctionBuilder fb(TestName(), p.get());
Type* u1 = p->GetBitsType(1);
BValue a = fb.Param("a", u1);
BValue b = fb.Param("b", u1);
BValue result = fb.Nor(a, fb.Add(a, b));

XLS_ASSERT_OK_AND_ASSIGN(Function * f, fb.BuildWithReturnValue(result));

EXPECT_THAT(Run(f, /*use_bdd=*/false), IsOkAndHolds(true));

EXPECT_THAT(f->return_value(),
m::Nor(m::Param("a"), m::Add(m::Literal(0), m::Param("b"))));
}

// Verify that we correctly track which value is the identity for a given
// bitwise operation.
//
// Discovered by fuzz-testing as crasher 0031623b.
TEST_F(ConditionalSpecializationPassTest, CorrectIdentityValueTracked) {
auto p = CreatePackage();
FunctionBuilder fb(TestName(), p.get());
Type* u1 = p->GetBitsType(1);
BValue x = fb.Param("x", u1);
BValue false_literal = fb.Literal(UBits(0, 1));
BValue and_v = fb.And(x, false_literal);
BValue or_v = fb.Or(and_v, false_literal);
BValue result = fb.Concat({or_v});

XLS_ASSERT_OK_AND_ASSIGN(Function * f, fb.BuildWithReturnValue(result));

solvers::z3::ScopedVerifyEquivalence sve{f};
EXPECT_THAT(Run(f, /*use_bdd=*/false), IsOkAndHolds(true));
EXPECT_THAT(f->return_value(),
m::Concat(m::And(m::Param("x"), m::Literal(0))));
}

// Verify that we correctly handle scenarios where it's provably impossible for
// one arm to be chosen.
//
// Discovered by fuzz-testing as crasher e8f52f00.
TEST_F(ConditionalSpecializationPassTest, ImpossibleArm) {
auto p = CreatePackage();
FunctionBuilder fb(TestName(), p.get());
BValue false_literal = fb.Literal(UBits(0, 1));
BValue false_or = fb.Or(false_literal, false_literal);
BValue priority_sel =
fb.PrioritySelect(false_or, {false_literal}, false_literal);
BValue nor = fb.Nor({false_literal, false_or, priority_sel});
BValue result = fb.And({nor, false_literal, false_or});
XLS_ASSERT_OK_AND_ASSIGN(Function * f, fb.BuildWithReturnValue(result));

solvers::z3::ScopedVerifyEquivalence sve{f};
EXPECT_THAT(Run(f, /*use_bdd=*/false), IsOkAndHolds(true));
EXPECT_THAT(f->return_value(), m::And(m::Nor(), m::Literal(0), m::Or()));
}

} // namespace
} // namespace xls

0 comments on commit 4651f2e

Please sign in to comment.