31#include "mlir/Pass/Pass.h"
32#include "llvm/ADT/MapVector.h"
33#include "llvm/ADT/TypeSwitch.h"
34#include "llvm/Support/raw_ostream.h"
37#define GEN_PASS_DEF_CONVERTHWTOBTOR2
38#include "circt/Conversion/Passes.h.inc"
47struct ConvertHWToBTOR2Pass
48 :
public circt::impl::ConvertHWToBTOR2Base<ConvertHWToBTOR2Pass>,
56 ConvertHWToBTOR2Pass(raw_ostream &os) : os(os) {}
58 void runOnOperation()
override;
74 DenseMap<size_t, size_t> sortToLIDMap;
79 DenseMap<APInt, size_t> constToLIDMap;
84 DenseMap<Operation *, size_t> opLIDMap;
88 DenseMap<size_t, size_t> inputLIDs;
94 SmallVector<Operation *> regOps;
98 llvm::SmallMapVector<Operation *, OperandRange::iterator, 16> worklist;
101 DenseSet<Operation *> handledOps;
104 static constexpr size_t noLID = -1UL;
105 [[maybe_unused]]
static constexpr int64_t noWidth = -1L;
112 size_t getOpLID(Operation *op) {
115 Operation *defOp = op;
116 auto &f = opLIDMap[defOp];
126 size_t setOpLID(Operation *op) {
127 size_t oplid = lid++;
128 opLIDMap[op] = oplid;
135 size_t getOpLID(Value value) {
136 Operation *defOp = value.getDefiningOp();
138 if (
auto it = opLIDMap.find(defOp); it != opLIDMap.end())
143 if (BlockArgument barg = dyn_cast<BlockArgument>(value)) {
145 size_t argIdx = barg.getArgNumber();
148 if (
auto it = inputLIDs.find(argIdx); it != inputLIDs.end())
160 size_t getSortLID(
size_t w) {
161 if (
auto it = sortToLIDMap.find(w); it != sortToLIDMap.end())
169 size_t setSortLID(
size_t w) {
170 size_t sortlid = lid;
172 sortToLIDMap[w] = lid++;
179 size_t getConstLID(int64_t val,
size_t w) {
180 if (
auto it = constToLIDMap.find(APInt(w, val)); it != constToLIDMap.end())
188 size_t setConstLID(int64_t val,
size_t w) {
189 size_t constlid = lid;
191 constToLIDMap[APInt(w, val)] = lid++;
199 void genSort(StringRef type,
size_t width) {
201 if (getSortLID(width) != noLID) {
205 size_t sortlid = setSortLID(width);
210 <<
" " << type <<
" " << width <<
"\n";
214 void genInput(
size_t inlid,
size_t width, StringRef name) {
216 size_t sid = sortToLIDMap.at(width);
221 <<
" " << sid <<
" " << name <<
"\n";
225 void genConst(APInt value,
size_t width, Operation *op) {
228 size_t opLID = getOpLID(op);
231 size_t sid = sortToLIDMap.at(width);
235 <<
" " << sid <<
" " << value <<
"\n";
239 size_t genZero(
size_t width) {
241 size_t zlid = getConstLID(0, width);
246 size_t sid = sortToLIDMap.at(width);
249 size_t constlid = setConstLID(0, width);
252 os << constlid <<
" "
254 <<
" " << sid <<
"\n";
260 void genInit(Operation *
reg, Value initVal, int64_t width) {
262 size_t regLID = getOpLID(
reg);
263 size_t sid = sortToLIDMap.at(width);
264 size_t initValLID = getOpLID(initVal);
270 <<
" " << sid <<
" " << regLID <<
" " << initValLID <<
"\n";
275 void genBinOp(StringRef inst, Operation *binop, Value op1, Value op2,
278 if (binop->getNumOperands() != 2) {
279 binop->emitError(
"variadic operations not are not currently supported");
284 size_t opLID = getOpLID(binop);
287 size_t sid = sortToLIDMap.at(width);
291 size_t op1LID = getOpLID(op1);
292 size_t op2LID = getOpLID(op2);
295 os << opLID <<
" " << inst <<
" " << sid <<
" " << op1LID <<
" " << op2LID
300 void genSlice(Operation *srcop, Value op0,
size_t lowbit, int64_t width) {
302 size_t opLID = getOpLID(srcop);
305 size_t sid = sortToLIDMap.at(width);
309 size_t op0LID = getOpLID(op0);
314 <<
" " << sid <<
" " << op0LID <<
" " << (lowbit + width - 1) <<
" "
319 void genUnaryOp(Operation *srcop, Operation *op0, StringRef inst,
322 size_t opLID = getOpLID(srcop);
325 size_t sid = sortToLIDMap.at(width);
329 size_t op0LID = getOpLID(op0);
331 os << opLID <<
" " << inst <<
" " << sid <<
" " << op0LID <<
"\n";
336 void genUnaryOp(Operation *srcop, Value op0, StringRef inst,
size_t width) {
337 genUnaryOp(srcop, op0.getDefiningOp(), inst, width);
341 size_t genUnaryOp(
size_t op0LID, StringRef inst,
size_t width) {
343 size_t curLid = lid++;
346 size_t sid = sortToLIDMap.at(width);
348 os << curLid <<
" " << inst <<
" " << sid <<
" " << op0LID <<
"\n";
353 size_t genUnaryOp(Operation *op0, StringRef inst,
size_t width) {
354 return genUnaryOp(getOpLID(op0), inst, width);
359 size_t genUnaryOp(Value op0, StringRef inst,
size_t width) {
360 return genUnaryOp(getOpLID(op0), inst, width);
366 void genBad(Operation *assertop) {
368 size_t assertLID = getOpLID(assertop);
375 void genBad(
size_t assertLID) {
380 <<
" " << assertLID <<
"\n";
385 void genConstraint(Value expr) {
387 size_t exprLID = getOpLID(expr);
389 genConstraint(exprLID);
394 void genConstraint(
size_t exprLID) {
399 <<
" " << exprLID <<
"\n";
404 void genIte(Operation *srcop, Value cond, Value t, Value f, int64_t width) {
406 size_t condLID = getOpLID(cond);
407 size_t tLID = getOpLID(t);
408 size_t fLID = getOpLID(f);
410 genIte(srcop, condLID, tLID, fLID, width);
415 void genIte(Operation *srcop,
size_t condLID,
size_t tLID,
size_t fLID,
418 size_t opLID = getOpLID(srcop);
421 size_t sid = sortToLIDMap.at(width);
426 <<
" " << sid <<
" " << condLID <<
" " << tLID <<
" " << fLID <<
"\n";
430 size_t genImplies(Operation *srcop, Value lhs, Value rhs) {
432 size_t lhsLID = getOpLID(lhs);
433 size_t rhsLID = getOpLID(rhs);
435 return genImplies(srcop, lhsLID, rhsLID);
439 size_t genImplies(Operation *srcop,
size_t lhsLID,
size_t rhsLID) {
441 size_t opLID = getOpLID(srcop);
442 return genImplies(opLID, lhsLID, rhsLID);
445 size_t genImplies(
size_t opLID,
size_t lhsLID,
size_t rhsLID) {
447 size_t sid = sortToLIDMap.at(1);
451 <<
" " << sid <<
" " << lhsLID <<
" " << rhsLID <<
"\n";
456 void genState(Operation *srcop, int64_t width, StringRef name) {
458 size_t opLID = getOpLID(srcop);
461 size_t sid = sortToLIDMap.at(width);
466 <<
" " << sid <<
" " << name <<
"\n";
471 void genNext(Value next, Operation *
reg, int64_t width) {
473 size_t sid = sortToLIDMap.at(width);
476 size_t regLID = getOpLID(
reg);
477 size_t nextLID = getOpLID(next);
483 <<
" " << sid <<
" " << regLID <<
" " << nextLID <<
"\n";
488 int64_t requireSort(mlir::Type type) {
490 int64_t width = hw::getBitWidth(type);
499 genSort(
"bitvec", width);
505 void finalizeRegVisit(Operation *op) {
507 Value next, reset, resetVal;
510 if (
auto reg = dyn_cast<seq::CompRegOp>(op)) {
511 width = hw::getBitWidth(
reg.getType());
512 next =
reg.getInput();
513 reset =
reg.getReset();
514 resetVal =
reg.getResetValue();
515 }
else if (
auto reg = dyn_cast<seq::FirRegOp>(op)) {
516 width = hw::getBitWidth(
reg.getType());
517 next =
reg.getNext();
518 reset =
reg.getReset();
519 resetVal =
reg.getResetValue();
521 op->emitError(
"Invalid register operation !");
525 genSort(
"bitvec", width);
530 size_t nextLID = noLID;
534 if (BlockArgument barg = dyn_cast<BlockArgument>(next)) {
536 size_t argIdx = barg.getArgNumber();
539 nextLID = inputLIDs[argIdx];
542 nextLID = getOpLID(next);
547 size_t resetValLID = noLID;
551 size_t resetLID = noLID;
552 if (BlockArgument barg = dyn_cast<BlockArgument>(reset)) {
555 size_t argIdx = barg.getArgNumber();
558 resetLID = inputLIDs[argIdx];
561 resetLID = getOpLID(reset);
566 resetValLID = getOpLID(resetVal.getDefiningOp());
568 resetValLID = genZero(width);
571 setOpLID(next.getDefiningOp());
580 genIte(next.getDefiningOp(), resetLID, resetValLID, nextLID, width);
583 if (nextLID == noLID) {
584 next.getDefiningOp()->emitError(
585 "Register input does not point to a valid op!");
591 genNext(next, op, width);
605 if (port.
isInput() && !isa<seq::ClockType, seq::ImmutableType>(port.
type)) {
607 StringRef iName = port.
getName();
611 int64_t w = requireSort(port.
type);
618 inputLIDs[port.
argNum] = lid;
623 genInput(inlid, w, iName);
632 if (handledOps.contains(op))
636 int64_t w = requireSort(op.getType());
640 genConst(op.getValue(), w, op);
644 void visit(hw::WireOp op) {
645 op->emitError(
"Wires are not supported in btor!");
646 return signalPassFailure();
649 void visitTypeOp(Operation *op) { visitInvalidTypeOp(op); }
652 void visitInvalidTypeOp(Operation *op) {
654 dispatchCombinationalVisitor(op);
659 template <
typename Op>
660 void visitBinOp(Op op, StringRef inst) {
662 int64_t w = requireSort(op.getType());
665 Value op1 = op.getOperand(0);
666 Value op2 = op.getOperand(1);
669 genBinOp(inst, op, op1, op2, w);
673 void visitComb(
comb::AddOp op) { visitBinOp(op,
"add"); }
674 void visitComb(
comb::SubOp op) { visitBinOp(op,
"sub"); }
675 void visitComb(
comb::MulOp op) { visitBinOp(op,
"mul"); }
676 void visitComb(
comb::DivSOp op) { visitBinOp(op,
"sdiv"); }
677 void visitComb(
comb::DivUOp op) { visitBinOp(op,
"udiv"); }
678 void visitComb(
comb::ModSOp op) { visitBinOp(op,
"smod"); }
679 void visitComb(
comb::ShlOp op) { visitBinOp(op,
"sll"); }
680 void visitComb(
comb::ShrUOp op) { visitBinOp(op,
"srl"); }
681 void visitComb(
comb::ShrSOp op) { visitBinOp(op,
"sra"); }
682 void visitComb(
comb::AndOp op) { visitBinOp(op,
"and"); }
683 void visitComb(
comb::OrOp op) { visitBinOp(op,
"or"); }
684 void visitComb(
comb::XorOp op) { visitBinOp(op,
"xor"); }
690 int64_t w = requireSort(op.getType());
694 Value op0 = op.getOperand();
695 size_t lb = op.getLowBit();
698 genSlice(op, op0, lb, w);
704 void visitComb(comb::ICmpOp op) {
705 Value lhs = op.getOperand(0);
706 Value rhs = op.getOperand(1);
710 StringRef pred = stringifyICmpPredicate(op.getPredicate());
715 else if (pred ==
"ule")
717 else if (pred ==
"sle")
719 else if (pred ==
"uge")
721 else if (pred ==
"sge")
725 genSort(
"bitvec", 1);
729 genBinOp(pred, op, lhs, rhs, 1);
735 Value pred = op.getCond();
736 Value tval = op.getTrueValue();
737 Value fval = op.getFalseValue();
741 int64_t w = requireSort(op.getType());
744 genIte(op, pred, tval, fval, w);
747 void visitComb(Operation *op) { visitInvalidComb(op); }
750 void visitInvalidComb(Operation *op) { dispatchSVVisitor(op); }
753 void visitSV(sv::AssertOp op) {
755 Value expr = op.getExpression();
758 genSort(
"bitvec", 1);
764 if (
auto ifop = dyn_cast<sv::IfOp>(((Operation *)op)->getParentOp())) {
765 Value
en = ifop.getOperand();
768 genImplies(ifop,
en, expr);
771 genUnaryOp(op, ifop,
"not", 1);
774 genUnaryOp(op, expr,
"not", 1);
781 void visitSV(sv::AssumeOp op) {
783 Value expr = op.getExpression();
787 void visitSV(Operation *op) { visitInvalidSV(op); }
790 void visitInvalidSV(Operation *op) { dispatchVerifVisitor(op); }
792 template <
typename Op>
793 void visitAssertLike(Op op) {
795 Value prop = op.getProperty();
796 Value
en = op.getEnable();
799 genSort(
"bitvec", 1);
801 size_t assertLID = noLID;
805 genImplies(op,
en, prop);
808 assertLID = genUnaryOp(op,
"not", 1);
811 assertLID = genUnaryOp(prop.getDefiningOp(),
"not", 1);
818 template <
typename Op>
819 void visitAssumeLike(Op op) {
821 Value prop = op.getProperty();
822 Value
en = op.getEnable();
824 size_t assumeLID = getOpLID(prop);
828 genSort(
"bitvec", 1);
830 assumeLID = genImplies(op,
en, prop);
834 genConstraint(assumeLID);
839 void visitVerif(verif::AssertOp op) { visitAssertLike(op); }
840 void visitVerif(verif::ClockedAssertOp op) { visitAssertLike(op); }
844 void visitVerif(verif::AssumeOp op) { visitAssumeLike(op); }
845 void visitVerif(verif::ClockedAssumeOp op) { visitAssumeLike(op); }
847 void visitUnhandledVerif(Operation *op) {
848 op->emitError(
"not supported in btor2!");
849 return signalPassFailure();
852 void visitInvalidVerif(Operation *op) { visit(op); }
856 void visit(Operation *op) {
859 TypeSwitch<Operation *, void>(op)
860 .Case<seq::FirRegOp,
seq::CompRegOp>([&](
auto expr) { visit(expr); })
861 .Default([&](
auto expr) { visitUnsupportedOp(op); });
867 void visit(seq::FirRegOp
reg) {
869 StringRef regName =
reg.getName();
870 int64_t w = requireSort(
reg.getType());
873 genState(
reg, w, regName);
878 regOps.push_back(
reg);
884 StringRef regName =
reg.getName().value();
885 int64_t w = requireSort(
reg.getType());
889 auto init =
reg.getInitialValue();
895 if (!init.getDefiningOp<seq::InitialOp>()) {
897 "Initial value must be emitted directly by a seq.initial op");
903 if (!initialConstant)
904 reg->emitError(
"initial value must be constant");
907 dispatchTypeOpVisitor(initialConstant);
910 handledOps.insert(initialConstant);
913 genState(
reg, w, regName);
916 genInit(
reg, initialConstant, w);
919 genState(
reg, w, regName);
925 regOps.push_back(
reg);
930 void ignore(Operation *op) {}
934 void visitUnsupportedOp(Operation *op) {
937 TypeSwitch<Operation *, void>(op)
939 .Case<sv::MacroDefOp, sv::MacroDeclOp, sv::VerbatimOp,
940 sv::VerbatimExprOp, sv::VerbatimExprSEOp, sv::IfOp,
sv::IfDefOp,
941 sv::IfDefProceduralOp, sv::AlwaysOp, sv::AlwaysCombOp,
942 seq::InitialOp, sv::AlwaysFFOp, seq::FromClockOp, seq::InitialOp,
944 [&](
auto expr) { ignore(op); })
947 .Case<seq::FromClockOp>([&](
auto expr) {
948 if (++nclocks > 1UL) {
949 op->emitOpError(
"Mutli-clock designs are not supported!");
950 return signalPassFailure();
956 .Default([&](
auto expr) {
957 op->emitOpError(
"is an unsupported operation");
958 return signalPassFailure();
964void ConvertHWToBTOR2Pass::runOnOperation() {
975 module.walk([&](Operation *op) {
976 TypeSwitch<Operation *, void>(op)
977 .Case<seq::FirRegOp, seq::CompRegOp>([&](auto reg) {
979 handledOps.insert(op);
981 .Default([&](
auto expr) {});
985 module.walk([&](Operation *op) {
987 if (isa<hw::InstanceOp>(op)) {
988 op->emitOpError("not supported in BTOR2 conversion");
993 if (handledOps.contains(op))
997 worklist.insert({op, op->operand_begin()});
1000 while (!worklist.empty()) {
1001 auto &[op, operandIt] = worklist.back();
1002 if (operandIt == op->operand_end()) {
1004 dispatchTypeOpVisitor(op);
1007 handledOps.insert(op);
1008 worklist.pop_back();
1014 Value operand = *(operandIt++);
1015 auto *defOp = operand.getDefiningOp();
1018 if (!defOp || handledOps.contains(defOp))
1023 if (!worklist.insert({defOp, defOp->operand_begin()}).second) {
1024 defOp->emitError(
"dependency cycle");
1031 for (
size_t i = 0; i < regOps.size(); ++i) {
1032 finalizeRegVisit(regOps[i]);
1036 sortToLIDMap.clear();
1037 constToLIDMap.clear();
1046std::unique_ptr<mlir::Pass>
1048 return std::make_unique<ConvertHWToBTOR2Pass>(os);
1053 return std::make_unique<ConvertHWToBTOR2Pass>(llvm::outs());
assert(baseType &&"element must be base type")
static SmallVector< PortInfo > getPortList(ModuleTy &mod)
This helps visit Combinational nodes.
This helps visit TypeOp nodes.
Value unwrapImmutableValue(mlir::TypedValue< seq::ImmutableType > immutableVal)
The InstanceGraph op interface, see InstanceGraphInterface.td for more details.
std::unique_ptr< mlir::Pass > createConvertHWToBTOR2Pass()
reg(value, clock, reset=None, reset_value=None, name=None, sym_name=None)
This holds the name, type, direction of a module's ports.
StringRef getName() const
size_t argNum
This is the argument index or the result index depending on the direction.