[Comb] Canonicalize using De Morgan's laws (#2668)

Resolves #2666.
This commit is contained in:
sinofp 2022-02-25 23:13:36 +00:00 committed by GitHub
parent 409af169f1
commit 727db57a3a
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
9 changed files with 67 additions and 34 deletions

View File

@ -49,6 +49,10 @@ Value createOrFoldSExt(Location loc, Value value, Type destTy,
OpBuilder &builder);
Value createOrFoldSExt(Value value, Type destTy, ImplicitLocOpBuilder &builder);
/// Create a ``Not'' gate on a value.
Value createOrFoldNot(Location loc, Value value, OpBuilder &builder);
Value createOrFoldNot(Value value, ImplicitLocOpBuilder &builder);
} // namespace comb
} // namespace circt

View File

@ -3645,7 +3645,6 @@ LogicalResult FIRRTLLowering::lowerVerificationStatement(
}
auto boolType = IntegerType::get(builder.getContext(), 1);
auto allOnes = builder.create<hw::ConstantOp>(APInt::getAllOnesValue(1));
// Handle the `ifElseFatal` format, which does not emit an SVA but
// rather a process that uses $error and $fatal to perform the checks.
@ -3653,7 +3652,7 @@ LogicalResult FIRRTLLowering::lowerVerificationStatement(
// option that the user of this pass can choose.
auto format = op->template getAttrOfType<StringAttr>("format");
if (format && format.getValue() == "ifElseFatal") {
predicate = builder.createOrFold<comb::XorOp>(predicate, allOnes);
predicate = comb::createOrFoldNot(predicate, builder);
predicate = builder.createOrFold<comb::AndOp>(enable, predicate);
addToAlwaysBlock(clock, [&]() {
addToIfDefProceduralBlock("SYNTHESIS", {}, [&]() {
@ -3674,7 +3673,7 @@ LogicalResult FIRRTLLowering::lowerVerificationStatement(
}
// Formulate the `enable -> predicate` as `!enable | predicate`.
auto notEnable = builder.createOrFold<comb::XorOp>(enable, allOnes);
auto notEnable = comb::createOrFoldNot(enable, builder);
predicate = builder.createOrFold<comb::OrOp>(notEnable, predicate);
// Handle the regular SVA case.

View File

@ -132,8 +132,7 @@ void CompileControlVisitor::visit(SeqOp seq, ComponentOp &component) {
// (2) the done signal of this group is not high.
auto eqCmp = builder.create<comb::ICmpOp>(
wires->getLoc(), comb::ICmpPredicate::eq, fsmOut, fsmCurrentState);
auto notDone =
builder.create<comb::XorOp>(wires->getLoc(), doneOpValue, oneConstant);
auto notDone = comb::createOrFoldNot(wires->getLoc(), doneOpValue, builder);
auto groupGoGuard =
builder.create<comb::AndOp>(wires->getLoc(), eqCmp, notDone);

View File

@ -1227,6 +1227,30 @@ LogicalResult XorOp::canonicalize(XorOp op, PatternRewriter &rewriter) {
auto size = inputs.size();
assert(size > 1 && "expected 2 or more operands");
// Check De Morgan's laws
Value sub;
if (matchPattern(static_cast<Operation *>(op), m_Complement(m_Any(&sub)))) {
auto getNegations = [&](auto term) {
SmallVector<Value, 2> negations;
auto operands = term->getOperands();
negations.reserve(operands.size());
llvm::transform(operands, std::back_inserter(negations), [&](Value x) {
return createOrFoldNot(op.getLoc(), x, rewriter);
});
return negations;
};
if (auto disjunction = sub.getDefiningOp<OrOp>()) {
rewriter.replaceOpWithNewOp<AndOp>(op, op.getType(),
getNegations(disjunction));
return success();
}
if (auto conjunction = sub.getDefiningOp<AndOp>()) {
rewriter.replaceOpWithNewOp<OrOp>(op, op.getType(),
getNegations(conjunction));
return success();
}
}
// xor(..., x, x) -> xor (...) -- idempotent
if (inputs[size - 1] == inputs[size - 2]) {
assert(size > 2 &&
@ -1923,11 +1947,6 @@ static bool foldCommonMuxValue(MuxOp op, bool isTrueOperand,
// If we got a hit, then go ahead and simplify it!
Value cond = op.cond();
auto invertBoolValue = [&](Value value) -> Value {
auto one = rewriter.create<hw::ConstantOp>(op.getLoc(), APInt(1, 1));
return rewriter.createOrFold<XorOp>(op.getLoc(), value, one);
};
// `mux(cond, a, mux(cond2, a, b))` -> `mux(cond|cond2, a, b)`
// `mux(cond, a, mux(cond2, b, a))` -> `mux(cond|~cond2, a, b)`
// `mux(cond, mux(cond2, a, b), a)` -> `mux(~cond|cond2, a, b)`
@ -1941,7 +1960,7 @@ static bool foldCommonMuxValue(MuxOp op, bool isTrueOperand,
otherValue = subMux.falseValue();
else if (subMux.falseValue() == commonValue) {
otherValue = subMux.trueValue();
subCond = invertBoolValue(subCond);
subCond = createOrFoldNot(op.getLoc(), subCond, rewriter);
} else {
// We can't fold `mux(cond, a, mux(a, x, y))`.
return false;
@ -1949,7 +1968,7 @@ static bool foldCommonMuxValue(MuxOp op, bool isTrueOperand,
// Invert the outer cond if needed, and combine the mux conditions.
if (!isTrueOperand)
cond = invertBoolValue(cond);
cond = createOrFoldNot(op.getLoc(), cond, rewriter);
cond = rewriter.createOrFold<OrOp>(op.getLoc(), cond, subCond);
rewriter.replaceOpWithNewOp<MuxOp>(op, cond, commonValue, otherValue);
return true;
@ -1959,7 +1978,7 @@ static bool foldCommonMuxValue(MuxOp op, bool isTrueOperand,
// TrueOperand, And inverts for False operand.
bool isaAndOp = isa<AndOp>(subExpr);
if (isTrueOperand ^ isaAndOp)
cond = invertBoolValue(cond);
cond = createOrFoldNot(op.getLoc(), cond, rewriter);
auto extendedCond =
rewriter.createOrFold<ReplicateOp>(op.getLoc(), op.getType(), cond);
@ -2097,9 +2116,7 @@ LogicalResult MuxOp::canonicalize(MuxOp op, PatternRewriter &rewriter) {
if (value.getBitWidth() == 1) {
// mux(a, 0, b) -> and(~a, b) for single-bit values.
if (value.isZero()) {
auto one = rewriter.create<hw::ConstantOp>(op.getLoc(), APInt(1, 1));
auto notCond =
rewriter.createOrFold<XorOp>(op.getLoc(), op.cond(), one);
auto notCond = createOrFoldNot(op.getLoc(), op.cond(), rewriter);
rewriter.replaceOpWithNewOp<AndOp>(op, notCond, op.falseValue());
return success();
}

View File

@ -45,6 +45,15 @@ Value comb::createOrFoldSExt(Value value, Type destTy,
return createOrFoldSExt(builder.getLoc(), value, destTy, builder);
}
Value comb::createOrFoldNot(Location loc, Value value, OpBuilder &builder) {
auto allOnes = builder.create<hw::ConstantOp>(loc, value.getType(), -1);
return builder.createOrFold<XorOp>(loc, value, allOnes);
}
Value comb::createOrFoldNot(Value value, ImplicitLocOpBuilder &builder) {
return createOrFoldNot(builder.getLoc(), value, builder);
}
//===----------------------------------------------------------------------===//
// ICmpOp
//===----------------------------------------------------------------------===//
@ -184,8 +193,7 @@ static LogicalResult verifyUTVariadicOp(Operation *op) {
bool XorOp::isBinaryNot() {
if (getNumOperands() != 2)
return false;
if (auto cst =
dyn_cast_or_null<hw::ConstantOp>(getOperand(1).getDefiningOp()))
if (auto cst = getOperand(1).getDefiningOp<hw::ConstantOp>())
if (cst.getValue().isAllOnes())
return true;
return false;

View File

@ -377,11 +377,7 @@ LogicalResult IfOp::canonicalize(IfOp op, PatternRewriter &rewriter) {
// Otherwise, invert the condition and move the 'else' block to the 'then'
// region.
auto full =
rewriter.create<hw::ConstantOp>(op.getLoc(), op.cond().getType(), -1);
Value ops[] = {full, op.cond()};
auto cond =
rewriter.createOrFold<comb::XorOp>(op.getLoc(), op.cond().getType(), ops);
auto cond = comb::createOrFoldNot(op.getLoc(), op.cond(), rewriter);
op.setOperand(cond);
auto *thenBlock = op.getThenBlock(), *elseBlock = op.getElseBlock();
@ -1266,11 +1262,7 @@ LogicalResult PAssignOp::canonicalize(PAssignOp op, PatternRewriter &rewriter) {
// conditional procedural assign. We've ensured that this is the only write
// of the register.
if (trueBranch) {
auto one =
rewriter.create<hw::ConstantOp>(mux.getLoc(), mux.cond().getType(), -1);
Value ops[] = {mux.cond(), one};
auto cond = rewriter.createOrFold<comb::XorOp>(mux.getLoc(),
mux.cond().getType(), ops);
auto cond = comb::createOrFoldNot(mux.getLoc(), mux.cond(), rewriter);
rewriter.create<sv::IfOp>(mux.getLoc(), cond, [&]() {
rewriter.create<PAssignOp>(op.getLoc(), reg, mux.falseValue());
});

View File

@ -1332,3 +1332,17 @@ hw.module @muxCommonOp(%cond: i1,
// CHECK: hw.output [[O1]], [[O2]], [[O3]]
hw.output %o1, %o2, %o3 : i128, i128, i128
}
// CHECK-LABEL: @deMorgan
hw.module @deMorgan(%a: i1, %b: i1) -> (c: i1, d: i1) {
// CHECK-NEXT: %0 = comb.and %a, %b : i1
// CHECK-NEXT: %1 = comb.or %a, %b : i1
%true = hw.constant true
%0 = comb.xor %true, %a : i1
%1 = comb.xor %true, %b : i1
%2 = comb.or %0, %1 : i1
%3 = comb.and %0, %1 : i1
%4 = comb.xor %true, %2 : i1
%5 = comb.xor %true, %3 : i1
hw.output %4, %5 : i1, i1
}

View File

@ -24,7 +24,7 @@ circuit Foo:
; CHECK-NEXT: `ifndef SYNTHESIS
; assert with predicate only
; CHECK-NEXT: if (enable & ~(predicate1 | reset)) begin
; CHECK-NEXT: if (enable & ~predicate1 & ~reset) begin
; CHECK-NEXT: if (`ASSERT_VERBOSE_COND_)
; CHECK-NEXT: $error("Assertion failed (verification library): ");
; CHECK-NEXT: if (`STOP_COND_)
@ -35,7 +35,7 @@ circuit Foo:
stop(clock, enable, 1)
; assert with message
; CHECK-NEXT: if (enable & ~(predicate2 | reset)) begin
; CHECK-NEXT: if (enable & ~predicate2 & ~reset) begin
; CHECK-NEXT: if (`ASSERT_VERBOSE_COND_)
; CHECK-NEXT: $error("Assertion failed (verification library): sum =/= 1.U");
; CHECK-NEXT: if (`STOP_COND_)
@ -46,7 +46,7 @@ circuit Foo:
stop(clock, enable, 1)
; assert with when
; CHECK-NEXT: if (other & enable & ~(predicate3 | reset)) begin
; CHECK-NEXT: if (other & enable & ~predicate3 & ~reset) begin
; CHECK-NEXT: if (`ASSERT_VERBOSE_COND_)
; CHECK-NEXT: $error("Assertion failed (verification library): Assert with when");
; CHECK-NEXT: if (`STOP_COND_)
@ -58,7 +58,7 @@ circuit Foo:
stop(clock, enable, 1)
; assert with message with arguments
; CHECK-NEXT: if (enable & ~(predicate4 | reset)) begin
; CHECK-NEXT: if (enable & ~predicate4 & ~reset)
; CHECK-NEXT: if (`ASSERT_VERBOSE_COND_)
; CHECK-NEXT: $error("Assertion failed (verification library): expected sum === 2.U but got %d", sum);
; CHECK-NEXT: if (`STOP_COND_)
@ -119,7 +119,7 @@ circuit Foo:
; if-else-fatal style assert with conditional compilation toggles
; CHECK-NEXT: always @(posedge clock) begin
; CHECK-NEXT: `ifndef SYNTHESIS
; CHECK-NEXT: if (enable & ~(predicate9 | reset)) begin
; CHECK-NEXT: if (enable & ~predicate9 & ~reset) begin
; CHECK-NEXT: if (`ASSERT_VERBOSE_COND_)
; CHECK-NEXT: $error("Assertion failed (verification library): Conditional compilation example with if-else-fatal style assert");
; CHECK-NEXT: if (`STOP_COND_)

View File

@ -33,7 +33,7 @@ circuit Foo:
stop(clock, enable, 1)
; assume with when
; CHECK-NEXT: {{assume__verif_library.*}}: assume property (@(posedge clock) ~(other & enable) | predicate3 | reset)
; CHECK-NEXT: {{assume__verif_library.*}}: assume property (@(posedge clock) ~other | ~enable | predicate3 | reset)
; CHECK-SAME: else $error("Assumption does not hold (verification library): assume with when");
when other :
when not(or(predicate3, asUInt(reset))) :