16#include "mlir/Analysis/TopologicalSortUtils.h"
17#include "mlir/IR/BuiltinAttributes.h"
18#include "mlir/IR/Matchers.h"
19#include "mlir/IR/OpDefinition.h"
20#include "mlir/IR/PatternMatch.h"
21#include "mlir/IR/Value.h"
22#include "llvm/ADT/APInt.h"
23#include "llvm/ADT/SmallVector.h"
24#include "llvm/Support/Casting.h"
25#include "llvm/Support/LogicalResult.h"
30using namespace circt::synth::aig;
32using namespace matchers;
35#include "circt/Dialect/Synth/Synth.cpp.inc"
39inline llvm::KnownBits applyInversion(llvm::KnownBits value,
bool inverted) {
41 std::swap(value.Zero, value.One);
45template <
typename SubType>
46struct ComplementMatcher {
48 ComplementMatcher(SubType lhs) : lhs(std::move(lhs)) {}
49 bool match(Operation *op) {
50 auto boolOp = dyn_cast<BooleanLogicOpInterface>(op);
51 return boolOp && boolOp.getInputs().size() == 1 && boolOp.isInverted(0) &&
52 lhs.match(op->getOperand(0));
56template <
typename SubType>
57static inline ComplementMatcher<SubType>
m_Complement(
const SubType &subExpr) {
58 return ComplementMatcher<SubType>(subExpr);
63LogicalResult ChoiceOp::verify() {
64 if (getNumOperands() < 1)
65 return emitOpError(
"requires at least one operand");
69OpFoldResult ChoiceOp::fold(FoldAdaptor adaptor) {
70 if (adaptor.getInputs().size() == 1)
84LogicalResult ChoiceOp::canonicalize(ChoiceOp op, PatternRewriter &rewriter) {
85 llvm::SetVector<Value> worklist;
88 auto addToWorklist = [&](ChoiceOp choice) ->
bool {
89 if (choice->getBlock() == op->getBlock() && visitedChoices.insert(choice)) {
90 worklist.insert(choice.getInputs().begin(), choice.getInputs().end());
98 bool mergedOtherChoices =
false;
101 for (
unsigned i = 0; i < worklist.size(); ++i) {
102 Value val = worklist[i];
103 if (
auto defOp = val.getDefiningOp<synth::ChoiceOp>()) {
105 if (addToWorklist(defOp))
106 mergedOtherChoices =
true;
109 for (Operation *user : val.getUsers()) {
110 if (
auto userChoice = llvm::dyn_cast<synth::ChoiceOp>(user)) {
111 if (addToWorklist(userChoice)) {
112 mergedOtherChoices =
true;
118 llvm::SmallVector<mlir::Value> finalOperands;
119 for (Value v : worklist) {
120 if (!visitedChoices.contains(v.getDefiningOp())) {
121 finalOperands.push_back(v);
125 if (!mergedOtherChoices && finalOperands.size() == op.getInputs().size())
126 return llvm::failure();
128 auto newChoice = synth::ChoiceOp::create(rewriter, op->getLoc(), op.getType(),
130 for (Operation *visited : visitedChoices.takeVector())
131 rewriter.replaceOp(visited, newChoice);
133 for (
auto value : newChoice.getInputs())
134 rewriter.replaceAllUsesExcept(value, newChoice.getResult(), newChoice);
143bool AndInverterOp::areInputsPermutationInvariant() {
return true; }
145OpFoldResult AndInverterOp::fold(FoldAdaptor adaptor) {
146 if (getNumOperands() == 1 && !isInverted(0))
147 return getOperand(0);
149 auto inputs = adaptor.getInputs();
150 if (inputs.size() == 2)
151 if (
auto intAttr = dyn_cast_or_null<IntegerAttr>(inputs[1])) {
152 auto value = intAttr.getValue();
156 return IntegerAttr::get(
157 IntegerType::get(getContext(), value.getBitWidth()), value);
158 if (value.isAllOnes()) {
162 return getOperand(0);
168LogicalResult AndInverterOp::canonicalize(AndInverterOp op,
169 PatternRewriter &rewriter) {
171 SmallVector<Value> uniqueValues;
172 SmallVector<bool> uniqueInverts;
175 APInt::getAllOnes(op.getResult().getType().getIntOrFloatBitWidth());
177 bool invertedConstFound =
false;
178 bool flippedFound =
false;
180 for (
auto [value, inverted] :
llvm::zip(op.getInputs(), op.getInverted())) {
181 bool newInverted = inverted;
184 constValue &= ~constOp.getValue();
185 invertedConstFound =
true;
187 constValue &= constOp.getValue();
192 if (
auto andInverterOp = value.getDefiningOp<synth::aig::AndInverterOp>()) {
193 if (andInverterOp.getInputs().size() == 1 &&
194 andInverterOp.isInverted(0)) {
195 value = andInverterOp.getOperand(0);
196 newInverted = andInverterOp.isInverted(0) ^ inverted;
201 auto it = seen.find(value);
202 if (it == seen.end()) {
203 seen.insert({value, newInverted});
204 uniqueValues.push_back(value);
205 uniqueInverts.push_back(newInverted);
206 }
else if (it->second != newInverted) {
209 op, APInt::getZero(value.getType().getIntOrFloatBitWidth()));
215 if (constValue.isZero()) {
221 if ((uniqueValues.size() == op.getInputs().size() && !flippedFound) ||
222 (!constValue.isAllOnes() && !invertedConstFound &&
223 uniqueValues.size() + 1 == op.getInputs().size()))
226 if (!constValue.isAllOnes()) {
228 uniqueInverts.push_back(
false);
229 uniqueValues.push_back(constOp);
233 if (uniqueValues.empty()) {
239 replaceOpWithNewOpAndCopyNamehint<synth::aig::AndInverterOp>(
240 rewriter, op, uniqueValues, uniqueInverts);
244APInt AndInverterOp::evaluateBooleanLogicWithoutInversion(
245 llvm::ArrayRef<APInt> inputs) {
246 assert(!inputs.empty() &&
"expected non-empty input list");
247 APInt result = APInt::getAllOnes(inputs.front().getBitWidth());
248 for (
const APInt &input : inputs)
253bool AndInverterOp::supportsNumInputs(
unsigned numInputs) {
254 return numInputs >= 1;
257llvm::KnownBits AndInverterOp::computeKnownBits(
258 llvm::function_ref<
const llvm::KnownBits &(
unsigned)> getInputKnownBits) {
259 assert(getNumOperands() > 0 &&
"Expected non-empty input list");
261 auto width = getInputKnownBits(0).getBitWidth();
262 llvm::KnownBits result(width);
263 result.One = APInt::getAllOnes(width);
264 result.Zero = APInt::getZero(width);
266 for (
auto [i, inverted] :
llvm::enumerate(getInverted()))
267 result &= applyInversion(getInputKnownBits(i), inverted);
272int64_t AndInverterOp::getLogicDepthCost() {
273 return llvm::Log2_64_Ceil(getNumOperands());
276std::optional<uint64_t> AndInverterOp::getLogicAreaCost() {
277 int64_t bitWidth = hw::getBitWidth(getType());
280 return static_cast<uint64_t
>(getNumOperands() - 1) * bitWidth;
283void AndInverterOp::emitCNFWithoutInversion(
284 int outVar, llvm::ArrayRef<int> inputVars,
285 llvm::function_ref<
void(llvm::ArrayRef<int>)> addClause,
286 llvm::function_ref<
int()> newVar) {
295bool XorInverterOp::areInputsPermutationInvariant() {
return true; }
297OpFoldResult XorInverterOp::fold(FoldAdaptor adaptor) {
299 if (getNumOperands() == 1 && !isInverted(0))
300 return getOperand(0);
302 auto inputs = adaptor.getInputs();
303 if (inputs.size() == 2)
304 if (
auto intAttr = dyn_cast_or_null<IntegerAttr>(inputs[1])) {
305 auto value = intAttr.getValue();
310 return getOperand(0);
315LogicalResult XorInverterOp::canonicalize(XorInverterOp op,
316 PatternRewriter &rewriter) {
323 APInt::getZero(op.getResult().getType().getIntOrFloatBitWidth());
325 bool constFound =
false;
326 bool changed =
false;
328 for (
auto [value, inverted] :
llvm::zip(op.getInputs(), op.getInverted())) {
329 Value currentValue = value;
330 bool newInverted = inverted;
334 if (
auto constOp = currentValue.getDefiningOp<
hw::ConstantOp>()) {
335 APInt val = constOp.getValue();
346 matchPattern(currentValue,
m_Complement(m_Any(&matchedVal)))) {
347 currentValue = matchedVal;
354 if (activeOperands.count(currentValue)) {
357 if (activeOperands[currentValue] != newInverted)
358 constValue.flipAllBits();
359 activeOperands.erase(currentValue);
362 activeOperands[currentValue] = newInverted;
368 if (!changed && !constFound && activeOperands.size() == op.getInputs().size())
373 if (!constValue.isZero()) {
374 if (constValue.isAllOnes() && !activeOperands.empty()) {
376 activeOperands.back().second = !activeOperands.back().second;
378 if (op.getInputs().size() == 2 && !op.getInverted()[1] &&
379 activeOperands.size() == 1)
382 activeOperands.insert({constOp,
false});
386 if (activeOperands.empty()) {
388 op, APInt::getZero(op.getResult().getType().getIntOrFloatBitWidth()));
393 XorInverterOp::create(rewriter, op.getLoc(),
394 activeOperands.getArrayRef()));
398APInt XorInverterOp::evaluateBooleanLogicWithoutInversion(
399 llvm::ArrayRef<APInt> inputs) {
400 assert(!inputs.empty() &&
"expected non-empty input list");
401 APInt result = APInt::getZero(inputs.front().getBitWidth());
402 for (
const APInt &input : inputs)
407bool XorInverterOp::supportsNumInputs(
unsigned numInputs) {
408 return numInputs >= 1;
411llvm::KnownBits XorInverterOp::computeKnownBits(
412 llvm::function_ref<
const llvm::KnownBits &(
unsigned)> getInputKnownBits) {
413 assert(getNumOperands() > 0 &&
"Expected non-empty input list");
415 llvm::KnownBits result(getInputKnownBits(0).
getBitWidth());
416 for (
auto [i, inverted] :
llvm::enumerate(getInverted()))
417 result ^= applyInversion(getInputKnownBits(i), inverted);
421int64_t XorInverterOp::getLogicDepthCost() {
422 return llvm::Log2_64_Ceil(getNumOperands());
425std::optional<uint64_t> XorInverterOp::getLogicAreaCost() {
426 int64_t bitWidth = hw::getBitWidth(getType());
429 return static_cast<uint64_t
>(getNumOperands() - 1) * bitWidth;
432void XorInverterOp::emitCNFWithoutInversion(
433 int outVar, llvm::ArrayRef<int> inputVars,
434 llvm::function_ref<
void(llvm::ArrayRef<int>)> addClause,
435 llvm::function_ref<
int()> newVar) {
443void DotOp::emitCNFWithoutInversion(
444 int outVar, llvm::ArrayRef<int> inputVars,
445 llvm::function_ref<
void(llvm::ArrayRef<int>)> addClause,
446 llvm::function_ref<
int()> newVar) {
447 assert(inputVars.size() == 3 &&
"expected one SAT variable per operand");
448 int andVar = newVar();
449 int orVar = newVar();
462void MajorityOp::emitCNFWithoutInversion(
463 int outVar, llvm::ArrayRef<int> inputVars,
464 llvm::function_ref<
void(llvm::ArrayRef<int>)> addClause,
465 llvm::function_ref<
int()> newVar) {
466 assert(inputVars.size() == 3 &&
"expected exactly three inputs");
481 Location loc, ValueRange operands, ArrayRef<bool> inverts,
482 PatternRewriter &rewriter,
483 llvm::function_ref<Value(Value,
bool)> createUnary,
484 llvm::function_ref<Value(Value, Value,
bool,
bool)> createBinary) {
485 switch (operands.size()) {
487 assert(0 &&
"cannot be called with empty operand range");
490 return inverts[0] ? createUnary(operands[0],
true) : operands[0];
492 return createBinary(operands[0], operands[1], inverts[0], inverts[1]);
494 auto firstHalf = operands.size() / 2;
496 inverts.take_front(firstHalf),
497 rewriter, createUnary, createBinary);
499 inverts.drop_front(firstHalf),
500 rewriter, createUnary, createBinary);
501 return createBinary(lhs, rhs,
false,
false);
506template <
typename OpTy>
508 PatternRewriter &rewriter) {
509 if (op.getInputs().size() <= 2)
512 op.getLoc(), op.getOperands(), op.getInverted(), rewriter,
513 [&](Value input,
bool invert) {
514 return OpTy::create(rewriter, op.getLoc(), input, invert);
516 [&](Value lhs, Value rhs,
bool invertLhs,
bool invertRhs) {
517 return OpTy::create(rewriter, op.getLoc(), lhs, rhs, invertLhs,
526 patterns.add(lowerVariadicAndInverterOpConversion<aig::AndInverterOp>);
531 patterns.add(lowerVariadicAndInverterOpConversion<XorInverterOp>);
535 return isa<synth::BooleanLogicOpInterface, synth::ChoiceOp,
comb::ExtractOp,
541 llvm::function_ref<
bool(mlir::Value, mlir::Operation *)> isOperandReady) {
543 auto walkResult = op->walk([&](Region *region) {
545 dyn_cast<mlir::RegionKindInterface>(region->getParentOp());
547 regionKindOp.hasSSADominance(region->getRegionNumber()))
548 return WalkResult::advance();
551 for (
auto &block : *region) {
552 if (!mlir::sortTopologically(&block, isOperandReady))
553 return WalkResult::interrupt();
555 return WalkResult::advance();
558 return success(!walkResult.wasInterrupted());
565void OneHotOp::emitCNFWithoutInversion(
566 int outVar, llvm::ArrayRef<int> inputVars,
567 llvm::function_ref<
void(llvm::ArrayRef<int>)> addClause,
568 llvm::function_ref<
int()> newVar) {
569 assert(inputVars.size() == 3 &&
"expected exactly three inputs");
572 int parity = newVar();
576 int allSet = newVar();
587void MuxInverterOp::emitCNFWithoutInversion(
588 int outVar, llvm::ArrayRef<int> inputVars,
589 llvm::function_ref<
void(llvm::ArrayRef<int>)> addClause,
590 llvm::function_ref<
int()> newVar) {
591 assert(inputVars.size() == 3 &&
"expected exactly three inputs");
593 int cond = inputVars[0];
594 int trueValue = inputVars[1];
595 int falseValue = inputVars[2];
612void GambleOp::emitCNFWithoutInversion(
613 int outVar, llvm::ArrayRef<int> inputVars,
614 llvm::function_ref<
void(llvm::ArrayRef<int>)> addClause,
615 llvm::function_ref<
int()> newVar) {
616 assert(inputVars.size() == 3 &&
"expected exactly three inputs");
619 int allSet = newVar();
623 int orSet = newVar();
assert(baseType &&"element must be base type")
static ComplementMatcher< SubType > m_Complement(const SubType &subExpr)
LogicalResult lowerVariadicAndInverterOpConversion(OpTy op, PatternRewriter &rewriter)
static Value lowerVariadicInvertibleOp(Location loc, ValueRange operands, ArrayRef< bool > inverts, PatternRewriter &rewriter, llvm::function_ref< Value(Value, bool)> createUnary, llvm::function_ref< Value(Value, Value, bool, bool)> createBinary)
int64_t getBitWidth(mlir::Type type)
Return the hardware bit width of a type.
void populateVariadicXorInverterLoweringPatterns(mlir::RewritePatternSet &patterns)
LogicalResult topologicallySortGraphRegionBlocks(mlir::Operation *op, llvm::function_ref< bool(mlir::Value, mlir::Operation *)> isOperandReady)
This function performs a topological sort on the operations within each block of graph regions in the...
bool isLogicNetworkOp(mlir::Operation *op)
void populateVariadicAndInverterLoweringPatterns(mlir::RewritePatternSet &patterns)
The InstanceGraph op interface, see InstanceGraphInterface.td for more details.
void addAndClauses(int outVar, llvm::ArrayRef< int > inputLits, llvm::function_ref< void(llvm::ArrayRef< int >)> addClause)
Emit clauses encoding outVar <=> and(inputLits).
void addXorClauses(int outVar, int lhsLit, int rhsLit, llvm::function_ref< void(llvm::ArrayRef< int >)> addClause)
Emit clauses encoding outVar <=> (lhsLit xor rhsLit).
void replaceOpAndCopyNamehint(PatternRewriter &rewriter, Operation *op, Value newValue)
A wrapper of PatternRewriter::replaceOp to propagate "sv.namehint" attribute.
void addOrClauses(int outVar, llvm::ArrayRef< int > inputLits, llvm::function_ref< void(llvm::ArrayRef< int >)> addClause)
Emit clauses encoding outVar <=> or(inputLits).
void addParityClauses(int outVar, llvm::ArrayRef< int > inputLits, llvm::function_ref< void(llvm::ArrayRef< int >)> addClause, llvm::function_ref< int()> newVar)
Emit clauses encoding outVar <=> parity(inputLits).