13 #include "../PassDetail.h"
30 #include "llvm/ADT/MapVector.h"
31 #include "llvm/ADT/TypeSwitch.h"
32 #include "llvm/Support/raw_ostream.h"
34 using namespace circt;
40 struct ConvertHWToBTOR2Pass
41 :
public ConvertHWToBTOR2Base<ConvertHWToBTOR2Pass>,
42 public comb::CombinationalVisitor<ConvertHWToBTOR2Pass>,
43 public sv::Visitor<ConvertHWToBTOR2Pass>,
44 public hw::TypeOpVisitor<ConvertHWToBTOR2Pass> {
46 ConvertHWToBTOR2Pass(raw_ostream &os) : os(os) {}
48 void runOnOperation()
override;
64 DenseMap<size_t, size_t> sortToLIDMap;
69 DenseMap<APInt, size_t> constToLIDMap;
74 DenseMap<Operation *, size_t> opLIDMap;
80 DenseMap<Operation *, Operation *> opAliasMap;
84 DenseMap<size_t, size_t> inputLIDs;
90 SmallVector<Operation *> regOps;
94 llvm::SmallMapVector<Operation *, OperandRange::iterator, 16> worklist;
97 DenseSet<Operation *> handledOps;
100 static constexpr
size_t noLID = -1UL;
101 static constexpr int64_t noWidth = -1L;
108 size_t getOpLID(Operation *op) {
111 Operation *defOp = getOpAlias(op);
112 auto &f = opLIDMap[defOp];
122 size_t setOpLID(Operation *op) {
123 size_t oplid = lid++;
124 opLIDMap[op] = oplid;
131 size_t getOpLID(Value value) {
133 Operation *defOp = getOpAlias(value.getDefiningOp());
135 if (
auto it = opLIDMap.find(defOp); it != opLIDMap.end())
140 if (BlockArgument barg = dyn_cast<BlockArgument>(value)) {
142 size_t argIdx = barg.getArgNumber();
145 if (
auto it = inputLIDs.find(argIdx); it != inputLIDs.end())
157 Operation *getOpAlias(Operation *op) {
160 if (
auto it = opAliasMap.find(op); it != opAliasMap.end()) {
163 op->emitError(
"BTOR2 emission does not support for wires of inputs!");
175 void setOpAlias(Operation *alias, Operation *op) {
176 opAliasMap[alias] = getOpAlias(op);
182 size_t getSortLID(
size_t w) {
183 if (
auto it = sortToLIDMap.find(w); it != sortToLIDMap.end())
191 size_t setSortLID(
size_t w) {
192 size_t sortlid = lid;
194 sortToLIDMap[w] = lid++;
201 size_t getConstLID(int64_t val,
size_t w) {
202 if (
auto it = constToLIDMap.find(APInt(w, val)); it != constToLIDMap.end())
210 size_t setConstLID(int64_t val,
size_t w) {
211 size_t constlid = lid;
213 constToLIDMap[APInt(w, val)] = lid++;
221 void genSort(StringRef type,
size_t width) {
223 if (getSortLID(
width) != noLID) {
227 size_t sortlid = setSortLID(
width);
232 <<
" " << type <<
" " <<
width <<
"\n";
236 void genInput(
size_t inlid,
size_t width, StringRef name) {
238 size_t sid = sortToLIDMap.at(
width);
243 <<
" " << sid <<
" " << name <<
"\n";
247 void genConst(int64_t value,
size_t width, Operation *op) {
250 size_t opLID = getOpLID(op);
253 size_t sid = sortToLIDMap.at(
width);
257 <<
" " << sid <<
" " << value <<
"\n";
261 size_t genZero(
size_t width) {
263 size_t zlid = getConstLID(0,
width);
268 size_t sid = sortToLIDMap.at(
width);
271 size_t constlid = setConstLID(0,
width);
274 os << constlid <<
" "
276 <<
" " << sid <<
"\n";
282 void genInit(Operation *
reg, Value initVal, int64_t
width) {
284 size_t regLID = getOpLID(
reg);
285 size_t sid = sortToLIDMap.at(
width);
286 size_t initValLID = getOpLID(initVal);
292 <<
" " << sid <<
" " << regLID <<
" " << initValLID <<
"\n";
297 void genBinOp(StringRef inst, Operation *binop, Value op1, Value op2,
300 size_t opLID = getOpLID(binop);
303 size_t sid = sortToLIDMap.at(
width);
307 size_t op1LID = getOpLID(op1);
308 size_t op2LID = getOpLID(op2);
311 os << opLID <<
" " << inst <<
" " << sid <<
" " << op1LID <<
" " << op2LID
316 void genSlice(Operation *srcop, Value op0,
size_t lowbit, int64_t
width) {
318 size_t opLID = getOpLID(srcop);
321 size_t sid = sortToLIDMap.at(
width);
325 size_t op0LID = getOpLID(op0);
330 <<
" " << sid <<
" " << op0LID <<
" " << (
width - 1) <<
" " << lowbit
335 void genUnaryOp(Operation *srcop, Operation *op0, StringRef inst,
338 size_t opLID = getOpLID(srcop);
341 size_t sid = sortToLIDMap.at(
width);
345 size_t op0LID = getOpLID(op0);
347 os << opLID <<
" " << inst <<
" " << sid <<
" " << op0LID <<
"\n";
351 void genUnaryOp(Operation *srcop, Value op0, StringRef inst,
size_t width) {
352 genUnaryOp(srcop, op0.getDefiningOp(), inst,
width);
358 void genBad(Operation *assertop) {
360 size_t assertLID = getOpLID(assertop);
366 <<
" " << assertLID <<
"\n";
371 void genConstraint(Value expr) {
373 size_t exprLID = getOpLID(expr);
375 genConstraint(exprLID);
380 void genConstraint(
size_t exprLID) {
385 <<
" " << exprLID <<
"\n";
390 void genIte(Operation *srcop, Value cond, Value t, Value f, int64_t
width) {
392 size_t condLID = getOpLID(cond);
393 size_t tLID = getOpLID(t);
394 size_t fLID = getOpLID(f);
396 genIte(srcop, condLID, tLID, fLID,
width);
401 void genIte(Operation *srcop,
size_t condLID,
size_t tLID,
size_t fLID,
404 size_t opLID = getOpLID(srcop);
407 size_t sid = sortToLIDMap.at(
width);
412 <<
" " << sid <<
" " << condLID <<
" " << tLID <<
" " << fLID <<
"\n";
416 void genImplies(Operation *srcop, Value lhs, Value rhs) {
418 size_t lhsLID = getOpLID(lhs);
419 size_t rhsLID = getOpLID(rhs);
421 genImplies(srcop, lhsLID, rhsLID);
425 void genImplies(Operation *srcop,
size_t lhsLID,
size_t rhsLID) {
427 size_t opLID = getOpLID(srcop);
430 size_t sid = sortToLIDMap.at(1);
435 <<
" " << sid <<
" " << lhsLID <<
" " << rhsLID <<
"\n";
439 void genState(Operation *srcop, int64_t
width, StringRef name) {
441 size_t opLID = getOpLID(srcop);
444 size_t sid = sortToLIDMap.at(
width);
449 <<
" " << sid <<
" " << name <<
"\n";
454 void genNext(Value next, Operation *
reg, int64_t
width) {
456 size_t sid = sortToLIDMap.at(
width);
459 size_t regLID = getOpLID(
reg);
460 size_t nextLID = getOpLID(next);
466 <<
" " << sid <<
" " << regLID <<
" " << nextLID <<
"\n";
471 int64_t requireSort(mlir::Type type) {
482 genSort(
"bitvec",
width);
488 void finalizeRegVisit(Operation *op) {
490 Value next, reset, resetVal;
493 if (
auto reg = dyn_cast<seq::CompRegOp>(op)) {
495 next =
reg.getInput();
496 reset =
reg.getReset();
497 resetVal =
reg.getResetValue();
498 }
else if (
auto reg = dyn_cast<seq::FirRegOp>(op)) {
500 next =
reg.getNext();
501 reset =
reg.getReset();
502 resetVal =
reg.getResetValue();
504 op->emitError(
"Invalid register operation !");
508 genSort(
"bitvec",
width);
513 size_t nextLID = noLID;
517 if (BlockArgument barg = dyn_cast<BlockArgument>(next)) {
519 size_t argIdx = barg.getArgNumber();
522 nextLID = inputLIDs[argIdx];
525 nextLID = getOpLID(next);
530 size_t resetValLID = noLID;
534 size_t resetLID = noLID;
535 if (BlockArgument barg = dyn_cast<BlockArgument>(reset)) {
537 size_t argIdx = barg.getArgNumber();
540 resetLID = inputLIDs[argIdx];
543 resetLID = getOpLID(reset);
548 resetValLID = getOpLID(resetVal.getDefiningOp());
550 resetValLID = genZero(
width);
553 setOpLID(next.getDefiningOp());
562 genIte(next.getDefiningOp(), resetLID, resetValLID, nextLID,
width);
565 setOpLID(next.getDefiningOp());
570 genNext(next, op,
width);
580 void visit(hw::PortInfo &port) {
584 if (port.isInput() && !port.type.isa<seq::ClockType>()) {
586 StringRef iName = port.getName();
590 int64_t w = requireSort(port.type);
597 inputLIDs[port.argNum] = lid;
602 genInput(inlid, w, iName);
611 int64_t w = requireSort(op.getType());
615 int64_t value = op.getValue().getSExtValue();
616 genConst(value, w, op);
621 void visit(hw::WireOp op) {
623 Operation *defOp = op.getOperand().getDefiningOp();
625 setOpAlias(op, defOp);
628 void visitTypeOp(Operation *op) { visitInvalidTypeOp(op); }
631 void visitInvalidTypeOp(Operation *op) {
633 dispatchCombinationalVisitor(op);
638 void visitBinOp(Operation *op, StringRef inst, int64_t w) {
641 Value op1 = op->getOperand(0);
642 Value op2 = op->getOperand(1);
645 genBinOp(inst, op, op1, op2, w);
650 visitBinOp(op,
"add", requireSort(op.getType()));
653 visitBinOp(op,
"sub", requireSort(op.getType()));
656 visitBinOp(op,
"mul", requireSort(op.getType()));
659 visitBinOp(op,
"sdiv", requireSort(op.getType()));
662 visitBinOp(op,
"udiv", requireSort(op.getType()));
665 visitBinOp(op,
"smod", requireSort(op.getType()));
668 visitBinOp(op,
"sll", requireSort(op.getType()));
671 visitBinOp(op,
"srl", requireSort(op.getType()));
674 visitBinOp(op,
"sra", requireSort(op.getType()));
677 visitBinOp(op,
"and", requireSort(op.getType()));
680 visitBinOp(op,
"or", requireSort(op.getType()));
683 visitBinOp(op,
"xor", requireSort(op.getType()));
686 visitBinOp(op,
"concat", requireSort(op.getType()));
691 int64_t w = requireSort(op.getType());
695 Value op0 = op.getOperand();
696 size_t lb = op.getLowBit();
699 genSlice(op, op0, lb, w);
705 void visitComb(comb::ICmpOp op) {
706 Value lhs = op.getOperand(0);
707 Value rhs = op.getOperand(1);
711 StringRef pred = stringifyICmpPredicate(op.getPredicate());
718 genSort(
"bitvec", 1);
722 genBinOp(pred, op, lhs, rhs, 1);
728 Value pred = op.getCond();
729 Value tval = op.getTrueValue();
730 Value fval = op.getFalseValue();
734 int64_t w = requireSort(op.getType());
737 genIte(op, pred, tval, fval, w);
740 void visitComb(Operation *op) { visitInvalidComb(op); }
743 void visitInvalidComb(Operation *op) { dispatchSVVisitor(op); }
746 void visitSV(sv::AssertOp op) {
748 Value expr = op.getExpression();
751 genSort(
"bitvec", 1);
757 if (
auto ifop = dyn_cast<sv::IfOp>(((Operation *)op)->getParentOp())) {
758 Value
en = ifop.getOperand();
761 genImplies(ifop, en, expr);
764 genUnaryOp(op, ifop,
"not", 1);
767 genUnaryOp(op, expr,
"not", 1);
774 void visitSV(sv::AssumeOp op) {
776 Value expr = op.getExpression();
780 void visitSV(Operation *op) { visitInvalidSV(op); }
783 void visitInvalidSV(Operation *op) { visit(op); }
787 void visit(Operation *op) {
790 TypeSwitch<Operation *, void>(op)
791 .Case<seq::FirRegOp, hw::WireOp>([&](
auto expr) { visit(expr); })
792 .Default([&](
auto expr) { visitUnsupportedOp(op); });
798 void visit(seq::FirRegOp
reg) {
800 StringRef regName =
reg.getName();
801 int64_t w = requireSort(
reg.getType());
804 genState(
reg, w, regName);
809 regOps.push_back(
reg);
815 StringRef regName =
reg.getName().value();
816 int64_t w = requireSort(
reg.getType());
819 Value pov =
reg.getPowerOnValue();
822 if (!isa_and_nonnull<hw::ConstantOp>(pov.getDefiningOp()))
823 reg->emitError(
"PowerOn Value must be constant!!");
826 dispatchTypeOpVisitor(pov.getDefiningOp());
829 handledOps.insert(pov.getDefiningOp());
832 genState(
reg, w, regName);
835 genInit(
reg, pov, w);
839 genState(
reg, w, regName);
845 regOps.push_back(
reg);
850 void ignore(Operation *op) {}
854 void visitUnsupportedOp(Operation *op) {
857 TypeSwitch<Operation *, void>(op)
859 .Case<sv::MacroDefOp, sv::MacroDeclOp, sv::VerbatimOp,
860 sv::VerbatimExprOp, sv::VerbatimExprSEOp, sv::IfOp,
sv::IfDefOp,
861 sv::IfDefProceduralOp, sv::AlwaysOp, sv::AlwaysCombOp,
863 [&](
auto expr) { ignore(op); })
866 .Case<seq::FromClockOp>([&](
auto expr) {
867 if (++nclocks > 1UL) {
868 op->emitOpError(
"Mutli-clock designs are not supported!");
869 return signalPassFailure();
875 .Default([&](
auto expr) {
876 op->emitOpError(
"is an unsupported operation");
877 return signalPassFailure();
883 void ConvertHWToBTOR2Pass::runOnOperation() {
889 for (
auto &port : module.getPortList()) {
894 module.walk([&](Operation *op) {
895 TypeSwitch<Operation *, void>(op)
896 .Case<seq::FirRegOp, seq::CompRegOp>([&](auto reg) {
898 handledOps.insert(op);
900 .Default([&](
auto expr) {});
904 module.walk([&](Operation *op) {
906 if (isa<hw::InstanceOp>(op)) {
907 op->emitOpError(
"not supported in BTOR2 conversion");
912 if (handledOps.contains(op))
916 worklist.insert({op, op->operand_begin()});
919 while (!worklist.empty()) {
920 auto &[op, operandIt] = worklist.back();
921 if (operandIt == op->operand_end()) {
923 dispatchTypeOpVisitor(op);
926 handledOps.insert(op);
933 Value operand = *(operandIt++);
934 auto *defOp = operand.getDefiningOp();
937 if (!defOp || handledOps.contains(defOp))
942 if (!worklist.insert({defOp, defOp->operand_begin()}).second) {
943 op->emitError(
"dependency cycle");
950 for (
size_t i = 0; i < regOps.size(); ++i) {
951 finalizeRegVisit(regOps[i]);
955 sortToLIDMap.clear();
956 constToLIDMap.clear();
966 std::unique_ptr<mlir::Pass>
968 return std::make_unique<ConvertHWToBTOR2Pass>(os);
973 return std::make_unique<ConvertHWToBTOR2Pass>(llvm::outs());
assert(baseType &&"element must be base type")
int64_t getBitWidth(mlir::Type type)
Return the hardware bit width of a type.
The InstanceGraph op interface, see InstanceGraphInterface.td for more details.
std::unique_ptr< mlir::Pass > createConvertHWToBTOR2Pass(llvm::raw_ostream &os)
def reg(value, clock, reset=None, reset_value=None, name=None, sym_name=None)