From 53ca2ff2ac99d23df2af63805545de123062ac95 Mon Sep 17 00:00:00 2001 From: Bas Niekel Date: Mon, 13 Apr 2026 20:50:24 +0200 Subject: [PATCH 01/29] algorithm for finding IOGs --- .../experimental/Support/FormalProperty.h | 18 ++ .../HandshakeAnnotateProperties.cpp | 300 ++++++++++++++++++ 2 files changed, 318 insertions(+) diff --git a/experimental/include/experimental/Support/FormalProperty.h b/experimental/include/experimental/Support/FormalProperty.h index 13ad88f330..9ea918d132 100644 --- a/experimental/include/experimental/Support/FormalProperty.h +++ b/experimental/include/experimental/Support/FormalProperty.h @@ -33,6 +33,7 @@ class FormalProperty { EFNAO /* Eager Fork Not All Output sent */, CSOAFAF, /* Copied Slots Of Active Forks Are Full */ RPF, /* Reconvergent Path Flow */ + IOGSingleToken, }; TAG getTag() const { return tag; } @@ -268,6 +269,23 @@ class ReconvergentPathFlow : public FormalProperty { inline static const StringLiteral EQUATIONS_LIT = "equations"; }; +class IOGSingleToken : public FormalProperty { +public: + llvm::json::Value extraInfoToJSON() const override; + static std::unique_ptr + fromJSON(const llvm::json::Value &value, llvm::json::Path path); + + IOGSingleToken() = default; + IOGSingleToken(unsigned long id, TAG tag); + ~IOGSingleToken() = default; + + static bool classof(const FormalProperty *fp) { + return fp->getType() == TYPE::IOGSingleToken; + } + +private: +}; + class FormalPropertyTable { public: FormalPropertyTable() = default; diff --git a/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp b/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp index cd9ebffbc2..fa0b35e51b 100644 --- a/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp +++ b/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp @@ -280,6 +280,304 @@ HandshakeAnnotatePropertiesPass::annotateReconvergentPathFlow(ModuleOp modOp) { return success(); } +namespace { +struct IOG { + IOG() = default; + std::unordered_set units; + llvm::DenseSet channels; + mlir::Value entry; + + bool contains(Operation *op) { + auto iter = units.find(op); + return iter != units.end(); + } + + bool contains(mlir::Value channel) { + auto iter = channels.find(channel); + return iter != channels.end(); + } + + void debug() { + std::vector stack; + llvm::DenseSet visited; + stack.push_back(entry); + visited.insert(entry); + while (!stack.empty()) { + mlir::Value channel = stack.back(); + stack.pop_back(); + Operation *prev = channel.getDefiningOp(); + if (prev == nullptr) { + llvm::errs() << "entry"; + } else { + llvm::errs() << getUniqueName(prev); + } + Operation *next = channel.getUses().begin()->getOwner(); + assert(next); + assert(contains(next)); + llvm::errs() << " -> " << getUniqueName(next) << "\n"; + for (mlir::Value out : next->getResults()) { + if (auto iter = visited.find(out); iter != visited.end()) + continue; + if (contains(out)) { + visited.insert(out); + stack.push_back(out); + } + } + } + } +}; + +struct IOGFinderCheckpoint { + IOG partial; + // Stack of channels at the edge that are not yet inserted into the IOG + std::vector unhandled; + // Set of channels that have been declared illegal by local rules + llvm::DenseSet illegals; + // Is the partial IOG still following the rules? Note that DONE does not + // actually mean done, as the `unhandled` stack should also be empty. + enum PROGRESS { ILLEGAL, PARTIAL, DONE }; + PROGRESS progress = PARTIAL; + Operation *endOp; + std::vector entries; + + PROGRESS getProgress() { + if (progress == ILLEGAL) + return ILLEGAL; + if (!unhandled.empty()) + return PARTIAL; + return progress; + } + + bool isLegal(mlir::Value channel) { + auto iter = illegals.find(channel); + return iter == illegals.end(); + } + + void follow(mlir::Value channel) { + if (!isLegal(channel)) { + // A non-legal channel has been followed, so mark this IOG as non-valid + progress = ILLEGAL; + return; + } + if (partial.contains(channel)) { + return; + } + unhandled.push_back(channel); + } + + void makeIllegal(mlir::Value channel) { + if (partial.contains(channel)) + progress = ILLEGAL; + // The legality of unhandled channels is checked in getNextOp + illegals.insert(channel); + } + + Operation *getNextOp() { + // Stop making progress if an illegal edge has been taken + if (progress == ILLEGAL) { + return nullptr; + } + + // Handle the `endOp` if it has not yet been inserted into the IOG + if (!partial.contains(endOp)) { + return endOp; + } + + if (unhandled.empty()) { + // All handling done! + return nullptr; + } + + // Look at channel at the top of the `unhandled` stack + auto channel = unhandled.back(); + + // If this channel has been marked as illegal, abort this branch + if (!isLegal(channel)) { + progress = ILLEGAL; + return nullptr; + } + + // If this channel is one of the target entry channels, mark the appropriate + // `entry` of the IOG and set the state accordingly + if (std::find(entries.begin(), entries.end(), channel) != entries.end()) { + partial.entry = channel; + progress = DONE; + } + + // To fully handle a channel, both the operation before and after have to be + // handled + Operation *before = channel.getDefiningOp(); + if (before && !partial.contains(before)) { + partial.units.insert(before); + return before; + } + + Operation *after = channel.getUses().begin()->getOwner(); + if (after && !partial.contains(after)) { + partial.units.insert(after); + return after; + } + + // Both sides of this channel have been handled, so this channel is done and + // can be removed/inserted into the appropriate locations + unhandled.pop_back(); + partial.channels.insert(channel); + + // Return next channel on unhandled stack + return getNextOp(); + } +}; + +struct IOGFinder { + IOGFinder() = default; + ~IOGFinder() = default; + std::vector partials; + std::vector finals; + + // This function takes a checkpoint and a list of channels. For each channel + // c, it pushes the IOG where *only* channel c is taken, and all the rest are + // illegal. Used for forks (which only allow exactly one of its outputs) and + // join operations (which only allow exactly one of its inputs) + template + void followSingle(const IOGFinderCheckpoint &checkpoint, T options) { + for (mlir::Value channel : options) { + IOGFinderCheckpoint goHere = checkpoint; + goHere.follow(channel); + for (mlir::Value other : options) { + if (channel == other) + continue; + goHere.makeIllegal(other); + } + partials.push_back(goHere); + } + } + + // Take a step towards computing all IOGs. Does nothing if there are no + // partial IOGs. + // Example usage: + // IOGFinder finder = ... + // while (!finder.partials.empty()) { + // finder.step(); + // } + void step() { + if (partials.empty()) + return; + auto checkpoint = partials.back(); + partials.pop_back(); + if (checkpoint.progress == IOGFinderCheckpoint::PROGRESS::ILLEGAL) + return; + + Operation *op = checkpoint.getNextOp(); + if (op == nullptr) { + if (checkpoint.progress == IOGFinderCheckpoint::PROGRESS::DONE) { + finals.push_back(checkpoint.partial); + } + return; + } + checkpoint.partial.units.insert(op); + + if (auto endOp = dyn_cast(op)) { + followSingle(checkpoint, endOp.getOperands()); + } else if (auto bufOp = dyn_cast(op)) { + checkpoint.follow(bufOp.getOperand()); + checkpoint.follow(bufOp.getResult()); + partials.push_back(checkpoint); + } else if (auto condBr = dyn_cast(op)) { + checkpoint.follow(condBr.getTrueResult()); + checkpoint.follow(condBr.getFalseResult()); + followSingle(checkpoint, condBr.getOperands()); + } else if (auto forkOp = dyn_cast(op)) { + checkpoint.follow(forkOp.getOperand()); + followSingle(checkpoint, forkOp.getResults()); + } else if (auto muxOp = dyn_cast(op)) { + // Either all data inputs, or the select input. Output always + checkpoint.follow(muxOp.getResult()); + auto dataFollower = checkpoint; + auto selectFollower = checkpoint; + for (auto data : muxOp.getDataOperands()) { + dataFollower.follow(data); + selectFollower.makeIllegal(data); + } + + dataFollower.makeIllegal(muxOp.getSelectOperand()); + selectFollower.follow(muxOp.getSelectOperand()); + + partials.push_back(dataFollower); + partials.push_back(selectFollower); + } else if (auto cmerge = dyn_cast(op)) { + for (auto data : cmerge.getDataOperands()) { + checkpoint.follow(data); + } + followSingle(checkpoint, cmerge.getResults()); + } else if (auto arithOp = dyn_cast(op)) { + checkpoint.follow(arithOp->getResults()[0]); + followSingle(checkpoint, arithOp->getOperands()); + } else if (isa(op)) { + // These operations can not be part of an IOG, as they generate/consume + // tokens. This means that the partial IOGs looking at these operations + // can be discarded, so nothing needs to be done + } else if (auto loadOp = dyn_cast(op)) { + checkpoint.follow(loadOp.getAddress()); + checkpoint.follow(loadOp.getAddressResult()); + checkpoint.follow(loadOp.getData()); + checkpoint.follow(loadOp.getDataResult()); + partials.push_back(checkpoint); + } else if (auto memCon = dyn_cast(op)) { + // Memory controllers will be handled at the annotation part. To make sure + // this IOG is not discarded, this checkpoint is added back to the stack + // of partial IOGs + partials.push_back(checkpoint); + } else { + op->emitError("unhandled case in IOG finding"); + } + } +}; + +std::vector findAllIOGsWithEndOp(std::vector entries, + EndOp endOp) { + IOGFinder finder{}; + auto x = IOGFinderCheckpoint{ + .partial = IOG(), + .unhandled = std::vector(), + .illegals = llvm::DenseSet(), + .endOp = endOp, + .entries = std::move(entries), + }; + finder.partials.push_back(x); + + // Compute all IOGs + while (!finder.partials.empty()) { + finder.step(); + } + return finder.finals; +} + +std::vector findAllIOGs(ModuleOp modOp) { + std::vector ret{}; + for (handshake::FuncOp funcOp : modOp.getOps()) { + // Each argument corresponds to an entry node. + std::vector arguments; + for (mlir::Value arg : funcOp.getRegion().getArguments()) { + arguments.push_back(arg); + } + + for (auto &op : funcOp.getOps()) { + if (auto endOp = dyn_cast(op)) { + for (auto &x : findAllIOGsWithEndOp(arguments, endOp)) { + ret.push_back(x); + } + } + } + } + for (auto &x : ret) { + llvm::errs() << "---------DEBUG----------\n"; + x.debug(); + llvm::errs() << "------------------------\n"; + } + return ret; +} +} // namespace + void HandshakeAnnotatePropertiesPass::runDynamaticPass() { ModuleOp modOp = getOperation(); @@ -294,6 +592,8 @@ void HandshakeAnnotatePropertiesPass::runDynamaticPass() { return signalPassFailure(); if (failed(annotateReconvergentPathFlow(modOp))) return signalPassFailure(); + + findAllIOGs(modOp); } llvm::json::Value jsonVal(std::move(propertyTable)); From e56f3805663425709a8d5e086328eff69cf418bf Mon Sep 17 00:00:00 2001 From: Bas Niekel Date: Thu, 16 Apr 2026 15:26:31 +0200 Subject: [PATCH 02/29] annotating invariant 6: Consecutive tokens within an IOG must have an active fork in between --- .../experimental/Support/FormalProperty.h | 28 ++ .../HandshakeAnnotateProperties.cpp | 300 ++++++++++++++---- experimental/lib/Support/FormalProperty.cpp | 83 +++++ tools/export-rtl/export-rtl.cpp | 18 ++ 4 files changed, 376 insertions(+), 53 deletions(-) diff --git a/experimental/include/experimental/Support/FormalProperty.h b/experimental/include/experimental/Support/FormalProperty.h index 9ea918d132..784c01e7f4 100644 --- a/experimental/include/experimental/Support/FormalProperty.h +++ b/experimental/include/experimental/Support/FormalProperty.h @@ -34,6 +34,7 @@ class FormalProperty { CSOAFAF, /* Copied Slots Of Active Forks Are Full */ RPF, /* Reconvergent Path Flow */ IOGSingleToken, + IOGConsecutiveTokens, }; TAG getTag() const { return tag; } @@ -286,6 +287,33 @@ class IOGSingleToken : public FormalProperty { private: }; +class IOGConsecutiveTokens : public FormalProperty { +public: + llvm::json::Value extraInfoToJSON() const override; + static std::unique_ptr + fromJSON(const llvm::json::Value &value, llvm::json::Path path); + + IOGConsecutiveTokens() = default; + IOGConsecutiveTokens(unsigned long id, TAG tag, + std::unique_ptr slot1, + std::unique_ptr slot2, + std::vector sents); + ~IOGConsecutiveTokens() = default; + + static bool classof(const FormalProperty *fp) { + return fp->getType() == TYPE::IOGConsecutiveTokens; + } + + std::unique_ptr slot1; + std::unique_ptr slot2; + std::vector sents; + +private: + inline static const StringLiteral SLOT1_LIT = "slot1"; + inline static const StringLiteral SLOT2_LIT = "slot2"; + inline static const StringLiteral SENTS_LIT = "sents"; +}; + class FormalPropertyTable { public: FormalPropertyTable() = default; diff --git a/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp b/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp index fa0b35e51b..9e6779e494 100644 --- a/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp +++ b/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp @@ -58,6 +58,7 @@ namespace experimental { namespace { +struct IOG; struct HandshakeAnnotatePropertiesPass : public dynamatic::experimental::impl::HandshakeAnnotatePropertiesBase< HandshakeAnnotatePropertiesPass> { @@ -82,6 +83,7 @@ struct HandshakeAnnotatePropertiesPass LogicalResult annotateCopiedSlots(Operation &op); LogicalResult annotateCopiedSlotsOfAllForks(ModuleOp modOp); LogicalResult annotateReconvergentPathFlow(ModuleOp modOp); + LogicalResult annotateIOGConsecutiveTokens(const IOG &iog); }; bool isChannelToBeChecked(OpResult res) { @@ -281,23 +283,46 @@ HandshakeAnnotatePropertiesPass::annotateReconvergentPathFlow(ModuleOp modOp) { } namespace { +struct IOGPath { + std::unordered_map prevSet; + std::unordered_map forwardSet; + Operation *from; + Operation *to; + IOGPath(const IOG &iog, Operation *from, Operation *to); + + void computeBackPath(const IOG &iog); + void computeForwardPathFromBackPath(); + + bool exists() const { return prevSet.find(to) != prevSet.end(); } + mlir::Value stepBack(Operation *cur) const { + auto iter = prevSet.find(cur); + assert(iter != prevSet.end()); + return iter->second; + } + mlir::Value stepForward(Operation *cur) const { + auto iter = forwardSet.find(cur); + assert(iter != forwardSet.end()); + return iter->second; + } +}; + struct IOG { IOG() = default; std::unordered_set units; llvm::DenseSet channels; mlir::Value entry; - bool contains(Operation *op) { + bool contains(Operation *op) const { auto iter = units.find(op); return iter != units.end(); } - bool contains(mlir::Value channel) { + bool contains(mlir::Value channel) const { auto iter = channels.find(channel); return iter != channels.end(); } - void debug() { + void debug() const { std::vector stack; llvm::DenseSet visited; stack.push_back(entry); @@ -327,6 +352,61 @@ struct IOG { } }; +IOGPath::IOGPath(const IOG &iog, Operation *fromArg, Operation *toArg) + : from(fromArg), to(toArg) { + assert(from && iog.contains(from)); + assert(to && iog.contains(to)); + computeBackPath(iog); + if (!exists()) { + return; + } + computeForwardPathFromBackPath(); +} + +void IOGPath::computeBackPath(const IOG &iog) { + std::vector stack; + for (mlir::Value out : from->getResults()) { + if (!iog.contains(out)) { + continue; + } + stack.push_back(out); + } + while (!stack.empty()) { + mlir::Value channel = stack.back(); + stack.pop_back(); + Operation *next = channel.getUses().begin()->getOwner(); + assert(next); + assert(iog.contains(next)); + if (prevSet.find(next) != prevSet.end()) { + continue; + } + prevSet.insert({next, channel}); + if (next == to) { + return; + } + + for (mlir::Value out : next->getResults()) { + if (!iog.contains(out)) { + // Only consider channels part of the IOG + continue; + } + stack.push_back(out); + } + } +} + +void IOGPath::computeForwardPathFromBackPath() { + assert(exists()); + Operation *cur = to; + while (cur != from) { + mlir::Value channel = stepBack(cur); + Operation *prev = channel.getDefiningOp(); + assert(prev); + forwardSet.insert({prev, channel}); + cur = prev; + } +} + struct IOGFinderCheckpoint { IOG partial; // Stack of channels at the edge that are not yet inserted into the IOG @@ -337,8 +417,13 @@ struct IOGFinderCheckpoint { // actually mean done, as the `unhandled` stack should also be empty. enum PROGRESS { ILLEGAL, PARTIAL, DONE }; PROGRESS progress = PARTIAL; - Operation *endOp; - std::vector entries; + + IOGFinderCheckpoint() = default; + IOGFinderCheckpoint(mlir::Value entry) { + partial.entry = entry; + follow(entry); + progress = DONE; + } PROGRESS getProgress() { if (progress == ILLEGAL) @@ -363,11 +448,13 @@ struct IOGFinderCheckpoint { return; } unhandled.push_back(channel); + partial.channels.insert(channel); } void makeIllegal(mlir::Value channel) { - if (partial.contains(channel)) + if (partial.contains(channel)) { progress = ILLEGAL; + } // The legality of unhandled channels is checked in getNextOp illegals.insert(channel); } @@ -378,11 +465,6 @@ struct IOGFinderCheckpoint { return nullptr; } - // Handle the `endOp` if it has not yet been inserted into the IOG - if (!partial.contains(endOp)) { - return endOp; - } - if (unhandled.empty()) { // All handling done! return nullptr; @@ -397,13 +479,6 @@ struct IOGFinderCheckpoint { return nullptr; } - // If this channel is one of the target entry channels, mark the appropriate - // `entry` of the IOG and set the state accordingly - if (std::find(entries.begin(), entries.end(), channel) != entries.end()) { - partial.entry = channel; - progress = DONE; - } - // To fully handle a channel, both the operation before and after have to be // handled Operation *before = channel.getDefiningOp(); @@ -421,7 +496,6 @@ struct IOGFinderCheckpoint { // Both sides of this channel have been handled, so this channel is done and // can be removed/inserted into the appropriate locations unhandled.pop_back(); - partial.channels.insert(channel); // Return next channel on unhandled stack return getNextOp(); @@ -440,6 +514,32 @@ struct IOGFinder { // join operations (which only allow exactly one of its inputs) template void followSingle(const IOGFinderCheckpoint &checkpoint, T options) { + size_t n = 0; + mlir::Value singleTaken = nullptr; + for (mlir::Value channel : options) { + if (checkpoint.partial.contains(channel)) { + n += 1; + singleTaken = channel; + } + } + if (n == 1) { + IOGFinderCheckpoint goHere = checkpoint; + // singleTaken is already part of the IOG, so no need to follow it + // goHere.follow(singleTaken); + for (mlir::Value other : options) { + if (other == singleTaken) { + continue; + } + goHere.makeIllegal(other); + } + partials.push_back(goHere); + return; + } + if (n > 1) { + // Multiple paths taken, but only single is allowed! => No IOGs from this + // branch + return; + } for (mlir::Value channel : options) { IOGFinderCheckpoint goHere = checkpoint; goHere.follow(channel); @@ -512,40 +612,33 @@ struct IOGFinder { } else if (auto arithOp = dyn_cast(op)) { checkpoint.follow(arithOp->getResults()[0]); followSingle(checkpoint, arithOp->getOperands()); - } else if (isa(op)) { - // These operations can not be part of an IOG, as they generate/consume - // tokens. This means that the partial IOGs looking at these operations - // can be discarded, so nothing needs to be done + } else if (auto sourceOp = dyn_cast(op)) { + // SourceOps can not be part of an IOG, as they act like entry nodes. This + // means that the partial IOGs looking at these operations can be + // discarded, so nothing needs to be done + } else if (isa(op)) { + partials.push_back(checkpoint); } else if (auto loadOp = dyn_cast(op)) { checkpoint.follow(loadOp.getAddress()); - checkpoint.follow(loadOp.getAddressResult()); - checkpoint.follow(loadOp.getData()); + // checkpoint.follow(loadOp.getAddressResult()); + // checkpoint.follow(loadOp.getData()); checkpoint.follow(loadOp.getDataResult()); partials.push_back(checkpoint); } else if (auto memCon = dyn_cast(op)) { - // Memory controllers will be handled at the annotation part. To make sure - // this IOG is not discarded, this checkpoint is added back to the stack - // of partial IOGs - partials.push_back(checkpoint); + // MemoryControllers are only accessed by control signals during this + // annotation, as the edges between loadOps/storeOps and the MC are not + // added to the IOG. These control signals usually grant trivial IOGs that + // can be skipped. } else { op->emitError("unhandled case in IOG finding"); } } }; -std::vector findAllIOGsWithEndOp(std::vector entries, - EndOp endOp) { +std::vector findAllIOGsWithEntry(mlir::Value entry) { IOGFinder finder{}; - auto x = IOGFinderCheckpoint{ - .partial = IOG(), - .unhandled = std::vector(), - .illegals = llvm::DenseSet(), - .endOp = endOp, - .entries = std::move(entries), - }; - finder.partials.push_back(x); - - // Compute all IOGs + IOGFinderCheckpoint cp(entry); + finder.partials.push_back(cp); while (!finder.partials.empty()) { finder.step(); } @@ -556,35 +649,132 @@ std::vector findAllIOGs(ModuleOp modOp) { std::vector ret{}; for (handshake::FuncOp funcOp : modOp.getOps()) { // Each argument corresponds to an entry node. - std::vector arguments; for (mlir::Value arg : funcOp.getRegion().getArguments()) { - arguments.push_back(arg); + for (auto &x : findAllIOGsWithEntry(arg)) { + ret.push_back(x); + } } + } + return ret; +} - for (auto &op : funcOp.getOps()) { - if (auto endOp = dyn_cast(op)) { - for (auto &x : findAllIOGsWithEndOp(arguments, endOp)) { - ret.push_back(x); +std::vector +followPathAndGetCopiedSents(const IOGPath &path) { + std::vector sents; + Operation *cur = path.from; + bool first = true; + while (cur != path.to) { + if (!first) { + if (auto slot = dyn_cast(cur)) { + return sents; + } + } + first = false; + mlir::Value forward = path.stepForward(cur); + if (auto sent = dyn_cast(cur)) { + // FORK DETECTED!! + size_t index; + // inconvenient way of getting the correct sent namer, but there is no + // better way for now + for (auto [i, channel] : llvm::enumerate(sent->getResults())) { + if (channel == forward) { + index = i; } } + sents.push_back(sent.getInternalSentStateNamers()[index]); } + cur = forward.getUses().begin()->getOwner(); } - for (auto &x : ret) { - llvm::errs() << "---------DEBUG----------\n"; - x.debug(); - llvm::errs() << "------------------------\n"; + return sents; +} + +LogicalResult +HandshakeAnnotatePropertiesPass::annotateIOGConsecutiveTokens(const IOG &iog) { + llvm::errs() << "performing IOG Consecutive tokens pass\n"; + llvm::errs() << "---------DEBUG----------\n"; + iog.debug(); + llvm::errs() << "---------UNITS----------\n"; + for (auto *op : iog.units) { + llvm::errs() << getUniqueName(op) << "\n"; } - return ret; + llvm::errs() << "---------CHANNELS-------\n"; + for (auto channel : iog.channels) { + Operation *before = channel.getDefiningOp(); + if (before == nullptr) { + llvm::errs() << "entry"; + } else { + llvm::errs() << getUniqueName(before); + } + Operation *after = channel.getUses().begin()->getOwner(); + assert(after); + llvm::errs() << " -> " << getUniqueName(after) << "\n"; + } + llvm::errs() << "------------------------\n"; + std::vector slots; + for (auto &op : iog.units) { + if (auto slot = dyn_cast(op)) { + slots.push_back(slot); + } + } + for (auto slot1 = slots.begin(); slot1 != slots.end(); ++slot1) { + for (auto slot2 = slot1 + 1; slot2 != slots.end(); ++slot2) { + if (slot1->getOperation() == slot2->getOperation()) { + continue; + } + std::vector copiedSents; + IOGPath path = IOGPath(iog, *slot1, *slot2); + if (path.exists()) { + std::vector extras = + followPathAndGetCopiedSents(path); + copiedSents.insert(copiedSents.end(), extras.begin(), extras.end()); + } + + path = IOGPath(iog, *slot2, *slot1); + if (path.exists()) { + std::vector extras = + followPathAndGetCopiedSents(path); + copiedSents.insert(copiedSents.end(), extras.begin(), extras.end()); + } + // Even if the copiedSents is empty, this invariant is interesting! It + // means that both slots cannot be occupied at the same time, as there is + // only (at most) one token in the IOG + auto slots1 = slot1->getInternalSlotStateNamers(); + auto slots2 = slot2->getInternalSlotStateNamers(); + /* + if (slots1.size() != 1) { + assert(false && "todo"); + return failure(); + } + if (slots2.size() != 1) { + assert(false && "todo"); + return failure(); + } + */ + std::unique_ptr slotStart = + std::make_unique(slots1[0]); + std::unique_ptr slotEnd = + std::make_unique(slots2[0]); + auto p = IOGConsecutiveTokens(uid, FormalProperty::TAG::OPT, + std::move(slotStart), std::move(slotEnd), + copiedSents); + uid++; + propertyTable.push_back(p.toJSON()); + } + } + return success(); } + } // namespace void HandshakeAnnotatePropertiesPass::runDynamaticPass() { ModuleOp modOp = getOperation(); +#if 0 if (failed(annotateAbsenceOfBackpressure(modOp))) return signalPassFailure(); if (failed(annotateValidEquivalence(modOp))) return signalPassFailure(); +#endif if (annotateInvariants) { if (failed(annotateEagerForkNotAllOutputSent(modOp))) return signalPassFailure(); @@ -593,7 +783,11 @@ void HandshakeAnnotatePropertiesPass::runDynamaticPass() { if (failed(annotateReconvergentPathFlow(modOp))) return signalPassFailure(); - findAllIOGs(modOp); + auto iogs = findAllIOGs(modOp); + for (const auto &iog : iogs) { + if (failed(annotateIOGConsecutiveTokens(iog))) + return signalPassFailure(); + } } llvm::json::Value jsonVal(std::move(propertyTable)); diff --git a/experimental/lib/Support/FormalProperty.cpp b/experimental/lib/Support/FormalProperty.cpp index d1bdcbf932..5f3f84a0a2 100644 --- a/experimental/lib/Support/FormalProperty.cpp +++ b/experimental/lib/Support/FormalProperty.cpp @@ -33,6 +33,10 @@ FormalProperty::typeFromStr(const std::string &s) { return FormalProperty::TYPE::CSOAFAF; if (s == "RPF") return FormalProperty::TYPE::RPF; + if (s == "IOGSingleToken") + return FormalProperty::TYPE::IOGSingleToken; + if (s == "IOGConsecutiveTokens") + return FormalProperty::TYPE::IOGConsecutiveTokens; return std::nullopt; } @@ -49,6 +53,10 @@ std::string FormalProperty::typeToStr(TYPE t) { return "CSOAFAF"; case TYPE::RPF: return "RPF"; + case TYPE::IOGSingleToken: + return "IOGSingleToken"; + case TYPE::IOGConsecutiveTokens: + return "IOGConsecutiveTokens"; } } @@ -108,6 +116,11 @@ FormalProperty::fromJSON(const llvm::json::Value &value, path.field(INFO_LIT)); case TYPE::RPF: return ReconvergentPathFlow::fromJSON(value, path.field(INFO_LIT)); + case TYPE::IOGSingleToken: + assert(false && "todo"); + return nullptr; + case TYPE::IOGConsecutiveTokens: + return IOGConsecutiveTokens::fromJSON(value, path.field(INFO_LIT)); } } @@ -380,6 +393,76 @@ ReconvergentPathFlow::fromJSON(const llvm::json::Value &value, return prop; } +// IOGConsecutiveTokens + +llvm::json::Value IOGConsecutiveTokens::extraInfoToJSON() const { + std::vector sentsJSON; + sentsJSON.reserve(sents.size()); + for (auto &sent : sents) { + sentsJSON.push_back(sent.toInnerJSON()); + } + llvm::json::Value sentsValue = sentsJSON; + + return llvm::json::Object({{SLOT1_LIT, slot1->toJSON()}, + {SLOT2_LIT, slot2->toJSON()}, + {SENTS_LIT, sentsValue}}); +} + +std::unique_ptr +IOGConsecutiveTokens::fromJSON(const llvm::json::Value &value, + llvm::json::Path path) { + auto prop = std::make_unique(); + llvm::json::Value info = prop->parseBaseAndExtractInfo(value, path); + + llvm::json::Object *obj = info.getAsObject(); + assert(obj); + if (auto iter = obj->find(SLOT1_LIT); iter != obj->end()) { + prop->slot1 = InternalStateNamer::fromJSON(iter->second, path); + } else { + path.report(json::ERR_MISSING_VALUE); + return nullptr; + } + + if (auto iter = obj->find(SLOT2_LIT); iter != obj->end()) { + prop->slot2 = InternalStateNamer::fromJSON(iter->second, path); + } else { + path.report(json::ERR_MISSING_VALUE); + return nullptr; + } + + if (auto iter = obj->find(SENTS_LIT); iter != obj->end()) { + llvm::json::Array *sentsArray = iter->second.getAsArray(); + assert(sentsArray); + prop->sents.reserve(sentsArray->size()); + for (const llvm::json::Value &sentValue : *sentsArray) { + auto innerJSON = EagerForkSentNamer::fromInnerJSON(sentValue, path); + assert(innerJSON); + prop->sents.push_back(*innerJSON); + } + } else { + path.report(json::ERR_MISSING_VALUE); + } + + /* + auto prop = std::make_unique(); + auto info = prop->parseBaseAndExtractInfo(value, path); + + const llvm::json::Object *obj = info.getAsObject(); + if (!obj) + return nullptr; + assert(false && "TODO"); + */ + return prop; +} + +IOGConsecutiveTokens::IOGConsecutiveTokens( + unsigned long id, TAG tag, std::unique_ptr slot1, + std::unique_ptr slot2, + std::vector sents) + : FormalProperty(id, tag, TYPE::IOGConsecutiveTokens), + slot1(std::move(slot1)), slot2(std::move(slot2)), + sents(std::move(sents)) {} + LogicalResult FormalPropertyTable::addPropertiesFromJSON(StringRef filepath) { // Open the properties' database std::ifstream inputFile(filepath.str()); diff --git a/tools/export-rtl/export-rtl.cpp b/tools/export-rtl/export-rtl.cpp index f5d255f995..a65e340f0d 100644 --- a/tools/export-rtl/export-rtl.cpp +++ b/tools/export-rtl/export-rtl.cpp @@ -1297,6 +1297,24 @@ LogicalResult SMVWriter::createProperties(WriteModData &data) const { } std::string propertyString = llvm::join(eqs, " & "); data.properties[p->getId()] = {propertyString, propertyTag}; + } else if (auto *p = llvm::dyn_cast(property.get())) { + // buffer1.slot_full | buffer2.slot_full -> fork3.outs1_sent | + // fork4.outs0_sent + std::string right; + if (p->sents.empty()) { + right = "FALSE"; + } else { + std::vector sentNames; + sentNames.reserve(p->sents.size()); + for (auto &sent : p->sents) { + sentNames.push_back(sent.getSMVName()); + } + right = llvm::join(sentNames, " | "); + } + std::string full = + llvm::formatv("({0} & {1}) -> ({2})", p->slot1->getSMVName(), + p->slot2->getSMVName(), right); + data.properties[p->getId()] = {full, propertyTag}; } else { llvm::errs() << "Formal property Type not known\n"; return failure(); From 8a4696f2d1264b460d5d6326dd50c391952733e2 Mon Sep 17 00:00:00 2001 From: Bas Niekel Date: Thu, 16 Apr 2026 16:00:40 +0200 Subject: [PATCH 03/29] invariant now works for any slot within an operation (rather than just the first slot) edge case: As the MC is not part of the IOG, tokens "hidden" within MC are not accounted for --- .../HandshakeAnnotateProperties.cpp | 23 ++++------------ .../handshake/buffers/one_slot_break_dv.py | 2 ++ .../handshake/buffers/one_slot_break_r.py | 2 ++ .../smv/generators/handshake/load.py | 2 ++ .../Dialect/Handshake/HandshakeInterfaces.td | 12 +++++++++ .../Handshake/HandshakeOpInternalStateNamer.h | 27 +++++++++++++++++++ .../HandshakeOpInternalStateNamer.cpp | 19 +++++++++++++ tools/export-rtl/export-rtl.cpp | 10 ++++--- 8 files changed, 75 insertions(+), 22 deletions(-) diff --git a/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp b/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp index 9e6779e494..b3f657e5c6 100644 --- a/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp +++ b/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp @@ -738,25 +738,12 @@ HandshakeAnnotatePropertiesPass::annotateIOGConsecutiveTokens(const IOG &iog) { // Even if the copiedSents is empty, this invariant is interesting! It // means that both slots cannot be occupied at the same time, as there is // only (at most) one token in the IOG - auto slots1 = slot1->getInternalSlotStateNamers(); - auto slots2 = slot2->getInternalSlotStateNamers(); - /* - if (slots1.size() != 1) { - assert(false && "todo"); - return failure(); - } - if (slots2.size() != 1) { - assert(false && "todo"); - return failure(); - } - */ - std::unique_ptr slotStart = - std::make_unique(slots1[0]); - std::unique_ptr slotEnd = - std::make_unique(slots2[0]); + + auto slot1Namer = slot1->getTokenCountNamer(); + auto slot2Namer = slot2->getTokenCountNamer(); auto p = IOGConsecutiveTokens(uid, FormalProperty::TAG::OPT, - std::move(slotStart), std::move(slotEnd), - copiedSents); + std::move(slot1Namer), + std::move(slot2Namer), copiedSents); uid++; propertyTable.push_back(p.toJSON()); } diff --git a/experimental/tools/unit-generators/smv/generators/handshake/buffers/one_slot_break_dv.py b/experimental/tools/unit-generators/smv/generators/handshake/buffers/one_slot_break_dv.py index 6cad16c8af..1a8f6972de 100644 --- a/experimental/tools/unit-generators/smv/generators/handshake/buffers/one_slot_break_dv.py +++ b/experimental/tools/unit-generators/smv/generators/handshake/buffers/one_slot_break_dv.py @@ -25,6 +25,7 @@ def _generate_one_slot_break_dv_dataless(name): ins_ready := !outs_valid_i | outs_ready; outs_valid := outs_valid_i; slot_0_full := outs_valid_i; + slotted_token_count := count(slot_0_full); """ @@ -48,6 +49,7 @@ def _generate_one_slot_break_dv(name, data_type): outs_valid := inner_one_slot_break_dv.outs_valid; outs := data; slot_0_full := inner_one_slot_break_dv.outs_valid_i; + slotted_token_count := inner_one_slot_break_dv.slotted_token_count; {_generate_one_slot_break_dv_dataless(f"{name}__one_slot_break_dv_dataless")} """ diff --git a/experimental/tools/unit-generators/smv/generators/handshake/buffers/one_slot_break_r.py b/experimental/tools/unit-generators/smv/generators/handshake/buffers/one_slot_break_r.py index b7d184c01f..f4b67af627 100644 --- a/experimental/tools/unit-generators/smv/generators/handshake/buffers/one_slot_break_r.py +++ b/experimental/tools/unit-generators/smv/generators/handshake/buffers/one_slot_break_r.py @@ -26,6 +26,7 @@ def _generate_one_slot_break_r_dataless(name): outs_valid := ins_valid | full; slot_0_full := full; + slotted_token_count := count(slot_0_full); """ @@ -47,6 +48,7 @@ def _generate_one_slot_break_r(name, data_type): outs := inner_one_slot_break_r.full ? data : ins; slot_0_full := inner_one_slot_break_r.slot_0_full; + slotted_token_count := inner_one_slot_break_r.slotted_token_count; {_generate_one_slot_break_r_dataless(f"{name}__one_slot_break_r_dataless")} """ diff --git a/experimental/tools/unit-generators/smv/generators/handshake/load.py b/experimental/tools/unit-generators/smv/generators/handshake/load.py index 58dd9c3552..10bfcd51af 100644 --- a/experimental/tools/unit-generators/smv/generators/handshake/load.py +++ b/experimental/tools/unit-generators/smv/generators/handshake/load.py @@ -28,6 +28,8 @@ def _generate_load(name, data_type, addr_type): addr_full := inner_addr_one_slot_break_r.slot_0_full; data_full := inner_data_one_slot_break_r.slot_0_full; + slotted_token_count := count(addr_full, data_full); + {generate_one_slot_break_r(f"{name}__addr_one_slot_break_r", {ATTR_BITWIDTH: addr_type.bitwidth})} {generate_one_slot_break_r(f"{name}__data_one_slot_break_r", {ATTR_BITWIDTH: data_type.bitwidth})} """ diff --git a/include/dynamatic/Dialect/Handshake/HandshakeInterfaces.td b/include/dynamatic/Dialect/Handshake/HandshakeInterfaces.td index 80ba20f0b4..9bfdae62ea 100644 --- a/include/dynamatic/Dialect/Handshake/HandshakeInterfaces.td +++ b/include/dynamatic/Dialect/Handshake/HandshakeInterfaces.td @@ -72,6 +72,18 @@ def BufferLikeOpInterface : OpInterface<"BufferLikeOpInterface"> { }], "std::vector", "getInternalSlotStateNamers", (ins) >, + InterfaceMethod<[{ + Get the internal state namer of the number of tokens currently + contained within this operation. + }], + "std::unique_ptr", "getTokenCountNamer", (ins), [{ + Operation *op = $_op.getOperation(); + auto name = op->getAttrOfType<::mlir::StringAttr>(NameAnalysis::ATTR_NAME); + if (!name) + return nullptr; + return std::make_unique(name.str()); + }] + >, ]; } diff --git a/include/dynamatic/Dialect/Handshake/HandshakeOpInternalStateNamer.h b/include/dynamatic/Dialect/Handshake/HandshakeOpInternalStateNamer.h index 45c069a377..9ced03aa9b 100644 --- a/include/dynamatic/Dialect/Handshake/HandshakeOpInternalStateNamer.h +++ b/include/dynamatic/Dialect/Handshake/HandshakeOpInternalStateNamer.h @@ -32,6 +32,7 @@ struct InternalStateNamer { PipelineSlot, Constrained, MemoryControllerSlot, + TokenCount, }; static std::optional typeFromStr(const std::string &s); static std::string typeToStr(TYPE t); @@ -74,6 +75,7 @@ struct InternalStateNamer { static constexpr llvm::StringLiteral CONSTRAINED = "Constrained"; static constexpr llvm::StringLiteral MEMORY_CONTROLLER_SLOT = "MemoryControllerSlot"; + static constexpr llvm::StringLiteral TOKEN_COUNT = "TokenCount"; static constexpr llvm::StringLiteral INNER_LIT = "inner"; }; @@ -285,6 +287,31 @@ struct PipelineSlotNamer : InternalStateNamer { static constexpr llvm::StringLiteral SLOT_INDEX_LIT = "pipeline_index"; }; +struct TokenCountNamer : InternalStateNamer { + TokenCountNamer() = default; + TokenCountNamer(const std::string &opName) + : InternalStateNamer(TYPE::TokenCount), opName(opName) {} + ~TokenCountNamer() = default; + + static inline bool classof(const InternalStateNamer *fp) { + return fp->type == TYPE::TokenCount; + } + + inline std::string getSMVName() const override { + return llvm::formatv("{0}.slotted_token_count", opName); + } + + inline llvm::json::Value toInnerJSON() const override { + return llvm::json::Object({{OPERATION_LIT, opName}}); + } + + std::unique_ptr static fromInnerJSON( + const llvm::json::Value &value, llvm::json::Path path); + std::string opName; + + static constexpr llvm::StringLiteral OPERATION_LIT = "operation"; +}; + struct MemoryControllerSlotNamer : InternalStateNamer { enum PortType { Load, diff --git a/lib/Dialect/Handshake/HandshakeOpInternalStateNamer.cpp b/lib/Dialect/Handshake/HandshakeOpInternalStateNamer.cpp index 0456811e29..406ca44b10 100644 --- a/lib/Dialect/Handshake/HandshakeOpInternalStateNamer.cpp +++ b/lib/Dialect/Handshake/HandshakeOpInternalStateNamer.cpp @@ -14,6 +14,9 @@ InternalStateNamer::typeFromStr(const std::string &s) { return TYPE::Constrained; if (s == MEMORY_CONTROLLER_SLOT) return TYPE::MemoryControllerSlot; + if (s == TOKEN_COUNT) + return TYPE::TokenCount; + llvm::errs() << "unknown type\n"; return std::nullopt; } @@ -29,6 +32,8 @@ std::string InternalStateNamer::typeToStr(TYPE t) { return CONSTRAINED.str(); case TYPE::MemoryControllerSlot: return MEMORY_CONTROLLER_SLOT.str(); + case TYPE::TokenCount: + return TOKEN_COUNT.str(); } } @@ -67,6 +72,10 @@ InternalStateNamer::fromJSON(const llvm::json::Value &value, case TYPE::Constrained: assert(false && "todo"); break; + case TYPE::TokenCount: + prop = TokenCountNamer::fromInnerJSON(inner, path); + assert(prop && "inner token count failed"); + break; case TYPE::MemoryControllerSlot: prop = MemoryControllerSlotNamer::fromInnerJSON(inner, path); assert(prop && "mc slot failed"); @@ -137,6 +146,16 @@ PipelineSlotNamer::fromInnerJSON(const llvm::json::Value &value, return prop; } +std::unique_ptr +TokenCountNamer::fromInnerJSON(const llvm::json::Value &value, + llvm::json::Path path) { + llvm::json::ObjectMapper mapper(value, path); + auto prop = std::make_unique(); + if (!mapper || !mapper.map(OPERATION_LIT, prop->opName)) + return nullptr; + return prop; +} + std::unique_ptr ConstrainedNamer::fromInnerJSON(const llvm::json::Value &value, llvm::json::Path path) { diff --git a/tools/export-rtl/export-rtl.cpp b/tools/export-rtl/export-rtl.cpp index a65e340f0d..ab438acc8b 100644 --- a/tools/export-rtl/export-rtl.cpp +++ b/tools/export-rtl/export-rtl.cpp @@ -1298,8 +1298,8 @@ LogicalResult SMVWriter::createProperties(WriteModData &data) const { std::string propertyString = llvm::join(eqs, " & "); data.properties[p->getId()] = {propertyString, propertyTag}; } else if (auto *p = llvm::dyn_cast(property.get())) { - // buffer1.slot_full | buffer2.slot_full -> fork3.outs1_sent | - // fork4.outs0_sent + // buffer1.slotted_token_count > 0 & buffer2.slotted_token_count > 0 -> + // fork3.outs1_sent | fork4.outs0_sent std::string right; if (p->sents.empty()) { right = "FALSE"; @@ -1311,9 +1311,11 @@ LogicalResult SMVWriter::createProperties(WriteModData &data) const { } right = llvm::join(sentNames, " | "); } + assert(p->slot1); + assert(p->slot2); std::string full = - llvm::formatv("({0} & {1}) -> ({2})", p->slot1->getSMVName(), - p->slot2->getSMVName(), right); + llvm::formatv("(({0} > 0) & ({1} > 0)) -> ({2})", + p->slot1->getSMVName(), p->slot2->getSMVName(), right); data.properties[p->getId()] = {full, propertyTag}; } else { llvm::errs() << "Formal property Type not known\n"; From 935a000460a0be1ef0fcc40252745f362eceea24 Mon Sep 17 00:00:00 2001 From: Bas Niekel Date: Thu, 16 Apr 2026 16:44:26 +0200 Subject: [PATCH 04/29] small cleanup of IOG generation code with better naming --- .../HandshakeAnnotateProperties.cpp | 301 +++++++++--------- 1 file changed, 142 insertions(+), 159 deletions(-) diff --git a/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp b/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp index b3f657e5c6..50550ab2c3 100644 --- a/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp +++ b/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp @@ -407,223 +407,175 @@ void IOGPath::computeForwardPathFromBackPath() { } } -struct IOGFinderCheckpoint { - IOG partial; +struct IOGCandidate { + IOG iog; // Stack of channels at the edge that are not yet inserted into the IOG - std::vector unhandled; + std::vector dfsQueue; // Set of channels that have been declared illegal by local rules - llvm::DenseSet illegals; - // Is the partial IOG still following the rules? Note that DONE does not - // actually mean done, as the `unhandled` stack should also be empty. - enum PROGRESS { ILLEGAL, PARTIAL, DONE }; - PROGRESS progress = PARTIAL; + llvm::DenseSet illegalChannels; - IOGFinderCheckpoint() = default; - IOGFinderCheckpoint(mlir::Value entry) { - partial.entry = entry; - follow(entry); - progress = DONE; - } + // Is the partial IOG contained within this struct invalid? I.e., is an + // illegal edge part of the IOG? + bool invalidIOG = false; - PROGRESS getProgress() { - if (progress == ILLEGAL) - return ILLEGAL; - if (!unhandled.empty()) - return PARTIAL; - return progress; + IOGCandidate() = default; + IOGCandidate(mlir::Value entry) { + iog.entry = entry; + markFollowed(entry); } bool isLegal(mlir::Value channel) { - auto iter = illegals.find(channel); - return iter == illegals.end(); + auto iter = illegalChannels.find(channel); + return iter == illegalChannels.end(); } - void follow(mlir::Value channel) { + void markFollowed(mlir::Value channel) { if (!isLegal(channel)) { // A non-legal channel has been followed, so mark this IOG as non-valid - progress = ILLEGAL; + invalidIOG = true; return; } - if (partial.contains(channel)) { + if (iog.contains(channel)) { return; } - unhandled.push_back(channel); - partial.channels.insert(channel); + dfsQueue.push_back(channel); + iog.channels.insert(channel); } - void makeIllegal(mlir::Value channel) { - if (partial.contains(channel)) { - progress = ILLEGAL; + void markIllegal(mlir::Value channel) { + if (iog.contains(channel)) { + invalidIOG = true; } // The legality of unhandled channels is checked in getNextOp - illegals.insert(channel); + illegalChannels.insert(channel); } - Operation *getNextOp() { + std::optional getNextOpToAdd() { // Stop making progress if an illegal edge has been taken - if (progress == ILLEGAL) { - return nullptr; + if (invalidIOG) { + return std::nullopt; } - if (unhandled.empty()) { + if (dfsQueue.empty()) { // All handling done! - return nullptr; + return std::nullopt; } // Look at channel at the top of the `unhandled` stack - auto channel = unhandled.back(); + auto channel = dfsQueue.back(); // If this channel has been marked as illegal, abort this branch if (!isLegal(channel)) { - progress = ILLEGAL; - return nullptr; + invalidIOG = true; + return std::nullopt; } // To fully handle a channel, both the operation before and after have to be // handled Operation *before = channel.getDefiningOp(); - if (before && !partial.contains(before)) { - partial.units.insert(before); + if (before && !iog.contains(before)) { + iog.units.insert(before); return before; } Operation *after = channel.getUses().begin()->getOwner(); - if (after && !partial.contains(after)) { - partial.units.insert(after); + if (after && !iog.contains(after)) { + iog.units.insert(after); return after; } // Both sides of this channel have been handled, so this channel is done and // can be removed/inserted into the appropriate locations - unhandled.pop_back(); + dfsQueue.pop_back(); // Return next channel on unhandled stack - return getNextOp(); + return getNextOpToAdd(); } }; -struct IOGFinder { - IOGFinder() = default; - ~IOGFinder() = default; - std::vector partials; - std::vector finals; - - // This function takes a checkpoint and a list of channels. For each channel - // c, it pushes the IOG where *only* channel c is taken, and all the rest are - // illegal. Used for forks (which only allow exactly one of its outputs) and - // join operations (which only allow exactly one of its inputs) - template - void followSingle(const IOGFinderCheckpoint &checkpoint, T options) { - size_t n = 0; - mlir::Value singleTaken = nullptr; - for (mlir::Value channel : options) { - if (checkpoint.partial.contains(channel)) { - n += 1; - singleTaken = channel; - } - } - if (n == 1) { - IOGFinderCheckpoint goHere = checkpoint; - // singleTaken is already part of the IOG, so no need to follow it - // goHere.follow(singleTaken); - for (mlir::Value other : options) { - if (other == singleTaken) { - continue; - } - goHere.makeIllegal(other); - } - partials.push_back(goHere); - return; - } - if (n > 1) { - // Multiple paths taken, but only single is allowed! => No IOGs from this - // branch - return; - } - for (mlir::Value channel : options) { - IOGFinderCheckpoint goHere = checkpoint; - goHere.follow(channel); - for (mlir::Value other : options) { - if (channel == other) - continue; - goHere.makeIllegal(other); - } - partials.push_back(goHere); - } +class IOGFinder { +public: + IOGFinder(mlir::Value entry) { + IOGCandidate cp(entry); + candidates.push_back(cp); } + ~IOGFinder() = default; // Take a step towards computing all IOGs. Does nothing if there are no // partial IOGs. // Example usage: // IOGFinder finder = ... - // while (!finder.partials.empty()) { + // while (!finder.isDone()) { // finder.step(); // } + // auto iogs = finder.getIOGs(); void step() { - if (partials.empty()) + if (candidates.empty()) return; - auto checkpoint = partials.back(); - partials.pop_back(); - if (checkpoint.progress == IOGFinderCheckpoint::PROGRESS::ILLEGAL) + auto candidate = std::move(candidates.back()); + candidates.pop_back(); + if (candidate.invalidIOG) return; - Operation *op = checkpoint.getNextOp(); - if (op == nullptr) { - if (checkpoint.progress == IOGFinderCheckpoint::PROGRESS::DONE) { - finals.push_back(checkpoint.partial); + std::optional optOp = candidate.getNextOpToAdd(); + if (optOp == std::nullopt) { + if (!candidate.invalidIOG) { + finals.push_back(candidate.iog); } return; } - checkpoint.partial.units.insert(op); + Operation *op = *optOp; + + candidate.iog.units.insert(op); if (auto endOp = dyn_cast(op)) { - followSingle(checkpoint, endOp.getOperands()); + followSingle(candidate, endOp.getOperands()); } else if (auto bufOp = dyn_cast(op)) { - checkpoint.follow(bufOp.getOperand()); - checkpoint.follow(bufOp.getResult()); - partials.push_back(checkpoint); + candidate.markFollowed(bufOp.getOperand()); + candidate.markFollowed(bufOp.getResult()); + candidates.push_back(candidate); } else if (auto condBr = dyn_cast(op)) { - checkpoint.follow(condBr.getTrueResult()); - checkpoint.follow(condBr.getFalseResult()); - followSingle(checkpoint, condBr.getOperands()); + candidate.markFollowed(condBr.getTrueResult()); + candidate.markFollowed(condBr.getFalseResult()); + followSingle(candidate, condBr.getOperands()); } else if (auto forkOp = dyn_cast(op)) { - checkpoint.follow(forkOp.getOperand()); - followSingle(checkpoint, forkOp.getResults()); + candidate.markFollowed(forkOp.getOperand()); + followSingle(candidate, forkOp.getResults()); } else if (auto muxOp = dyn_cast(op)) { // Either all data inputs, or the select input. Output always - checkpoint.follow(muxOp.getResult()); - auto dataFollower = checkpoint; - auto selectFollower = checkpoint; + candidate.markFollowed(muxOp.getResult()); + auto dataFollower = candidate; + auto selectFollower = candidate; for (auto data : muxOp.getDataOperands()) { - dataFollower.follow(data); - selectFollower.makeIllegal(data); + dataFollower.markFollowed(data); + selectFollower.markIllegal(data); } - dataFollower.makeIllegal(muxOp.getSelectOperand()); - selectFollower.follow(muxOp.getSelectOperand()); + dataFollower.markIllegal(muxOp.getSelectOperand()); + selectFollower.markFollowed(muxOp.getSelectOperand()); - partials.push_back(dataFollower); - partials.push_back(selectFollower); + candidates.push_back(dataFollower); + candidates.push_back(selectFollower); } else if (auto cmerge = dyn_cast(op)) { for (auto data : cmerge.getDataOperands()) { - checkpoint.follow(data); + candidate.markFollowed(data); } - followSingle(checkpoint, cmerge.getResults()); + followSingle(candidate, cmerge.getResults()); } else if (auto arithOp = dyn_cast(op)) { - checkpoint.follow(arithOp->getResults()[0]); - followSingle(checkpoint, arithOp->getOperands()); + candidate.markFollowed(arithOp->getResults()[0]); + followSingle(candidate, arithOp->getOperands()); } else if (auto sourceOp = dyn_cast(op)) { // SourceOps can not be part of an IOG, as they act like entry nodes. This // means that the partial IOGs looking at these operations can be // discarded, so nothing needs to be done } else if (isa(op)) { - partials.push_back(checkpoint); + candidates.push_back(candidate); } else if (auto loadOp = dyn_cast(op)) { - checkpoint.follow(loadOp.getAddress()); + candidate.markFollowed(loadOp.getAddress()); // checkpoint.follow(loadOp.getAddressResult()); // checkpoint.follow(loadOp.getData()); - checkpoint.follow(loadOp.getDataResult()); - partials.push_back(checkpoint); + candidate.markFollowed(loadOp.getDataResult()); + candidates.push_back(candidate); } else if (auto memCon = dyn_cast(op)) { // MemoryControllers are only accessed by control signals during this // annotation, as the edges between loadOps/storeOps and the MC are not @@ -633,16 +585,69 @@ struct IOGFinder { op->emitError("unhandled case in IOG finding"); } } + + inline bool isDone() { return candidates.empty(); } + + inline std::vector getIOGs() { + assert(isDone()); + return std::move(finals); + } + +private: + // This function takes a checkpoint and a list of channels. For each channel + // c, it pushes the IOG where *only* channel c is taken, and all the rest are + // illegal. Used for forks (which only allow exactly one of its outputs) and + // join operations (which only allow exactly one of its inputs) + template + void followSingle(const IOGCandidate &checkpoint, T options) { + size_t n = 0; + mlir::Value singleTaken = nullptr; + for (mlir::Value channel : options) { + if (checkpoint.iog.contains(channel)) { + n += 1; + singleTaken = channel; + } + } + if (n == 1) { + IOGCandidate goHere = checkpoint; + // singleTaken is already part of the IOG, so no need to follow it + // goHere.follow(singleTaken); + for (mlir::Value other : options) { + if (other == singleTaken) { + continue; + } + goHere.markIllegal(other); + } + candidates.push_back(goHere); + return; + } + if (n > 1) { + // Multiple paths taken, but only single is allowed! => No IOGs from this + // branch + return; + } + for (mlir::Value channel : options) { + IOGCandidate goHere = checkpoint; + goHere.markFollowed(channel); + for (mlir::Value other : options) { + if (channel == other) + continue; + goHere.markIllegal(other); + } + candidates.push_back(goHere); + } + } + + std::vector candidates; + std::vector finals; }; std::vector findAllIOGsWithEntry(mlir::Value entry) { - IOGFinder finder{}; - IOGFinderCheckpoint cp(entry); - finder.partials.push_back(cp); - while (!finder.partials.empty()) { + IOGFinder finder(entry); + while (!finder.isDone()) { finder.step(); } - return finder.finals; + return finder.getIOGs(); } std::vector findAllIOGs(ModuleOp modOp) { @@ -650,8 +655,8 @@ std::vector findAllIOGs(ModuleOp modOp) { for (handshake::FuncOp funcOp : modOp.getOps()) { // Each argument corresponds to an entry node. for (mlir::Value arg : funcOp.getRegion().getArguments()) { - for (auto &x : findAllIOGsWithEntry(arg)) { - ret.push_back(x); + for (auto &iog : findAllIOGsWithEntry(arg)) { + ret.push_back(std::move(iog)); } } } @@ -690,26 +695,6 @@ followPathAndGetCopiedSents(const IOGPath &path) { LogicalResult HandshakeAnnotatePropertiesPass::annotateIOGConsecutiveTokens(const IOG &iog) { - llvm::errs() << "performing IOG Consecutive tokens pass\n"; - llvm::errs() << "---------DEBUG----------\n"; - iog.debug(); - llvm::errs() << "---------UNITS----------\n"; - for (auto *op : iog.units) { - llvm::errs() << getUniqueName(op) << "\n"; - } - llvm::errs() << "---------CHANNELS-------\n"; - for (auto channel : iog.channels) { - Operation *before = channel.getDefiningOp(); - if (before == nullptr) { - llvm::errs() << "entry"; - } else { - llvm::errs() << getUniqueName(before); - } - Operation *after = channel.getUses().begin()->getOwner(); - assert(after); - llvm::errs() << " -> " << getUniqueName(after) << "\n"; - } - llvm::errs() << "------------------------\n"; std::vector slots; for (auto &op : iog.units) { if (auto slot = dyn_cast(op)) { @@ -741,7 +726,7 @@ HandshakeAnnotatePropertiesPass::annotateIOGConsecutiveTokens(const IOG &iog) { auto slot1Namer = slot1->getTokenCountNamer(); auto slot2Namer = slot2->getTokenCountNamer(); - auto p = IOGConsecutiveTokens(uid, FormalProperty::TAG::OPT, + auto p = IOGConsecutiveTokens(uid, FormalProperty::TAG::INVAR, std::move(slot1Namer), std::move(slot2Namer), copiedSents); uid++; @@ -756,12 +741,10 @@ HandshakeAnnotatePropertiesPass::annotateIOGConsecutiveTokens(const IOG &iog) { void HandshakeAnnotatePropertiesPass::runDynamaticPass() { ModuleOp modOp = getOperation(); -#if 0 if (failed(annotateAbsenceOfBackpressure(modOp))) return signalPassFailure(); if (failed(annotateValidEquivalence(modOp))) return signalPassFailure(); -#endif if (annotateInvariants) { if (failed(annotateEagerForkNotAllOutputSent(modOp))) return signalPassFailure(); From e7427252868f0cd8516717f95974ed0971a3bc7c Mon Sep 17 00:00:00 2001 From: Bas Niekel Date: Thu, 16 Apr 2026 17:27:25 +0200 Subject: [PATCH 05/29] extraction of IOG finding into separate file --- .../include/experimental/Support/IOG.h | 84 ++++ .../HandshakeAnnotateProperties.cpp | 386 +----------------- experimental/lib/Support/CMakeLists.txt | 1 + experimental/lib/Support/IOG.cpp | 321 +++++++++++++++ 4 files changed, 408 insertions(+), 384 deletions(-) create mode 100644 experimental/include/experimental/Support/IOG.h create mode 100644 experimental/lib/Support/IOG.cpp diff --git a/experimental/include/experimental/Support/IOG.h b/experimental/include/experimental/Support/IOG.h new file mode 100644 index 0000000000..0f3bcefe55 --- /dev/null +++ b/experimental/include/experimental/Support/IOG.h @@ -0,0 +1,84 @@ +#pragma once + +#include "dynamatic/Analysis/NameAnalysis.h" +#include "dynamatic/Support/LLVM.h" +#include "mlir/IR/Value.h" + +#include + +namespace dynamatic { +struct IOG; +struct IOGPath; + +struct IOGPath { + std::unordered_map prevSet; + std::unordered_map forwardSet; + Operation *from; + Operation *to; + IOGPath(const IOG &iog, Operation *from, Operation *to); + + void computeBackPath(const IOG &iog); + void computeForwardPathFromBackPath(); + + inline bool exists() const { return prevSet.find(to) != prevSet.end(); } + mlir::Value stepBack(Operation *cur) const { + auto iter = prevSet.find(cur); + assert(iter != prevSet.end()); + return iter->second; + } + mlir::Value stepForward(Operation *cur) const { + auto iter = forwardSet.find(cur); + assert(iter != forwardSet.end()); + return iter->second; + } +}; + +struct IOG { + IOG() = default; + std::unordered_set units; + llvm::DenseSet channels; + mlir::Value entry; + + inline bool contains(Operation *op) const { + auto iter = units.find(op); + return iter != units.end(); + } + + inline bool contains(mlir::Value channel) const { + auto iter = channels.find(channel); + return iter != channels.end(); + } + + void debug() const { + std::vector stack; + llvm::DenseSet visited; + stack.push_back(entry); + visited.insert(entry); + while (!stack.empty()) { + mlir::Value channel = stack.back(); + stack.pop_back(); + Operation *prev = channel.getDefiningOp(); + if (prev == nullptr) { + llvm::errs() << "entry"; + } else { + llvm::errs() << getUniqueName(prev); + } + Operation *next = channel.getUses().begin()->getOwner(); + assert(next); + assert(contains(next)); + llvm::errs() << " -> " << getUniqueName(next) << "\n"; + for (mlir::Value out : next->getResults()) { + if (auto iter = visited.find(out); iter != visited.end()) + continue; + if (contains(out)) { + visited.insert(out); + stack.push_back(out); + } + } + } + } +}; + +std::vector findAllIOGs(ModuleOp modOp); + +} // namespace dynamatic diff --git a/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp b/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp index 50550ab2c3..fec64a49c4 100644 --- a/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp +++ b/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp @@ -26,6 +26,7 @@ #include "dynamatic/Support/TimingModels.h" #include "dynamatic/Transforms/BufferPlacement/CFDFC.h" #include "experimental/Support/FormalProperty.h" +#include "experimental/Support/IOG.h" #include "mlir/IR/Value.h" #include "mlir/Pass/Pass.h" #include "mlir/Pass/PassManager.h" @@ -57,8 +58,6 @@ namespace experimental { // [END Boilerplate code for the MLIR pass] namespace { - -struct IOG; struct HandshakeAnnotatePropertiesPass : public dynamatic::experimental::impl::HandshakeAnnotatePropertiesBase< HandshakeAnnotatePropertiesPass> { @@ -283,386 +282,6 @@ HandshakeAnnotatePropertiesPass::annotateReconvergentPathFlow(ModuleOp modOp) { } namespace { -struct IOGPath { - std::unordered_map prevSet; - std::unordered_map forwardSet; - Operation *from; - Operation *to; - IOGPath(const IOG &iog, Operation *from, Operation *to); - - void computeBackPath(const IOG &iog); - void computeForwardPathFromBackPath(); - - bool exists() const { return prevSet.find(to) != prevSet.end(); } - mlir::Value stepBack(Operation *cur) const { - auto iter = prevSet.find(cur); - assert(iter != prevSet.end()); - return iter->second; - } - mlir::Value stepForward(Operation *cur) const { - auto iter = forwardSet.find(cur); - assert(iter != forwardSet.end()); - return iter->second; - } -}; - -struct IOG { - IOG() = default; - std::unordered_set units; - llvm::DenseSet channels; - mlir::Value entry; - - bool contains(Operation *op) const { - auto iter = units.find(op); - return iter != units.end(); - } - - bool contains(mlir::Value channel) const { - auto iter = channels.find(channel); - return iter != channels.end(); - } - - void debug() const { - std::vector stack; - llvm::DenseSet visited; - stack.push_back(entry); - visited.insert(entry); - while (!stack.empty()) { - mlir::Value channel = stack.back(); - stack.pop_back(); - Operation *prev = channel.getDefiningOp(); - if (prev == nullptr) { - llvm::errs() << "entry"; - } else { - llvm::errs() << getUniqueName(prev); - } - Operation *next = channel.getUses().begin()->getOwner(); - assert(next); - assert(contains(next)); - llvm::errs() << " -> " << getUniqueName(next) << "\n"; - for (mlir::Value out : next->getResults()) { - if (auto iter = visited.find(out); iter != visited.end()) - continue; - if (contains(out)) { - visited.insert(out); - stack.push_back(out); - } - } - } - } -}; - -IOGPath::IOGPath(const IOG &iog, Operation *fromArg, Operation *toArg) - : from(fromArg), to(toArg) { - assert(from && iog.contains(from)); - assert(to && iog.contains(to)); - computeBackPath(iog); - if (!exists()) { - return; - } - computeForwardPathFromBackPath(); -} - -void IOGPath::computeBackPath(const IOG &iog) { - std::vector stack; - for (mlir::Value out : from->getResults()) { - if (!iog.contains(out)) { - continue; - } - stack.push_back(out); - } - while (!stack.empty()) { - mlir::Value channel = stack.back(); - stack.pop_back(); - Operation *next = channel.getUses().begin()->getOwner(); - assert(next); - assert(iog.contains(next)); - if (prevSet.find(next) != prevSet.end()) { - continue; - } - prevSet.insert({next, channel}); - if (next == to) { - return; - } - - for (mlir::Value out : next->getResults()) { - if (!iog.contains(out)) { - // Only consider channels part of the IOG - continue; - } - stack.push_back(out); - } - } -} - -void IOGPath::computeForwardPathFromBackPath() { - assert(exists()); - Operation *cur = to; - while (cur != from) { - mlir::Value channel = stepBack(cur); - Operation *prev = channel.getDefiningOp(); - assert(prev); - forwardSet.insert({prev, channel}); - cur = prev; - } -} - -struct IOGCandidate { - IOG iog; - // Stack of channels at the edge that are not yet inserted into the IOG - std::vector dfsQueue; - // Set of channels that have been declared illegal by local rules - llvm::DenseSet illegalChannels; - - // Is the partial IOG contained within this struct invalid? I.e., is an - // illegal edge part of the IOG? - bool invalidIOG = false; - - IOGCandidate() = default; - IOGCandidate(mlir::Value entry) { - iog.entry = entry; - markFollowed(entry); - } - - bool isLegal(mlir::Value channel) { - auto iter = illegalChannels.find(channel); - return iter == illegalChannels.end(); - } - - void markFollowed(mlir::Value channel) { - if (!isLegal(channel)) { - // A non-legal channel has been followed, so mark this IOG as non-valid - invalidIOG = true; - return; - } - if (iog.contains(channel)) { - return; - } - dfsQueue.push_back(channel); - iog.channels.insert(channel); - } - - void markIllegal(mlir::Value channel) { - if (iog.contains(channel)) { - invalidIOG = true; - } - // The legality of unhandled channels is checked in getNextOp - illegalChannels.insert(channel); - } - - std::optional getNextOpToAdd() { - // Stop making progress if an illegal edge has been taken - if (invalidIOG) { - return std::nullopt; - } - - if (dfsQueue.empty()) { - // All handling done! - return std::nullopt; - } - - // Look at channel at the top of the `unhandled` stack - auto channel = dfsQueue.back(); - - // If this channel has been marked as illegal, abort this branch - if (!isLegal(channel)) { - invalidIOG = true; - return std::nullopt; - } - - // To fully handle a channel, both the operation before and after have to be - // handled - Operation *before = channel.getDefiningOp(); - if (before && !iog.contains(before)) { - iog.units.insert(before); - return before; - } - - Operation *after = channel.getUses().begin()->getOwner(); - if (after && !iog.contains(after)) { - iog.units.insert(after); - return after; - } - - // Both sides of this channel have been handled, so this channel is done and - // can be removed/inserted into the appropriate locations - dfsQueue.pop_back(); - - // Return next channel on unhandled stack - return getNextOpToAdd(); - } -}; - -class IOGFinder { -public: - IOGFinder(mlir::Value entry) { - IOGCandidate cp(entry); - candidates.push_back(cp); - } - ~IOGFinder() = default; - - // Take a step towards computing all IOGs. Does nothing if there are no - // partial IOGs. - // Example usage: - // IOGFinder finder = ... - // while (!finder.isDone()) { - // finder.step(); - // } - // auto iogs = finder.getIOGs(); - void step() { - if (candidates.empty()) - return; - auto candidate = std::move(candidates.back()); - candidates.pop_back(); - if (candidate.invalidIOG) - return; - - std::optional optOp = candidate.getNextOpToAdd(); - if (optOp == std::nullopt) { - if (!candidate.invalidIOG) { - finals.push_back(candidate.iog); - } - return; - } - Operation *op = *optOp; - - candidate.iog.units.insert(op); - - if (auto endOp = dyn_cast(op)) { - followSingle(candidate, endOp.getOperands()); - } else if (auto bufOp = dyn_cast(op)) { - candidate.markFollowed(bufOp.getOperand()); - candidate.markFollowed(bufOp.getResult()); - candidates.push_back(candidate); - } else if (auto condBr = dyn_cast(op)) { - candidate.markFollowed(condBr.getTrueResult()); - candidate.markFollowed(condBr.getFalseResult()); - followSingle(candidate, condBr.getOperands()); - } else if (auto forkOp = dyn_cast(op)) { - candidate.markFollowed(forkOp.getOperand()); - followSingle(candidate, forkOp.getResults()); - } else if (auto muxOp = dyn_cast(op)) { - // Either all data inputs, or the select input. Output always - candidate.markFollowed(muxOp.getResult()); - auto dataFollower = candidate; - auto selectFollower = candidate; - for (auto data : muxOp.getDataOperands()) { - dataFollower.markFollowed(data); - selectFollower.markIllegal(data); - } - - dataFollower.markIllegal(muxOp.getSelectOperand()); - selectFollower.markFollowed(muxOp.getSelectOperand()); - - candidates.push_back(dataFollower); - candidates.push_back(selectFollower); - } else if (auto cmerge = dyn_cast(op)) { - for (auto data : cmerge.getDataOperands()) { - candidate.markFollowed(data); - } - followSingle(candidate, cmerge.getResults()); - } else if (auto arithOp = dyn_cast(op)) { - candidate.markFollowed(arithOp->getResults()[0]); - followSingle(candidate, arithOp->getOperands()); - } else if (auto sourceOp = dyn_cast(op)) { - // SourceOps can not be part of an IOG, as they act like entry nodes. This - // means that the partial IOGs looking at these operations can be - // discarded, so nothing needs to be done - } else if (isa(op)) { - candidates.push_back(candidate); - } else if (auto loadOp = dyn_cast(op)) { - candidate.markFollowed(loadOp.getAddress()); - // checkpoint.follow(loadOp.getAddressResult()); - // checkpoint.follow(loadOp.getData()); - candidate.markFollowed(loadOp.getDataResult()); - candidates.push_back(candidate); - } else if (auto memCon = dyn_cast(op)) { - // MemoryControllers are only accessed by control signals during this - // annotation, as the edges between loadOps/storeOps and the MC are not - // added to the IOG. These control signals usually grant trivial IOGs that - // can be skipped. - } else { - op->emitError("unhandled case in IOG finding"); - } - } - - inline bool isDone() { return candidates.empty(); } - - inline std::vector getIOGs() { - assert(isDone()); - return std::move(finals); - } - -private: - // This function takes a checkpoint and a list of channels. For each channel - // c, it pushes the IOG where *only* channel c is taken, and all the rest are - // illegal. Used for forks (which only allow exactly one of its outputs) and - // join operations (which only allow exactly one of its inputs) - template - void followSingle(const IOGCandidate &checkpoint, T options) { - size_t n = 0; - mlir::Value singleTaken = nullptr; - for (mlir::Value channel : options) { - if (checkpoint.iog.contains(channel)) { - n += 1; - singleTaken = channel; - } - } - if (n == 1) { - IOGCandidate goHere = checkpoint; - // singleTaken is already part of the IOG, so no need to follow it - // goHere.follow(singleTaken); - for (mlir::Value other : options) { - if (other == singleTaken) { - continue; - } - goHere.markIllegal(other); - } - candidates.push_back(goHere); - return; - } - if (n > 1) { - // Multiple paths taken, but only single is allowed! => No IOGs from this - // branch - return; - } - for (mlir::Value channel : options) { - IOGCandidate goHere = checkpoint; - goHere.markFollowed(channel); - for (mlir::Value other : options) { - if (channel == other) - continue; - goHere.markIllegal(other); - } - candidates.push_back(goHere); - } - } - - std::vector candidates; - std::vector finals; -}; - -std::vector findAllIOGsWithEntry(mlir::Value entry) { - IOGFinder finder(entry); - while (!finder.isDone()) { - finder.step(); - } - return finder.getIOGs(); -} - -std::vector findAllIOGs(ModuleOp modOp) { - std::vector ret{}; - for (handshake::FuncOp funcOp : modOp.getOps()) { - // Each argument corresponds to an entry node. - for (mlir::Value arg : funcOp.getRegion().getArguments()) { - for (auto &iog : findAllIOGsWithEntry(arg)) { - ret.push_back(std::move(iog)); - } - } - } - return ret; -} - std::vector followPathAndGetCopiedSents(const IOGPath &path) { std::vector sents; @@ -692,6 +311,7 @@ followPathAndGetCopiedSents(const IOGPath &path) { } return sents; } +} // namespace LogicalResult HandshakeAnnotatePropertiesPass::annotateIOGConsecutiveTokens(const IOG &iog) { @@ -736,8 +356,6 @@ HandshakeAnnotatePropertiesPass::annotateIOGConsecutiveTokens(const IOG &iog) { return success(); } -} // namespace - void HandshakeAnnotatePropertiesPass::runDynamaticPass() { ModuleOp modOp = getOperation(); diff --git a/experimental/lib/Support/CMakeLists.txt b/experimental/lib/Support/CMakeLists.txt index ad8ea89455..5433a4a9f1 100644 --- a/experimental/lib/Support/CMakeLists.txt +++ b/experimental/lib/Support/CMakeLists.txt @@ -10,6 +10,7 @@ add_dynamatic_library(DynamaticExperimentalSupport CFGAnnotation.cpp FormalProperty.cpp FlowExpression.cpp + IOG.cpp LINK_LIBS PUBLIC MLIRIR diff --git a/experimental/lib/Support/IOG.cpp b/experimental/lib/Support/IOG.cpp new file mode 100644 index 0000000000..95db679bee --- /dev/null +++ b/experimental/lib/Support/IOG.cpp @@ -0,0 +1,321 @@ +#include "experimental/Support/IOG.h" +#include "dynamatic/Dialect/Handshake/HandshakeOps.h" +#include "mlir/IR/BuiltinOps.h" + +namespace dynamatic { +IOGPath::IOGPath(const IOG &iog, Operation *fromArg, Operation *toArg) + : from(fromArg), to(toArg) { + assert(from && iog.contains(from)); + assert(to && iog.contains(to)); + computeBackPath(iog); + if (!exists()) { + return; + } + computeForwardPathFromBackPath(); +} + +void IOGPath::computeBackPath(const IOG &iog) { + std::vector stack; + for (mlir::Value out : from->getResults()) { + if (!iog.contains(out)) { + continue; + } + stack.push_back(out); + } + while (!stack.empty()) { + mlir::Value channel = stack.back(); + stack.pop_back(); + Operation *next = channel.getUses().begin()->getOwner(); + assert(next); + assert(iog.contains(next)); + if (prevSet.find(next) != prevSet.end()) { + continue; + } + prevSet.insert({next, channel}); + if (next == to) { + return; + } + + for (mlir::Value out : next->getResults()) { + if (!iog.contains(out)) { + // Only consider channels part of the IOG + continue; + } + stack.push_back(out); + } + } +} + +void IOGPath::computeForwardPathFromBackPath() { + assert(exists()); + Operation *cur = to; + while (cur != from) { + mlir::Value channel = stepBack(cur); + Operation *prev = channel.getDefiningOp(); + assert(prev); + forwardSet.insert({prev, channel}); + cur = prev; + } +} + +namespace { +struct IOGCandidate { + IOG iog; + // Stack of channels at the edge that are not yet inserted into the IOG + std::vector dfsQueue; + // Set of channels that have been declared illegal by local rules + llvm::DenseSet illegalChannels; + + // Is the partial IOG contained within this struct invalid? I.e., is an + // illegal edge part of the IOG? + bool invalidIOG = false; + + IOGCandidate() = default; + IOGCandidate(mlir::Value entry) { + iog.entry = entry; + markFollowed(entry); + } + + bool isLegal(mlir::Value channel) { + auto iter = illegalChannels.find(channel); + return iter == illegalChannels.end(); + } + + void markFollowed(mlir::Value channel) { + if (!isLegal(channel)) { + // A non-legal channel has been followed, so mark this IOG as non-valid + invalidIOG = true; + return; + } + if (iog.contains(channel)) { + return; + } + dfsQueue.push_back(channel); + iog.channels.insert(channel); + } + + void markIllegal(mlir::Value channel) { + if (iog.contains(channel)) { + invalidIOG = true; + } + // The legality of unhandled channels is checked in getNextOp + illegalChannels.insert(channel); + } + + std::optional getNextOpToAdd() { + // Stop making progress if an illegal edge has been taken + if (invalidIOG) { + return std::nullopt; + } + + if (dfsQueue.empty()) { + // All handling done! + return std::nullopt; + } + + // Look at channel at the top of the `unhandled` stack + auto channel = dfsQueue.back(); + + // If this channel has been marked as illegal, abort this branch + if (!isLegal(channel)) { + invalidIOG = true; + return std::nullopt; + } + + // To fully handle a channel, both the operation before and after have to be + // handled + Operation *before = channel.getDefiningOp(); + if (before && !iog.contains(before)) { + iog.units.insert(before); + return before; + } + + Operation *after = channel.getUses().begin()->getOwner(); + if (after && !iog.contains(after)) { + iog.units.insert(after); + return after; + } + + // Both sides of this channel have been handled, so this channel is done and + // can be removed/inserted into the appropriate locations + dfsQueue.pop_back(); + + // Return next channel on unhandled stack + return getNextOpToAdd(); + } +}; + +using namespace dynamatic::handshake; +class IOGFinder { +public: + IOGFinder(mlir::Value entry) { + IOGCandidate cp(entry); + candidates.push_back(cp); + } + ~IOGFinder() = default; + + // Take a step towards computing all IOGs. Does nothing if there are no + // partial IOGs. + // Example usage: + // IOGFinder finder = ... + // while (!finder.isDone()) { + // finder.step(); + // } + // auto iogs = finder.getIOGs(); + void step() { + if (candidates.empty()) + return; + auto candidate = std::move(candidates.back()); + candidates.pop_back(); + if (candidate.invalidIOG) + return; + + std::optional optOp = candidate.getNextOpToAdd(); + if (optOp == std::nullopt) { + if (!candidate.invalidIOG) { + finals.push_back(candidate.iog); + } + return; + } + Operation *op = *optOp; + + candidate.iog.units.insert(op); + + if (auto endOp = dyn_cast(op)) { + followSingle(candidate, endOp.getOperands()); + } else if (auto bufOp = dyn_cast(op)) { + candidate.markFollowed(bufOp.getOperand()); + candidate.markFollowed(bufOp.getResult()); + candidates.push_back(candidate); + } else if (auto condBr = dyn_cast(op)) { + candidate.markFollowed(condBr.getTrueResult()); + candidate.markFollowed(condBr.getFalseResult()); + followSingle(candidate, condBr.getOperands()); + } else if (auto forkOp = dyn_cast(op)) { + candidate.markFollowed(forkOp.getOperand()); + followSingle(candidate, forkOp.getResults()); + } else if (auto muxOp = dyn_cast(op)) { + // Either all data inputs, or the select input. Output always + candidate.markFollowed(muxOp.getResult()); + auto dataFollower = candidate; + auto selectFollower = candidate; + for (auto data : muxOp.getDataOperands()) { + dataFollower.markFollowed(data); + selectFollower.markIllegal(data); + } + + dataFollower.markIllegal(muxOp.getSelectOperand()); + selectFollower.markFollowed(muxOp.getSelectOperand()); + + candidates.push_back(dataFollower); + candidates.push_back(selectFollower); + } else if (auto cmerge = dyn_cast(op)) { + for (auto data : cmerge.getDataOperands()) { + candidate.markFollowed(data); + } + followSingle(candidate, cmerge.getResults()); + } else if (auto arithOp = dyn_cast(op)) { + candidate.markFollowed(arithOp->getResults()[0]); + followSingle(candidate, arithOp->getOperands()); + } else if (auto sourceOp = dyn_cast(op)) { + // SourceOps can not be part of an IOG, as they act like entry nodes. This + // means that the partial IOGs looking at these operations can be + // discarded, so nothing needs to be done + } else if (isa(op)) { + candidates.push_back(candidate); + } else if (auto loadOp = dyn_cast(op)) { + candidate.markFollowed(loadOp.getAddress()); + // checkpoint.follow(loadOp.getAddressResult()); + // checkpoint.follow(loadOp.getData()); + candidate.markFollowed(loadOp.getDataResult()); + candidates.push_back(candidate); + } else if (auto memCon = dyn_cast(op)) { + // MemoryControllers are only accessed by control signals during this + // annotation, as the edges between loadOps/storeOps and the MC are not + // added to the IOG. These control signals usually grant trivial IOGs that + // can be skipped. + } else { + op->emitError("unhandled case in IOG finding"); + } + } + + inline bool isDone() { return candidates.empty(); } + + inline std::vector getIOGs() { + assert(isDone()); + return std::move(finals); + } + +private: + // This function takes a checkpoint and a list of channels. For each channel + // c, it pushes the IOG where *only* channel c is taken, and all the rest are + // illegal. Used for forks (which only allow exactly one of its outputs) and + // join operations (which only allow exactly one of its inputs) + template + void followSingle(const IOGCandidate &checkpoint, T options) { + size_t n = 0; + mlir::Value singleTaken = nullptr; + for (mlir::Value channel : options) { + if (checkpoint.iog.contains(channel)) { + n += 1; + singleTaken = channel; + } + } + if (n == 1) { + IOGCandidate goHere = checkpoint; + // singleTaken is already part of the IOG, so no need to follow it + // goHere.follow(singleTaken); + for (mlir::Value other : options) { + if (other == singleTaken) { + continue; + } + goHere.markIllegal(other); + } + candidates.push_back(goHere); + return; + } + if (n > 1) { + // Multiple paths taken, but only single is allowed! => No IOGs from this + // branch + return; + } + for (mlir::Value channel : options) { + IOGCandidate goHere = checkpoint; + goHere.markFollowed(channel); + for (mlir::Value other : options) { + if (channel == other) + continue; + goHere.markIllegal(other); + } + candidates.push_back(goHere); + } + } + + std::vector candidates; + std::vector finals; +}; + +std::vector findAllIOGsWithEntry(mlir::Value entry) { + IOGFinder finder(entry); + while (!finder.isDone()) { + finder.step(); + } + return finder.getIOGs(); +} + +} // namespace + +std::vector findAllIOGs(ModuleOp modOp) { + std::vector ret{}; + for (handshake::FuncOp funcOp : modOp.getOps()) { + // Each argument corresponds to an entry node. + for (mlir::Value arg : funcOp.getRegion().getArguments()) { + for (auto &iog : findAllIOGsWithEntry(arg)) { + ret.push_back(std::move(iog)); + } + } + } + return ret; +} + +} // namespace dynamatic From b9f632b05268225fb7ecc8f8fda64ccefc95bd0b Mon Sep 17 00:00:00 2001 From: Bas Niekel Date: Thu, 16 Apr 2026 19:01:24 +0200 Subject: [PATCH 06/29] fixed IOG path code to support multiple possible paths --- .../include/experimental/Support/IOG.h | 37 ++++---- .../HandshakeAnnotateProperties.cpp | 65 +++++++------- experimental/lib/Support/IOG.cpp | 85 +++++++++++-------- 3 files changed, 98 insertions(+), 89 deletions(-) diff --git a/experimental/include/experimental/Support/IOG.h b/experimental/include/experimental/Support/IOG.h index 0f3bcefe55..c83d5ba20f 100644 --- a/experimental/include/experimental/Support/IOG.h +++ b/experimental/include/experimental/Support/IOG.h @@ -3,34 +3,27 @@ #include "dynamatic/Analysis/NameAnalysis.h" #include "dynamatic/Support/LLVM.h" #include "mlir/IR/Value.h" - #include +// An In-order graph (IOG) of a dataflow circuit is a subgraph of the dataflow +// circuit. It contains one and only one entry channel (i.e. an argument of a +// FuncOp) which can reach all other operations using only channels part of the +// IOG. The IOG does not lose or gain any tokens: For any merge/mux, all the +// data inputs must be contained in the IOG, and for any fork, only a single +// output can be part of the IOG. Similarly, all branch outputs are part of the +// IOG, and for each join-operation, only a single input is part of the IOG. +// This way, there is a fixed number of tokens within the IOG. + namespace dynamatic { struct IOG; -struct IOGPath; - -struct IOGPath { - std::unordered_map prevSet; - std::unordered_map forwardSet; - Operation *from; - Operation *to; - IOGPath(const IOG &iog, Operation *from, Operation *to); +struct IOGPathSet; - void computeBackPath(const IOG &iog); - void computeForwardPathFromBackPath(); +struct IOGPathSet { + IOGPathSet(const IOG &iog, Operation *start, Operation *end); - inline bool exists() const { return prevSet.find(to) != prevSet.end(); } - mlir::Value stepBack(Operation *cur) const { - auto iter = prevSet.find(cur); - assert(iter != prevSet.end()); - return iter->second; - } - mlir::Value stepForward(Operation *cur) const { - auto iter = forwardSet.find(cur); - assert(iter != forwardSet.end()); - return iter->second; - } + std::unordered_set units; + Operation *start; + Operation *end; }; struct IOG { diff --git a/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp b/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp index fec64a49c4..dc8311d924 100644 --- a/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp +++ b/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp @@ -282,32 +282,38 @@ HandshakeAnnotatePropertiesPass::annotateReconvergentPathFlow(ModuleOp modOp) { } namespace { -std::vector -followPathAndGetCopiedSents(const IOGPath &path) { +std::vector findCopiedSents(const IOG &iog, + const IOGPathSet &pathSet) { std::vector sents; - Operation *cur = path.from; + std::vector stack; + stack.push_back(pathSet.start); bool first = true; - while (cur != path.to) { + while (!stack.empty()) { + Operation *cur = stack.back(); + stack.pop_back(); if (!first) { if (auto slot = dyn_cast(cur)) { return sents; } } first = false; - mlir::Value forward = path.stepForward(cur); - if (auto sent = dyn_cast(cur)) { - // FORK DETECTED!! - size_t index; - // inconvenient way of getting the correct sent namer, but there is no - // better way for now - for (auto [i, channel] : llvm::enumerate(sent->getResults())) { - if (channel == forward) { - index = i; - } + for (OpResult forward : cur->getResults()) { + if (!iog.contains(forward)) { + continue; + } + Operation *next = forward.getUses().begin()->getOwner(); + assert(iog.contains(next)); + if (pathSet.units.find(next) == pathSet.units.end()) { + continue; + } + + if (auto forkOp = dyn_cast(cur)) { + sents.push_back( + forkOp.getInternalSentStateNamers()[forward.getResultNumber()]); } - sents.push_back(sent.getInternalSentStateNamers()[index]); + + stack.push_back(next); } - cur = forward.getUses().begin()->getOwner(); } return sents; } @@ -326,27 +332,24 @@ HandshakeAnnotatePropertiesPass::annotateIOGConsecutiveTokens(const IOG &iog) { if (slot1->getOperation() == slot2->getOperation()) { continue; } - std::vector copiedSents; - IOGPath path = IOGPath(iog, *slot1, *slot2); - if (path.exists()) { - std::vector extras = - followPathAndGetCopiedSents(path); - copiedSents.insert(copiedSents.end(), extras.begin(), extras.end()); - } - path = IOGPath(iog, *slot2, *slot1); - if (path.exists()) { - std::vector extras = - followPathAndGetCopiedSents(path); - copiedSents.insert(copiedSents.end(), extras.begin(), extras.end()); - } + IOGPathSet pathSet12(iog, *slot1, *slot2); + + std::vector copiedSents = + findCopiedSents(iog, pathSet12); + + IOGPathSet pathSet21(iog, *slot2, *slot1); + std::vector extra = findCopiedSents(iog, pathSet21); + copiedSents.insert(copiedSents.end(), extra.begin(), extra.end()); + + // Note: // Even if the copiedSents is empty, this invariant is interesting! It // means that both slots cannot be occupied at the same time, as there is // only (at most) one token in the IOG auto slot1Namer = slot1->getTokenCountNamer(); auto slot2Namer = slot2->getTokenCountNamer(); - auto p = IOGConsecutiveTokens(uid, FormalProperty::TAG::INVAR, + auto p = IOGConsecutiveTokens(uid, FormalProperty::TAG::OPT, std::move(slot1Namer), std::move(slot2Namer), copiedSents); uid++; @@ -359,10 +362,12 @@ HandshakeAnnotatePropertiesPass::annotateIOGConsecutiveTokens(const IOG &iog) { void HandshakeAnnotatePropertiesPass::runDynamaticPass() { ModuleOp modOp = getOperation(); +#if 0 if (failed(annotateAbsenceOfBackpressure(modOp))) return signalPassFailure(); if (failed(annotateValidEquivalence(modOp))) return signalPassFailure(); +#endif if (annotateInvariants) { if (failed(annotateEagerForkNotAllOutputSent(modOp))) return signalPassFailure(); diff --git a/experimental/lib/Support/IOG.cpp b/experimental/lib/Support/IOG.cpp index 95db679bee..7a9f08235b 100644 --- a/experimental/lib/Support/IOG.cpp +++ b/experimental/lib/Support/IOG.cpp @@ -3,58 +3,69 @@ #include "mlir/IR/BuiltinOps.h" namespace dynamatic { -IOGPath::IOGPath(const IOG &iog, Operation *fromArg, Operation *toArg) - : from(fromArg), to(toArg) { - assert(from && iog.contains(from)); - assert(to && iog.contains(to)); - computeBackPath(iog); - if (!exists()) { - return; - } - computeForwardPathFromBackPath(); -} +IOGPathSet::IOGPathSet(const IOG &iog, Operation *startA, Operation *endA) + : start(startA), end(endA) { + std::vector stack; + stack.push_back(start); + std::unordered_set forward; + while (!stack.empty()) { + Operation *op = stack.back(); + stack.pop_back(); + + if (forward.find(op) != forward.end()) { + continue; + } + + forward.insert(op); -void IOGPath::computeBackPath(const IOG &iog) { - std::vector stack; - for (mlir::Value out : from->getResults()) { - if (!iog.contains(out)) { + if (op == end) { continue; } - stack.push_back(out); + + for (auto channel : op->getResults()) { + if (!iog.contains(channel)) { + continue; + } + Operation *next = channel.getUses().begin()->getOwner(); + assert(iog.contains(next)); + stack.push_back(next); + } } + + stack.push_back(end); + std::unordered_set back; + while (!stack.empty()) { - mlir::Value channel = stack.back(); + Operation *op = stack.back(); stack.pop_back(); - Operation *next = channel.getUses().begin()->getOwner(); - assert(next); - assert(iog.contains(next)); - if (prevSet.find(next) != prevSet.end()) { + + if (back.find(op) != back.end()) { continue; } - prevSet.insert({next, channel}); - if (next == to) { - return; + + back.insert(op); + + if (op == start) { + continue; } - for (mlir::Value out : next->getResults()) { - if (!iog.contains(out)) { - // Only consider channels part of the IOG + for (auto channel : op->getOperands()) { + if (!iog.contains(channel)) { + continue; + } + Operation *next = channel.getDefiningOp(); + if (next == nullptr) { continue; } - stack.push_back(out); + assert(iog.contains(next)); + stack.push_back(next); } } -} -void IOGPath::computeForwardPathFromBackPath() { - assert(exists()); - Operation *cur = to; - while (cur != from) { - mlir::Value channel = stepBack(cur); - Operation *prev = channel.getDefiningOp(); - assert(prev); - forwardSet.insert({prev, channel}); - cur = prev; + for (Operation *op : forward) { + if (back.find(op) != back.end()) { + units.insert(op); + } } } From 3c64778fe9c0ece3e1846c5887ac896660dca595 Mon Sep 17 00:00:00 2001 From: Bas Niekel Date: Fri, 17 Apr 2026 13:54:57 +0200 Subject: [PATCH 07/29] handle pipeline slots as well as normal slots in invariant 6 --- .../experimental/Support/FormalProperty.h | 8 +-- .../HandshakeAnnotateProperties.cpp | 33 ++++++------ experimental/lib/Support/FormalProperty.cpp | 4 +- .../smv/generators/support/delay_buffer.py | 1 + .../Dialect/Handshake/HandshakeInterfaces.td | 12 ----- .../Handshake/HandshakeOpInternalStateNamer.h | 40 +++++++++++++- .../HandshakeOpInternalStateNamer.cpp | 54 +++++++++++++++++++ 7 files changed, 117 insertions(+), 35 deletions(-) diff --git a/experimental/include/experimental/Support/FormalProperty.h b/experimental/include/experimental/Support/FormalProperty.h index 784c01e7f4..34da8e6d2d 100644 --- a/experimental/include/experimental/Support/FormalProperty.h +++ b/experimental/include/experimental/Support/FormalProperty.h @@ -295,8 +295,8 @@ class IOGConsecutiveTokens : public FormalProperty { IOGConsecutiveTokens() = default; IOGConsecutiveTokens(unsigned long id, TAG tag, - std::unique_ptr slot1, - std::unique_ptr slot2, + std::shared_ptr slot1, + std::shared_ptr slot2, std::vector sents); ~IOGConsecutiveTokens() = default; @@ -304,8 +304,8 @@ class IOGConsecutiveTokens : public FormalProperty { return fp->getType() == TYPE::IOGConsecutiveTokens; } - std::unique_ptr slot1; - std::unique_ptr slot2; + std::shared_ptr slot1; + std::shared_ptr slot2; std::vector sents; private: diff --git a/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp b/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp index dc8311d924..b9d0e34377 100644 --- a/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp +++ b/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp @@ -292,7 +292,8 @@ std::vector findCopiedSents(const IOG &iog, Operation *cur = stack.back(); stack.pop_back(); if (!first) { - if (auto slot = dyn_cast(cur)) { + auto slots = getAllSlotsOfOperation(cur); + if (!slots.empty()) { return sents; } } @@ -321,24 +322,29 @@ std::vector findCopiedSents(const IOG &iog, LogicalResult HandshakeAnnotatePropertiesPass::annotateIOGConsecutiveTokens(const IOG &iog) { - std::vector slots; + std::vector>> + slotOps; for (auto &op : iog.units) { - if (auto slot = dyn_cast(op)) { - slots.push_back(slot); + auto slotCountNamer = getTokenCountNamerOfOperation(op); + if (slotCountNamer.has_value()) { + assert(*slotCountNamer); + slotOps.push_back({op, std::move(*slotCountNamer)}); } } - for (auto slot1 = slots.begin(); slot1 != slots.end(); ++slot1) { - for (auto slot2 = slot1 + 1; slot2 != slots.end(); ++slot2) { - if (slot1->getOperation() == slot2->getOperation()) { + for (auto slot1 = slotOps.begin(); slot1 != slotOps.end(); ++slot1) { + for (auto slot2 = slot1 + 1; slot2 != slotOps.end(); ++slot2) { + if (slot1 == slot2) { + // TODO: Handle loops, i.e. if the slot contains >=2 tokens, there + // should be a copied fork within a loop continue; } - IOGPathSet pathSet12(iog, *slot1, *slot2); + IOGPathSet pathSet12(iog, slot1->first, slot2->first); std::vector copiedSents = findCopiedSents(iog, pathSet12); - IOGPathSet pathSet21(iog, *slot2, *slot1); + IOGPathSet pathSet21(iog, slot2->first, slot1->first); std::vector extra = findCopiedSents(iog, pathSet21); copiedSents.insert(copiedSents.end(), extra.begin(), extra.end()); @@ -347,11 +353,8 @@ HandshakeAnnotatePropertiesPass::annotateIOGConsecutiveTokens(const IOG &iog) { // means that both slots cannot be occupied at the same time, as there is // only (at most) one token in the IOG - auto slot1Namer = slot1->getTokenCountNamer(); - auto slot2Namer = slot2->getTokenCountNamer(); - auto p = IOGConsecutiveTokens(uid, FormalProperty::TAG::OPT, - std::move(slot1Namer), - std::move(slot2Namer), copiedSents); + auto p = IOGConsecutiveTokens(uid, FormalProperty::TAG::INVAR, + slot1->second, slot2->second, copiedSents); uid++; propertyTable.push_back(p.toJSON()); } @@ -362,12 +365,10 @@ HandshakeAnnotatePropertiesPass::annotateIOGConsecutiveTokens(const IOG &iog) { void HandshakeAnnotatePropertiesPass::runDynamaticPass() { ModuleOp modOp = getOperation(); -#if 0 if (failed(annotateAbsenceOfBackpressure(modOp))) return signalPassFailure(); if (failed(annotateValidEquivalence(modOp))) return signalPassFailure(); -#endif if (annotateInvariants) { if (failed(annotateEagerForkNotAllOutputSent(modOp))) return signalPassFailure(); diff --git a/experimental/lib/Support/FormalProperty.cpp b/experimental/lib/Support/FormalProperty.cpp index 5f3f84a0a2..ccf02da2b0 100644 --- a/experimental/lib/Support/FormalProperty.cpp +++ b/experimental/lib/Support/FormalProperty.cpp @@ -456,8 +456,8 @@ IOGConsecutiveTokens::fromJSON(const llvm::json::Value &value, } IOGConsecutiveTokens::IOGConsecutiveTokens( - unsigned long id, TAG tag, std::unique_ptr slot1, - std::unique_ptr slot2, + unsigned long id, TAG tag, std::shared_ptr slot1, + std::shared_ptr slot2, std::vector sents) : FormalProperty(id, tag, TYPE::IOGConsecutiveTokens), slot1(std::move(slot1)), slot2(std::move(slot2)), diff --git a/experimental/tools/unit-generators/smv/generators/support/delay_buffer.py b/experimental/tools/unit-generators/smv/generators/support/delay_buffer.py index bc54ed4cec..e25f258328 100644 --- a/experimental/tools/unit-generators/smv/generators/support/delay_buffer.py +++ b/experimental/tools/unit-generators/smv/generators/support/delay_buffer.py @@ -54,6 +54,7 @@ def _generate_delay_buffer(name, latency): DEFINE ins_ready := inner_one_slot_break_dv.ins_ready; DEFINE outs_valid := inner_one_slot_break_dv.outs_valid; DEFINE v{no_one_slot_break_dv_latency} := inner_one_slot_break_dv.slot_0_full; + DEFINE pipeline_token_count := count({", ".join([f"v{n}" for n in range(latency)])}); {generate_one_slot_break_dv(f"{name}__one_slot_break_dv_dataless", {ATTR_BITWIDTH: 0})} """ diff --git a/include/dynamatic/Dialect/Handshake/HandshakeInterfaces.td b/include/dynamatic/Dialect/Handshake/HandshakeInterfaces.td index 9bfdae62ea..80ba20f0b4 100644 --- a/include/dynamatic/Dialect/Handshake/HandshakeInterfaces.td +++ b/include/dynamatic/Dialect/Handshake/HandshakeInterfaces.td @@ -72,18 +72,6 @@ def BufferLikeOpInterface : OpInterface<"BufferLikeOpInterface"> { }], "std::vector", "getInternalSlotStateNamers", (ins) >, - InterfaceMethod<[{ - Get the internal state namer of the number of tokens currently - contained within this operation. - }], - "std::unique_ptr", "getTokenCountNamer", (ins), [{ - Operation *op = $_op.getOperation(); - auto name = op->getAttrOfType<::mlir::StringAttr>(NameAnalysis::ATTR_NAME); - if (!name) - return nullptr; - return std::make_unique(name.str()); - }] - >, ]; } diff --git a/include/dynamatic/Dialect/Handshake/HandshakeOpInternalStateNamer.h b/include/dynamatic/Dialect/Handshake/HandshakeOpInternalStateNamer.h index 9ced03aa9b..4ed859b092 100644 --- a/include/dynamatic/Dialect/Handshake/HandshakeOpInternalStateNamer.h +++ b/include/dynamatic/Dialect/Handshake/HandshakeOpInternalStateNamer.h @@ -11,12 +11,19 @@ namespace handshake { struct InternalStateNamer; struct EagerForkSentNamer; struct BufferSlotFullNamer; +struct TokenCountNamer; struct PipelineSlotNamer; +struct PipelineTokenCountNamer; struct ConstrainedNamer; struct ConstrainedEagerForkSentNamer; struct ConstrainedBufferSlotFullNamer; struct MemoryControllerSlotNamer; +std::vector> +getAllSlotsOfOperation(Operation *op); +std::optional> +getTokenCountNamerOfOperation(Operation *op); + // A general structure for an operation is assumed: // in1, in2, ... -> Join/Merge/Mux // -> Pipeline Slots @@ -29,10 +36,11 @@ struct InternalStateNamer { enum class TYPE { EagerForkSent, BufferSlotFull, + TokenCount, PipelineSlot, + PipelineTokenCount, Constrained, MemoryControllerSlot, - TokenCount, }; static std::optional typeFromStr(const std::string &s); static std::string typeToStr(TYPE t); @@ -76,6 +84,8 @@ struct InternalStateNamer { static constexpr llvm::StringLiteral MEMORY_CONTROLLER_SLOT = "MemoryControllerSlot"; static constexpr llvm::StringLiteral TOKEN_COUNT = "TokenCount"; + static constexpr llvm::StringLiteral PIPELINE_TOKEN_COUNT = + "PipelineTokenCount"; static constexpr llvm::StringLiteral INNER_LIT = "inner"; }; @@ -287,6 +297,33 @@ struct PipelineSlotNamer : InternalStateNamer { static constexpr llvm::StringLiteral SLOT_INDEX_LIT = "pipeline_index"; }; +struct PipelineTokenCountNamer : InternalStateNamer { + PipelineTokenCountNamer() = default; + PipelineTokenCountNamer(const std::string &opName) + : InternalStateNamer(TYPE::PipelineTokenCount), opName(opName) {} + ~PipelineTokenCountNamer() = default; + + static inline bool classof(const InternalStateNamer *fp) { + return fp->type == TYPE::PipelineTokenCount; + } + + inline std::string getSMVName() const override { + return llvm::formatv( + "{0}.inner_handshake_manager.inner_delay_buffer.pipeline_token_count", + opName); + } + + inline llvm::json::Value toInnerJSON() const override { + return llvm::json::Object({{OPERATION_LIT, opName}}); + } + + std::unique_ptr static fromInnerJSON( + const llvm::json::Value &value, llvm::json::Path path); + std::string opName; + + static constexpr llvm::StringLiteral OPERATION_LIT = "operation"; +}; + struct TokenCountNamer : InternalStateNamer { TokenCountNamer() = default; TokenCountNamer(const std::string &opName) @@ -360,6 +397,7 @@ struct MemoryControllerSlotNamer : InternalStateNamer { static constexpr llvm::StringLiteral PORT_TYPE_LIT = "port_type"; static constexpr llvm::StringLiteral LOADLESS_LIT = "loadless"; }; + } // namespace handshake } // namespace dynamatic diff --git a/lib/Dialect/Handshake/HandshakeOpInternalStateNamer.cpp b/lib/Dialect/Handshake/HandshakeOpInternalStateNamer.cpp index 406ca44b10..b96e277f5b 100644 --- a/lib/Dialect/Handshake/HandshakeOpInternalStateNamer.cpp +++ b/lib/Dialect/Handshake/HandshakeOpInternalStateNamer.cpp @@ -1,4 +1,5 @@ #include "dynamatic/Dialect/Handshake/HandshakeOpInternalStateNamer.h" +#include "dynamatic/Dialect/Handshake/HandshakeInterfaces.h" namespace dynamatic { namespace handshake { @@ -16,6 +17,8 @@ InternalStateNamer::typeFromStr(const std::string &s) { return TYPE::MemoryControllerSlot; if (s == TOKEN_COUNT) return TYPE::TokenCount; + if (s == PIPELINE_TOKEN_COUNT) + return TYPE::PipelineTokenCount; llvm::errs() << "unknown type\n"; return std::nullopt; } @@ -34,6 +37,8 @@ std::string InternalStateNamer::typeToStr(TYPE t) { return MEMORY_CONTROLLER_SLOT.str(); case TYPE::TokenCount: return TOKEN_COUNT.str(); + case TYPE::PipelineTokenCount: + return PIPELINE_TOKEN_COUNT.str(); } } @@ -76,6 +81,10 @@ InternalStateNamer::fromJSON(const llvm::json::Value &value, prop = TokenCountNamer::fromInnerJSON(inner, path); assert(prop && "inner token count failed"); break; + case TYPE::PipelineTokenCount: + prop = PipelineTokenCountNamer::fromInnerJSON(inner, path); + assert(prop && "pipeline token count failed"); + break; case TYPE::MemoryControllerSlot: prop = MemoryControllerSlotNamer::fromInnerJSON(inner, path); assert(prop && "mc slot failed"); @@ -146,6 +155,16 @@ PipelineSlotNamer::fromInnerJSON(const llvm::json::Value &value, return prop; } +std::unique_ptr +PipelineTokenCountNamer::fromInnerJSON(const llvm::json::Value &value, + llvm::json::Path path) { + llvm::json::ObjectMapper mapper(value, path); + auto prop = std::make_unique(); + if (!mapper || !mapper.map(OPERATION_LIT, prop->opName)) + return nullptr; + return prop; +} + std::unique_ptr TokenCountNamer::fromInnerJSON(const llvm::json::Value &value, llvm::json::Path path) { @@ -188,5 +207,40 @@ MemoryControllerSlotNamer::fromInnerJSON(const llvm::json::Value &value, return prop; } +std::vector> +getAllSlotsOfOperation(Operation *op) { + std::vector> ret; + if (auto latencyOp = dyn_cast(op)) { + auto slots = latencyOp.getPipelineSlots(); + for (auto &slot : slots) { + ret.push_back(std::make_unique(slot)); + } + } + if (auto bufferOp = dyn_cast(op)) { + auto slots = bufferOp.getInternalSlotStateNamers(); + for (auto &slot : slots) { + ret.push_back(std::make_unique(slot)); + } + } + return ret; +} + +std::optional> +getTokenCountNamerOfOperation(Operation *op) { + if (isa(op) && isa(op)) { + assert(false && + "cannot handle token count of operations with latency and slots"); + return std::nullopt; + } + + if (auto latencyOp = dyn_cast(op)) { + return std::make_unique(getUniqueName(op).str()); + } + if (auto bufferOp = dyn_cast(op)) { + return std::make_unique(getUniqueName(op).str()); + } + return std::nullopt; +} + } // namespace handshake } // namespace dynamatic From b4e5fd457a3d227319b529bc7fcae1d4960da670 Mon Sep 17 00:00:00 2001 From: Bas Niekel Date: Wed, 22 Apr 2026 13:23:09 +0200 Subject: [PATCH 08/29] added some more explaining comments for the IOG finding algorithm --- experimental/lib/Support/IOG.cpp | 40 +++++++++++++++++++++++++++----- 1 file changed, 34 insertions(+), 6 deletions(-) diff --git a/experimental/lib/Support/IOG.cpp b/experimental/lib/Support/IOG.cpp index 7a9f08235b..a4121f2933 100644 --- a/experimental/lib/Support/IOG.cpp +++ b/experimental/lib/Support/IOG.cpp @@ -113,6 +113,15 @@ struct IOGCandidate { illegalChannels.insert(channel); } + // Get an operation that needs to be added to the IOG: + // OP_BEFORE ---channel--> OP_AFTER + // 1. Pop an edge from the unhandled edges stack + // 2. Check if OP_BEFORE has been handled already. If not, return it for + // handling + // 3. Check if OP_AFTER has been handled already. If not, return it for + // handling + // 4. Both sides of this edge have been added, so mark this edge as done and + // repeat for the next edge on the stack std::optional getNextOpToAdd() { // Stop making progress if an illegal edge has been taken if (invalidIOG) { @@ -173,6 +182,13 @@ class IOGFinder { // finder.step(); // } // auto iogs = finder.getIOGs(); + // + // + // The algorithm works as follows: + // 1. Pick a candidate IOG to work on + // 2. Within this IOG, get the next operation that should be added to the IOG + // 3. Handle the operation according to local rules, eliminating the candidate + // or splitting into multiple possible possibilities as necessary void step() { if (candidates.empty()) return; @@ -190,8 +206,18 @@ class IOGFinder { } Operation *op = *optOp; - candidate.iog.units.insert(op); + handleUnit(candidate, op); + } + // Handles an operation for a specific IOG candidate by: + // + // 1. Inserting the unit into the IOG + // 2. Marking necessary edges as followed (e.g. all merge inputs) + // 3. Splitting into multiple potential candidates if necessary: For example, + // only a single fork output can be followed, so there is a different possible + // IOG for each output + void handleUnit(IOGCandidate candidate, Operation *op) { + candidate.iog.units.insert(op); if (auto endOp = dyn_cast(op)) { followSingle(candidate, endOp.getOperands()); } else if (auto bufOp = dyn_cast(op)) { @@ -228,11 +254,9 @@ class IOGFinder { } else if (auto arithOp = dyn_cast(op)) { candidate.markFollowed(arithOp->getResults()[0]); followSingle(candidate, arithOp->getOperands()); - } else if (auto sourceOp = dyn_cast(op)) { - // SourceOps can not be part of an IOG, as they act like entry nodes. This - // means that the partial IOGs looking at these operations can be - // discarded, so nothing needs to be done } else if (isa(op)) { + // These act as terminating units, and no further edges need to be + // followed candidates.push_back(candidate); } else if (auto loadOp = dyn_cast(op)) { candidate.markFollowed(loadOp.getAddress()); @@ -240,7 +264,11 @@ class IOGFinder { // checkpoint.follow(loadOp.getData()); candidate.markFollowed(loadOp.getDataResult()); candidates.push_back(candidate); - } else if (auto memCon = dyn_cast(op)) { + } else if (isa(op)) { + // SourceOps can not be part of an IOG, as they act like entry nodes. This + // means that the partial IOGs looking at these operations can be + // discarded, so nothing needs to be done + // // MemoryControllers are only accessed by control signals during this // annotation, as the edges between loadOps/storeOps and the MC are not // added to the IOG. These control signals usually grant trivial IOGs that From f52748b588f0ca4a67b41f4462fcf65bef711f1f Mon Sep 17 00:00:00 2001 From: Bas Niekel Date: Sat, 25 Apr 2026 14:38:24 +0200 Subject: [PATCH 09/29] start of IOG-single-token invariant: Mark slots as IOG-terminating, and annotate SMV with a single slot in that case Annotate entry slots Extract all slots and eager fork states from IOG Export invariant to SMV --- data/rtl-config-smv.json | 4 +- .../experimental/Support/FormalProperty.h | 11 +++- .../include/experimental/Support/IOG.h | 2 +- .../HandshakeAnnotateProperties.cpp | 51 +++++++++++++++- experimental/lib/Support/FlowExpression.cpp | 1 + experimental/lib/Support/FormalProperty.cpp | 60 ++++++++++++++++++- experimental/lib/Support/IOG.cpp | 8 +-- .../tools/rigidification/rigidification.sh | 5 +- .../smv/generators/handshake/sink.py | 42 ++++++++++++- .../Handshake/HandshakeOpInternalStateNamer.h | 31 ++++++++++ .../HandshakeToHW/HandshakeToHW.cpp | 14 +++-- .../HandshakeOpInternalStateNamer.cpp | 19 ++++++ lib/Support/RTL/RTL.cpp | 6 ++ tools/export-rtl/export-rtl.cpp | 28 ++++++++- 14 files changed, 259 insertions(+), 23 deletions(-) diff --git a/data/rtl-config-smv.json b/data/rtl-config-smv.json index 0bf2d456f5..756849feef 100644 --- a/data/rtl-config-smv.json +++ b/data/rtl-config-smv.json @@ -89,7 +89,7 @@ }, { "name": "handshake.sink", - "generator": "python $DYNAMATIC/experimental/tools/unit-generators/smv/smv-unit-generator.py -n $MODULE_NAME -o $OUTPUT_DIR/$MODULE_NAME.smv -t sink -p bitwidth=$BITWIDTH", + "generator": "python $DYNAMATIC/experimental/tools/unit-generators/smv/smv-unit-generator.py -n $MODULE_NAME -o $OUTPUT_DIR/$MODULE_NAME.smv -t sink -p bitwidth=$BITWIDTH iog_terminator=$IOG_TERMINATOR", "hdl": "smv" }, { @@ -298,4 +298,4 @@ "generator": "python $DYNAMATIC/experimental/tools/unit-generators/smv/smv-unit-generator.py -n $MODULE_NAME -o $OUTPUT_DIR/$MODULE_NAME.smv -t lsq -p data_bitwidth=$DATA_BITWIDTH addr_bitwidth=$ADDR_BITWIDTH config_file=\"'$OUTPUT_DIR/$MODULE_NAME.json'\"", "hdl": "smv" } -] \ No newline at end of file +] diff --git a/experimental/include/experimental/Support/FormalProperty.h b/experimental/include/experimental/Support/FormalProperty.h index 34da8e6d2d..da78b35e69 100644 --- a/experimental/include/experimental/Support/FormalProperty.h +++ b/experimental/include/experimental/Support/FormalProperty.h @@ -277,14 +277,23 @@ class IOGSingleToken : public FormalProperty { fromJSON(const llvm::json::Value &value, llvm::json::Path path); IOGSingleToken() = default; - IOGSingleToken(unsigned long id, TAG tag); + IOGSingleToken(unsigned long id, TAG tag, + std::vector> slots, + std::vector forks) + : FormalProperty(id, tag, TYPE::IOGSingleToken), slots(std::move(slots)), + forks(std::move(forks)){}; ~IOGSingleToken() = default; static bool classof(const FormalProperty *fp) { return fp->getType() == TYPE::IOGSingleToken; } + std::vector> slots; + std::vector forks; + private: + inline static const StringLiteral SLOTS_LIT = "slots"; + inline static const StringLiteral FORKS_LIT = "forks"; }; class IOGConsecutiveTokens : public FormalProperty { diff --git a/experimental/include/experimental/Support/IOG.h b/experimental/include/experimental/Support/IOG.h index c83d5ba20f..ea0ced125b 100644 --- a/experimental/include/experimental/Support/IOG.h +++ b/experimental/include/experimental/Support/IOG.h @@ -30,7 +30,7 @@ struct IOG { IOG() = default; std::unordered_set units; llvm::DenseSet channels; - mlir::Value entry; + BlockArgument entry; inline bool contains(Operation *op) const { auto iter = units.find(op); diff --git a/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp b/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp index b9d0e34377..5ebd87c1f9 100644 --- a/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp +++ b/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp @@ -82,6 +82,7 @@ struct HandshakeAnnotatePropertiesPass LogicalResult annotateCopiedSlots(Operation &op); LogicalResult annotateCopiedSlotsOfAllForks(ModuleOp modOp); LogicalResult annotateReconvergentPathFlow(ModuleOp modOp); + LogicalResult annotateIOGSingleToken(const IOG &iog); LogicalResult annotateIOGConsecutiveTokens(const IOG &iog); }; @@ -320,6 +321,39 @@ std::vector findCopiedSents(const IOG &iog, } } // namespace +LogicalResult +HandshakeAnnotatePropertiesPass::annotateIOGSingleToken(const IOG &iog) { + std::vector> slots(0); + Operation *op = iog.entry.getOwner()->getParentOp(); + auto nameAttr = + op->getAttrOfType("argNames")[iog.entry.getArgNumber()]; + std::string name = dyn_cast(nameAttr).str(); + + slots.push_back(std::make_unique(name)); + std::vector forks(0); + for (auto &op : iog.units) { + for (auto &slot : getAllSlotsOfOperation(op)) { + slots.push_back(std::move(slot)); + } + if (auto forkOp = dyn_cast(op)) { + auto forkSlots = forkOp.getInternalSentStateNamers(); + int count = 0; + for (auto [i, channel] : llvm::enumerate(forkOp->getResults())) { + if (iog.contains(channel)) { + forks.push_back(forkSlots[i]); + count += 1; + } + } + assert(count == 1); + } + } + auto p = IOGSingleToken(uid, FormalProperty::TAG::INVAR, std::move(slots), + std::move(forks)); + uid++; + propertyTable.push_back(p.toJSON()); + return success(); +} + LogicalResult HandshakeAnnotatePropertiesPass::annotateIOGConsecutiveTokens(const IOG &iog) { std::vector>> @@ -364,6 +398,20 @@ HandshakeAnnotatePropertiesPass::annotateIOGConsecutiveTokens(const IOG &iog) { void HandshakeAnnotatePropertiesPass::runDynamaticPass() { ModuleOp modOp = getOperation(); + auto iogs = findAllIOGs(modOp); + llvm::DenseSet sinks; + for (auto &iog : iogs) { + for (Operation *unit : iog.units) { + if (auto sinkOp = dyn_cast(unit)) { + sinks.insert(sinkOp); + } + } + } + + for (SinkOp sink : sinks) { + auto x = UnitAttr::get(modOp.getContext()); + sink->setAttr("IOG_TERMINATOR", x); + } if (failed(annotateAbsenceOfBackpressure(modOp))) return signalPassFailure(); @@ -377,8 +425,9 @@ void HandshakeAnnotatePropertiesPass::runDynamaticPass() { if (failed(annotateReconvergentPathFlow(modOp))) return signalPassFailure(); - auto iogs = findAllIOGs(modOp); for (const auto &iog : iogs) { + if (failed(annotateIOGSingleToken(iog))) + return signalPassFailure(); if (failed(annotateIOGConsecutiveTokens(iog))) return signalPassFailure(); } diff --git a/experimental/lib/Support/FlowExpression.cpp b/experimental/lib/Support/FlowExpression.cpp index c15751892f..4ab21b717a 100644 --- a/experimental/lib/Support/FlowExpression.cpp +++ b/experimental/lib/Support/FlowExpression.cpp @@ -447,6 +447,7 @@ LogicalResult FlowEquationExtractor::extractBufferOp(BufferOp bufferOp) { // in = next + slot // Then, `in` is set to `next` auto slot = FlowVariable(FlowInternalState(slotNamer)); + slot.indexTokenTracker = in.indexTokenTracker; FlowVariable next = in.nextInternal(); if (failed(extractSlotEquation(in, next, slot))) { return failure(); diff --git a/experimental/lib/Support/FormalProperty.cpp b/experimental/lib/Support/FormalProperty.cpp index ccf02da2b0..4d60d847ae 100644 --- a/experimental/lib/Support/FormalProperty.cpp +++ b/experimental/lib/Support/FormalProperty.cpp @@ -117,8 +117,7 @@ FormalProperty::fromJSON(const llvm::json::Value &value, case TYPE::RPF: return ReconvergentPathFlow::fromJSON(value, path.field(INFO_LIT)); case TYPE::IOGSingleToken: - assert(false && "todo"); - return nullptr; + return IOGSingleToken::fromJSON(value, path.field(INFO_LIT)); case TYPE::IOGConsecutiveTokens: return IOGConsecutiveTokens::fromJSON(value, path.field(INFO_LIT)); } @@ -393,6 +392,63 @@ ReconvergentPathFlow::fromJSON(const llvm::json::Value &value, return prop; } +// IOGSingleToken + +llvm::json::Value IOGSingleToken::extraInfoToJSON() const { + std::vector slotsJSON; + slotsJSON.reserve(slots.size()); + for (auto &namer : slots) { + slotsJSON.push_back(namer->toJSON()); + } + llvm::json::Value slotsValue = slotsJSON; + + std::vector forksJSON; + forksJSON.reserve(forks.size()); + for (auto &sent : forks) { + forksJSON.push_back(sent.toInnerJSON()); + } + llvm::json::Value forksValue = forksJSON; + + return llvm::json::Object({{SLOTS_LIT, slotsValue}, {FORKS_LIT, forksValue}}); +} + +std::unique_ptr +IOGSingleToken::fromJSON(const llvm::json::Value &value, + llvm::json::Path path) { + auto prop = std::make_unique(); + llvm::json::Value info = prop->parseBaseAndExtractInfo(value, path); + + llvm::json::Object *obj = info.getAsObject(); + assert(obj); + if (auto iter = obj->find(SLOTS_LIT); iter != obj->end()) { + llvm::json::Array *slotsArray = iter->second.getAsArray(); + assert(slotsArray); + prop->slots.reserve(slotsArray->size()); + for (const llvm::json::Value &sentValue : *slotsArray) { + auto json = InternalStateNamer::fromJSON(sentValue, path); + assert(json); + prop->slots.push_back(std::move(json)); + } + } else { + path.report(json::ERR_MISSING_VALUE); + return nullptr; + } + if (auto iter = obj->find(FORKS_LIT); iter != obj->end()) { + llvm::json::Array *forksArray = iter->second.getAsArray(); + assert(forksArray); + prop->forks.reserve(forksArray->size()); + for (const llvm::json::Value &sentValue : *forksArray) { + auto innerJSON = EagerForkSentNamer::fromInnerJSON(sentValue, path); + assert(innerJSON); + prop->forks.push_back(*innerJSON); + } + } else { + path.report(json::ERR_MISSING_VALUE); + return nullptr; + } + return prop; +} + // IOGConsecutiveTokens llvm::json::Value IOGConsecutiveTokens::extraInfoToJSON() const { diff --git a/experimental/lib/Support/IOG.cpp b/experimental/lib/Support/IOG.cpp index a4121f2933..c69777bbc9 100644 --- a/experimental/lib/Support/IOG.cpp +++ b/experimental/lib/Support/IOG.cpp @@ -82,7 +82,7 @@ struct IOGCandidate { bool invalidIOG = false; IOGCandidate() = default; - IOGCandidate(mlir::Value entry) { + IOGCandidate(BlockArgument entry) { iog.entry = entry; markFollowed(entry); } @@ -168,7 +168,7 @@ struct IOGCandidate { using namespace dynamatic::handshake; class IOGFinder { public: - IOGFinder(mlir::Value entry) { + IOGFinder(BlockArgument entry) { IOGCandidate cp(entry); candidates.push_back(cp); } @@ -334,7 +334,7 @@ class IOGFinder { std::vector finals; }; -std::vector findAllIOGsWithEntry(mlir::Value entry) { +std::vector findAllIOGsWithEntry(BlockArgument entry) { IOGFinder finder(entry); while (!finder.isDone()) { finder.step(); @@ -348,7 +348,7 @@ std::vector findAllIOGs(ModuleOp modOp) { std::vector ret{}; for (handshake::FuncOp funcOp : modOp.getOps()) { // Each argument corresponds to an entry node. - for (mlir::Value arg : funcOp.getRegion().getArguments()) { + for (BlockArgument arg : funcOp.getRegion().getArguments()) { for (auto &iog : findAllIOGsWithEntry(arg)) { ret.push_back(std::move(iog)); } diff --git a/experimental/tools/rigidification/rigidification.sh b/experimental/tools/rigidification/rigidification.sh index 8e870e674d..26f8ecdf21 100644 --- a/experimental/tools/rigidification/rigidification.sh +++ b/experimental/tools/rigidification/rigidification.sh @@ -15,6 +15,7 @@ DYNAMATIC_OPT_BIN="$DYNAMATIC_DIR/bin/dynamatic-opt" DYNAMATIC_EXPORT_RTL_BIN="$DYNAMATIC_DIR/bin/export-rtl" F_FORMAL_HW="$FORMAL_DIR/hw.mlir" +F_FORMAL_INTERMEDIATE="$FORMAL_DIR/intermediate.mlir" F_FORMAL_PROP="$FORMAL_DIR/formal_properties.json" F_NUXMV_PROP="$FORMAL_DIR/property.rpt" F_NUXMV_CMD="$FORMAL_DIR/prove.cmd" @@ -35,10 +36,10 @@ rm -rf "$FORMAL_DIR" && mkdir -p "$FORMAL_DIR" # Annotate properties "$DYNAMATIC_OPT_BIN" "$F_HANDSHAKE_EXPORT" \ --handshake-annotate-properties="json-path=$F_FORMAL_PROP annotate-invariants" \ - > /dev/null + > "$F_FORMAL_INTERMEDIATE" # handshake level -> hw level -"$DYNAMATIC_OPT_BIN" "$F_HANDSHAKE_EXPORT" --lower-handshake-to-hw \ +"$DYNAMATIC_OPT_BIN" "$F_FORMAL_INTERMEDIATE" --lower-handshake-to-hw \ > "$F_FORMAL_HW" # generate SMV diff --git a/experimental/tools/unit-generators/smv/generators/handshake/sink.py b/experimental/tools/unit-generators/smv/generators/handshake/sink.py index fe8c573ac3..bbdb53e42a 100644 --- a/experimental/tools/unit-generators/smv/generators/handshake/sink.py +++ b/experimental/tools/unit-generators/smv/generators/handshake/sink.py @@ -4,12 +4,48 @@ def generate_sink(name, params): data_type = SmvScalarType(params[ATTR_BITWIDTH]) - if data_type.bitwidth == 0: - return _generate_sink_dataless(name) + if params["iog_terminator"]: + if data_type.bitwidth == 0: + return _generate_iog_terminator_dataless(name) + else: + return _generate_iog_terminator(name, data_type) else: - return _generate_sink(name, data_type) + if data_type.bitwidth == 0: + return _generate_sink_dataless(name) + else: + return _generate_sink(name, data_type) +def _generate_iog_terminator_dataless(name): + return f""" +MODULE {name}(ins_valid) + VAR + full : boolean; + + ASSIGN + init(full) := FALSE; + next(full) := full | ins_valid; + + -- output + DEFINE + ins_ready := !full; +""" + +def _generate_iog_terminator(name, data_type): + return f""" +MODULE {name}(ins, ins_valid) + VAR + full : boolean; + + ASSIGN + init(full) := FALSE; + next(full) := full | ins_valid; + + -- output + DEFINE + ins_ready := !full; +""" + def _generate_sink_dataless(name): return f""" MODULE {name}(ins_valid) diff --git a/include/dynamatic/Dialect/Handshake/HandshakeOpInternalStateNamer.h b/include/dynamatic/Dialect/Handshake/HandshakeOpInternalStateNamer.h index 4ed859b092..a81dc2093f 100644 --- a/include/dynamatic/Dialect/Handshake/HandshakeOpInternalStateNamer.h +++ b/include/dynamatic/Dialect/Handshake/HandshakeOpInternalStateNamer.h @@ -18,6 +18,7 @@ struct ConstrainedNamer; struct ConstrainedEagerForkSentNamer; struct ConstrainedBufferSlotFullNamer; struct MemoryControllerSlotNamer; +struct EntrySlotNamer; std::vector> getAllSlotsOfOperation(Operation *op); @@ -41,6 +42,7 @@ struct InternalStateNamer { PipelineTokenCount, Constrained, MemoryControllerSlot, + EntrySlot, }; static std::optional typeFromStr(const std::string &s); static std::string typeToStr(TYPE t); @@ -83,6 +85,7 @@ struct InternalStateNamer { static constexpr llvm::StringLiteral CONSTRAINED = "Constrained"; static constexpr llvm::StringLiteral MEMORY_CONTROLLER_SLOT = "MemoryControllerSlot"; + static constexpr llvm::StringLiteral ENTRY_SLOT = "EntrySlot"; static constexpr llvm::StringLiteral TOKEN_COUNT = "TokenCount"; static constexpr llvm::StringLiteral PIPELINE_TOKEN_COUNT = "PipelineTokenCount"; @@ -398,6 +401,34 @@ struct MemoryControllerSlotNamer : InternalStateNamer { static constexpr llvm::StringLiteral LOADLESS_LIT = "loadless"; }; +struct EntrySlotNamer : InternalStateNamer { + // a_valid + // b_valid + // y_start_valid + // x_start_valid + // start_valid + EntrySlotNamer() = default; + EntrySlotNamer(const std::string &name) + : InternalStateNamer(TYPE::EntrySlot), argName(name) {} + ~EntrySlotNamer() = default; + + static inline bool classof(const InternalStateNamer *fp) { + return fp->type == TYPE::EntrySlot; + } + + inline std::string getSMVName() const override { + return llvm::formatv("{0}_valid", argName); + } + + inline llvm::json::Value toInnerJSON() const override { + return llvm::json::Object({{ARG_NAME_LIT, argName}}); + } + std::unique_ptr static fromInnerJSON( + const llvm::json::Value &value, llvm::json::Path path); + std::string argName; + static constexpr llvm::StringLiteral ARG_NAME_LIT = "arg_name"; +}; + } // namespace handshake } // namespace dynamatic diff --git a/lib/Conversion/HandshakeToHW/HandshakeToHW.cpp b/lib/Conversion/HandshakeToHW/HandshakeToHW.cpp index 00fb5d03b2..f12765c641 100644 --- a/lib/Conversion/HandshakeToHW/HandshakeToHW.cpp +++ b/lib/Conversion/HandshakeToHW/HandshakeToHW.cpp @@ -585,11 +585,15 @@ ModuleDiscriminator::ModuleDiscriminator(Operation *op) { // Number of input channels addUnsigned("SIZE", op->getNumOperands()); }) - .Case( - [&](auto) { - // Bitwidth - addType("DATA_TYPE", op->getOperand(0)); - }) + .Case([&](auto) { + // Bitwidth + addType("DATA_TYPE", op->getOperand(0)); + addBoolean("IOG_TERMINATOR", op->hasAttr("IOG_TERMINATOR")); + }) + .Case([&](auto) { + // Bitwidth + addType("DATA_TYPE", op->getOperand(0)); + }) .Case([&](handshake::BufferOp bufferOp) { // Bitwidth addType("DATA_TYPE", bufferOp.getOperand()); diff --git a/lib/Dialect/Handshake/HandshakeOpInternalStateNamer.cpp b/lib/Dialect/Handshake/HandshakeOpInternalStateNamer.cpp index b96e277f5b..0918699296 100644 --- a/lib/Dialect/Handshake/HandshakeOpInternalStateNamer.cpp +++ b/lib/Dialect/Handshake/HandshakeOpInternalStateNamer.cpp @@ -15,6 +15,8 @@ InternalStateNamer::typeFromStr(const std::string &s) { return TYPE::Constrained; if (s == MEMORY_CONTROLLER_SLOT) return TYPE::MemoryControllerSlot; + if (s == ENTRY_SLOT) + return TYPE::EntrySlot; if (s == TOKEN_COUNT) return TYPE::TokenCount; if (s == PIPELINE_TOKEN_COUNT) @@ -35,6 +37,8 @@ std::string InternalStateNamer::typeToStr(TYPE t) { return CONSTRAINED.str(); case TYPE::MemoryControllerSlot: return MEMORY_CONTROLLER_SLOT.str(); + case TYPE::EntrySlot: + return ENTRY_SLOT.str(); case TYPE::TokenCount: return TOKEN_COUNT.str(); case TYPE::PipelineTokenCount: @@ -89,6 +93,10 @@ InternalStateNamer::fromJSON(const llvm::json::Value &value, prop = MemoryControllerSlotNamer::fromInnerJSON(inner, path); assert(prop && "mc slot failed"); break; + case TYPE::EntrySlot: + prop = EntrySlotNamer::fromInnerJSON(inner, path); + assert(prop && "entry slot failed"); + break; } prop->type = type; return prop; @@ -207,6 +215,16 @@ MemoryControllerSlotNamer::fromInnerJSON(const llvm::json::Value &value, return prop; } +std::unique_ptr +EntrySlotNamer::fromInnerJSON(const llvm::json::Value &value, + llvm::json::Path path) { + llvm::json::ObjectMapper mapper(value, path); + auto prop = std::make_unique(); + if (!mapper || !mapper.map(ARG_NAME_LIT, prop->argName)) + return nullptr; + return prop; +} + std::vector> getAllSlotsOfOperation(Operation *op) { std::vector> ret; @@ -216,6 +234,7 @@ getAllSlotsOfOperation(Operation *op) { ret.push_back(std::make_unique(slot)); } } + // TODO: Handle LoadOp for MC slot if (auto bufferOp = dyn_cast(op)) { auto slots = bufferOp.getInternalSlotStateNamers(); for (auto &slot : slots) { diff --git a/lib/Support/RTL/RTL.cpp b/lib/Support/RTL/RTL.cpp index b613155b7d..3833792bb9 100644 --- a/lib/Support/RTL/RTL.cpp +++ b/lib/Support/RTL/RTL.cpp @@ -286,6 +286,12 @@ LogicalResult RTLMatch::registerParameters(hw::HWModuleExternOp &modOp) { modOp->template getAttrOfType(RTL_NAME_ATTR_NAME).getValue(); auto modType = modOp.getModuleType(); + if (handshakeOp == "handshake.sink") { + bool x = modOp->getAttrOfType(RTL_PARAMETERS_ATTR_NAME) + .contains("IOG_TERMINATOR"); + serializedParams["IOG_TERMINATOR"] = x ? "True" : "False"; + } + LogicalResult gotBitwidth = registerBitwidthParameter(modOp, handshakeOp, modType); LogicalResult gotExtraSignals = diff --git a/tools/export-rtl/export-rtl.cpp b/tools/export-rtl/export-rtl.cpp index ab438acc8b..2fc90fa073 100644 --- a/tools/export-rtl/export-rtl.cpp +++ b/tools/export-rtl/export-rtl.cpp @@ -1297,6 +1297,30 @@ LogicalResult SMVWriter::createProperties(WriteModData &data) const { } std::string propertyString = llvm::join(eqs, " & "); data.properties[p->getId()] = {propertyString, propertyTag}; + } else if (auto *p = llvm::dyn_cast(property.get())) { + // count(slot1, slot2, ...) = 1 + count(fork1, fork2, ...) + std::vector smvSlots(0); + smvSlots.reserve(p->slots.size()); + for (auto &slot : p->slots) { + smvSlots.push_back(slot->getSMVName()); + } + // smvSlots cannot be empty, as each IOG contains at least the entry slot + + std::vector smvForks(0); + smvForks.reserve(p->forks.size()); + for (auto &fork : p->forks) { + smvForks.push_back(fork.getSMVName()); + } + std::string rhs; + if (smvForks.empty()) { + rhs = "1"; + } else { + rhs = llvm::formatv("1 + count({0})", llvm::join(smvForks, ", ")); + } + + std::string propertyString = + llvm::formatv("count({0}) = {1}", llvm::join(smvSlots, ", "), rhs); + data.properties[p->getId()] = {propertyString, propertyTag}; } else if (auto *p = llvm::dyn_cast(property.get())) { // buffer1.slotted_token_count > 0 & buffer2.slotted_token_count > 0 -> // fork3.outs1_sent | fork4.outs0_sent @@ -1313,10 +1337,10 @@ LogicalResult SMVWriter::createProperties(WriteModData &data) const { } assert(p->slot1); assert(p->slot2); - std::string full = + std::string propertyString = llvm::formatv("(({0} > 0) & ({1} > 0)) -> ({2})", p->slot1->getSMVName(), p->slot2->getSMVName(), right); - data.properties[p->getId()] = {full, propertyTag}; + data.properties[p->getId()] = {propertyString, propertyTag}; } else { llvm::errs() << "Formal property Type not known\n"; return failure(); From 5accc263c03193eeab91aa96fb1e5a6d605c3da7 Mon Sep 17 00:00:00 2001 From: Bas Niekel Date: Sat, 25 Apr 2026 15:49:03 +0200 Subject: [PATCH 10/29] getAllSlotsOfOperation properly handles load's hidden slot in MC --- .../HandshakeOpInternalStateNamer.cpp | 24 ++++++++++++++++++- 1 file changed, 23 insertions(+), 1 deletion(-) diff --git a/lib/Dialect/Handshake/HandshakeOpInternalStateNamer.cpp b/lib/Dialect/Handshake/HandshakeOpInternalStateNamer.cpp index 0918699296..9266e59f2e 100644 --- a/lib/Dialect/Handshake/HandshakeOpInternalStateNamer.cpp +++ b/lib/Dialect/Handshake/HandshakeOpInternalStateNamer.cpp @@ -1,5 +1,6 @@ #include "dynamatic/Dialect/Handshake/HandshakeOpInternalStateNamer.h" #include "dynamatic/Dialect/Handshake/HandshakeInterfaces.h" +#include "dynamatic/Dialect/Handshake/HandshakeOps.h" namespace dynamatic { namespace handshake { @@ -234,7 +235,28 @@ getAllSlotsOfOperation(Operation *op) { ret.push_back(std::make_unique(slot)); } } - // TODO: Handle LoadOp for MC slot + if (auto loadOp = dyn_cast(op)) { + // TODO: Handle LoadOp for MC slot + auto slots = loadOp.getInternalSlotStateNamers(); + auto *mcOp = loadOp.getAddressResult().getUses().begin()->getOwner(); + assert(mcOp); + auto mc = dyn_cast(mcOp); + assert(mc); + size_t nLoads = mc.getNumLoadPorts(); + std::optional mcSlot; + for (size_t i = 0; i < nLoads; ++i) { + if (mc.getLoadPort(i)->getLoadOp() == loadOp) { + assert(!mcSlot.has_value()); + mcSlot = mc.getLoadPortSlotNamer(i); + } + } + assert(mcSlot); + ret.push_back(std::make_unique(slots[0])); + ret.push_back(std::make_unique(*mcSlot)); + ret.push_back(std::make_unique(slots[1])); + return ret; + } + if (auto bufferOp = dyn_cast(op)) { auto slots = bufferOp.getInternalSlotStateNamers(); for (auto &slot : slots) { From c05778fa973c3c1268006fcafe53e4b42d69e2ed Mon Sep 17 00:00:00 2001 From: Bas Niekel Date: Sat, 25 Apr 2026 16:15:13 +0200 Subject: [PATCH 11/29] slot of terminating sink is annotatable --- .../Dialect/Handshake/HandshakeOpInternalStateNamer.h | 1 + include/dynamatic/Dialect/Handshake/HandshakeOps.td | 4 ++++ .../Handshake/HandshakeOpInternalStateNamer.cpp | 7 +++++++ lib/Dialect/Handshake/HandshakeOps.cpp | 11 +++++++++++ 4 files changed, 23 insertions(+) diff --git a/include/dynamatic/Dialect/Handshake/HandshakeOpInternalStateNamer.h b/include/dynamatic/Dialect/Handshake/HandshakeOpInternalStateNamer.h index a81dc2093f..b7bdfd41ad 100644 --- a/include/dynamatic/Dialect/Handshake/HandshakeOpInternalStateNamer.h +++ b/include/dynamatic/Dialect/Handshake/HandshakeOpInternalStateNamer.h @@ -19,6 +19,7 @@ struct ConstrainedEagerForkSentNamer; struct ConstrainedBufferSlotFullNamer; struct MemoryControllerSlotNamer; struct EntrySlotNamer; +struct TerminatingSinkNamer; std::vector> getAllSlotsOfOperation(Operation *op); diff --git a/include/dynamatic/Dialect/Handshake/HandshakeOps.td b/include/dynamatic/Dialect/Handshake/HandshakeOps.td index d34c6acc79..80bdb632ad 100644 --- a/include/dynamatic/Dialect/Handshake/HandshakeOps.td +++ b/include/dynamatic/Dialect/Handshake/HandshakeOps.td @@ -567,6 +567,10 @@ def SinkOp : Handshake_Op<"sink"> { ``` }]; + let extraClassDeclaration = [{ + bool terminatesIOG(); + BufferSlotFullNamer getTerminatingSlot(); + }]; let arguments = (ins HandshakeType:$operand); let assemblyFormat = [{ $operand attr-dict `:` custom(type($operand)) diff --git a/lib/Dialect/Handshake/HandshakeOpInternalStateNamer.cpp b/lib/Dialect/Handshake/HandshakeOpInternalStateNamer.cpp index 9266e59f2e..70016ecfec 100644 --- a/lib/Dialect/Handshake/HandshakeOpInternalStateNamer.cpp +++ b/lib/Dialect/Handshake/HandshakeOpInternalStateNamer.cpp @@ -235,6 +235,13 @@ getAllSlotsOfOperation(Operation *op) { ret.push_back(std::make_unique(slot)); } } + if (auto sinkOp = dyn_cast(op)) { + if (sinkOp.terminatesIOG()) { + ret.push_back( + std::make_unique(sinkOp.getTerminatingSlot())); + } + return ret; + } if (auto loadOp = dyn_cast(op)) { // TODO: Handle LoadOp for MC slot auto slots = loadOp.getInternalSlotStateNamers(); diff --git a/lib/Dialect/Handshake/HandshakeOps.cpp b/lib/Dialect/Handshake/HandshakeOps.cpp index c1c197a0f2..b79e09f8a9 100644 --- a/lib/Dialect/Handshake/HandshakeOps.cpp +++ b/lib/Dialect/Handshake/HandshakeOps.cpp @@ -611,6 +611,17 @@ LogicalResult ConstantOp::verify() { } bool JoinOp::isControl() { return true; } +bool SinkOp::terminatesIOG() { + return getOperation()->hasAttr("IOG_TERMINATOR"); +} + +BufferSlotFullNamer SinkOp::getTerminatingSlot() { + assert(terminatesIOG()); + Operation *op = getOperation(); + std::string name = + op->getAttrOfType<::mlir::StringAttr>(NameAnalysis::ATTR_NAME).str(); + return BufferSlotFullNamer(name, "full", 0); +} /// Based on mlir::func::CallOp::verifySymbolUses LogicalResult InstanceOp::verifySymbolUses(SymbolTableCollection &symbolTable) { From 82ec8c6bd66c07e2b7048f7178b1ccd30896e5b3 Mon Sep 17 00:00:00 2001 From: Bas Niekel Date: Sat, 25 Apr 2026 17:15:25 +0200 Subject: [PATCH 12/29] change testbench generator to work with IOG single-token invariant --- .../FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp | 4 ++-- experimental/lib/Support/CreateSmvFormalTestbench.cpp | 4 ++-- .../tools/rigidification/rigidification-testbench.cpp | 4 ++-- .../tools/unit-generators/smv/generators/handshake/sink.py | 2 ++ 4 files changed, 8 insertions(+), 6 deletions(-) diff --git a/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp b/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp index 5ebd87c1f9..1ed0da9aca 100644 --- a/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp +++ b/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp @@ -409,8 +409,8 @@ void HandshakeAnnotatePropertiesPass::runDynamaticPass() { } for (SinkOp sink : sinks) { - auto x = UnitAttr::get(modOp.getContext()); - sink->setAttr("IOG_TERMINATOR", x); + auto unitAttr = UnitAttr::get(modOp.getContext()); + sink->setAttr("IOG_TERMINATOR", unitAttr); } if (failed(annotateAbsenceOfBackpressure(modOp))) diff --git a/experimental/lib/Support/CreateSmvFormalTestbench.cpp b/experimental/lib/Support/CreateSmvFormalTestbench.cpp index 8ac8ee1274..213a8007da 100644 --- a/experimental/lib/Support/CreateSmvFormalTestbench.cpp +++ b/experimental/lib/Support/CreateSmvFormalTestbench.cpp @@ -375,7 +375,7 @@ std::string createSmvFormalTestbench(const SmvTestbenchConfig &config) { if (config.syncOutput) { wrapper << instantiateJoin(config.modelSmvName, config.results) << "\n"; - wrapper << " DEFINE global_ready := TRUE;\n"; + wrapper << " DEFINE global_ready := FALSE;\n"; } else { wrapper << instantiateSinks(config.modelSmvName, config.results) << "\n"; @@ -384,4 +384,4 @@ std::string createSmvFormalTestbench(const SmvTestbenchConfig &config) { return wrapper.str(); } -} // namespace dynamatic::experimental \ No newline at end of file +} // namespace dynamatic::experimental diff --git a/experimental/tools/rigidification/rigidification-testbench.cpp b/experimental/tools/rigidification/rigidification-testbench.cpp index 4759c78c5a..67c7a08c24 100644 --- a/experimental/tools/rigidification/rigidification-testbench.cpp +++ b/experimental/tools/rigidification/rigidification-testbench.cpp @@ -100,7 +100,7 @@ integration-tests/fir/out/hdl/ --mlir intregation-tests/fir/out/comp/hw.mlir/n)D .results = res, .modelSmvName = kernelName, .nrOfTokens = 1, - .generateExactNrOfTokens = false, + .generateExactNrOfTokens = true, .syncOutput = true}; std::string wrapper = @@ -111,4 +111,4 @@ integration-tests/fir/out/hdl/ --mlir intregation-tests/fir/out/comp/hw.mlir/n)D } exit(false); -} \ No newline at end of file +} diff --git a/experimental/tools/unit-generators/smv/generators/handshake/sink.py b/experimental/tools/unit-generators/smv/generators/handshake/sink.py index bbdb53e42a..c12a51e3d9 100644 --- a/experimental/tools/unit-generators/smv/generators/handshake/sink.py +++ b/experimental/tools/unit-generators/smv/generators/handshake/sink.py @@ -29,6 +29,7 @@ def _generate_iog_terminator_dataless(name): -- output DEFINE ins_ready := !full; + full_full := full; """ def _generate_iog_terminator(name, data_type): @@ -44,6 +45,7 @@ def _generate_iog_terminator(name, data_type): -- output DEFINE ins_ready := !full; + full_full := full; """ def _generate_sink_dataless(name): From dcb74b6b5806edf3098e290085e63a5499c76500 Mon Sep 17 00:00:00 2001 From: Bas Niekel Date: Wed, 29 Apr 2026 17:59:56 +0200 Subject: [PATCH 13/29] change testbench to: pass "self" to module of the environment endOp is a terminating node --- .../experimental/Support/CreateSmvFormalTestbench.h | 4 +++- .../lib/Support/CreateSmvFormalTestbench.cpp | 12 ++++++++++-- .../unit-generators/smv/generators/handshake/sink.py | 2 ++ .../Handshake/HandshakeOpInternalStateNamer.cpp | 4 ++++ tools/export-rtl/export-rtl.cpp | 2 +- 5 files changed, 20 insertions(+), 4 deletions(-) diff --git a/experimental/include/experimental/Support/CreateSmvFormalTestbench.h b/experimental/include/experimental/Support/CreateSmvFormalTestbench.h index 351fe81378..8a28ab2370 100644 --- a/experimental/include/experimental/Support/CreateSmvFormalTestbench.h +++ b/experimental/include/experimental/Support/CreateSmvFormalTestbench.h @@ -48,6 +48,8 @@ struct SmvTestbenchConfig { // Determines if the outputs are synchronized with a join or if they are // consumed by sinks bool syncOutput = false; + + bool deadBufferOutput = true; }; // Create a wrapper for the provided SMV file. @@ -157,4 +159,4 @@ MODULE sink(ins_valid) DEFINE ins_ready := TRUE;)DELIM"; } // namespace dynamatic::experimental -#endif // DYNAMATIC_EXPERIMENTAL_ELASTIC_MITER_CREATE_FORMAL_TESTBENCH_H \ No newline at end of file +#endif // DYNAMATIC_EXPERIMENTAL_ELASTIC_MITER_CREATE_FORMAL_TESTBENCH_H diff --git a/experimental/lib/Support/CreateSmvFormalTestbench.cpp b/experimental/lib/Support/CreateSmvFormalTestbench.cpp index 213a8007da..67f4c855da 100644 --- a/experimental/lib/Support/CreateSmvFormalTestbench.cpp +++ b/experimental/lib/Support/CreateSmvFormalTestbench.cpp @@ -34,6 +34,7 @@ static std::string instantiateModuleUnderTest( const SmallVector> &results, bool syncOutput = false) { SmallVector inputVariables; + inputVariables.push_back("self"); for (const auto &argument : arguments) { // The current handshake2smv conversion also creates a dataOut port when it // is of type control @@ -373,9 +374,16 @@ std::string createSmvFormalTestbench(const SmvTestbenchConfig &config) { config.results, config.syncOutput) << "\n"; - if (config.syncOutput) { + if (config.deadBufferOutput) { wrapper << instantiateJoin(config.modelSmvName, config.results) << "\n"; - wrapper << " DEFINE global_ready := FALSE;\n"; + wrapper << " VAR end_full : boolean;\n"; + wrapper << " ASSIGN\n"; + wrapper << " init(end_full) := FALSE;\n"; + wrapper << " next(end_full) := end_full | join_global.outs_valid;\n"; + wrapper << " DEFINE global_ready := !end_full;\n"; + } else if (config.syncOutput) { + wrapper << instantiateJoin(config.modelSmvName, config.results) << "\n"; + wrapper << " DEFINE global_ready := TRUE;\n"; } else { wrapper << instantiateSinks(config.modelSmvName, config.results) << "\n"; diff --git a/experimental/tools/unit-generators/smv/generators/handshake/sink.py b/experimental/tools/unit-generators/smv/generators/handshake/sink.py index c12a51e3d9..1311a0b97a 100644 --- a/experimental/tools/unit-generators/smv/generators/handshake/sink.py +++ b/experimental/tools/unit-generators/smv/generators/handshake/sink.py @@ -32,6 +32,7 @@ def _generate_iog_terminator_dataless(name): full_full := full; """ + def _generate_iog_terminator(name, data_type): return f""" MODULE {name}(ins, ins_valid) @@ -48,6 +49,7 @@ def _generate_iog_terminator(name, data_type): full_full := full; """ + def _generate_sink_dataless(name): return f""" MODULE {name}(ins_valid) diff --git a/lib/Dialect/Handshake/HandshakeOpInternalStateNamer.cpp b/lib/Dialect/Handshake/HandshakeOpInternalStateNamer.cpp index 70016ecfec..dc5501fe70 100644 --- a/lib/Dialect/Handshake/HandshakeOpInternalStateNamer.cpp +++ b/lib/Dialect/Handshake/HandshakeOpInternalStateNamer.cpp @@ -242,6 +242,10 @@ getAllSlotsOfOperation(Operation *op) { } return ret; } + + if (auto endOp = dyn_cast(op)) { + ret.push_back(std::make_unique("testbench", "end", 0)); + } if (auto loadOp = dyn_cast(op)) { // TODO: Handle LoadOp for MC slot auto slots = loadOp.getInternalSlotStateNamers(); diff --git a/tools/export-rtl/export-rtl.cpp b/tools/export-rtl/export-rtl.cpp index af9d17d8ba..7c27c453c3 100644 --- a/tools/export-rtl/export-rtl.cpp +++ b/tools/export-rtl/export-rtl.cpp @@ -1443,7 +1443,7 @@ LogicalResult SMVWriter::write(hw::HWModuleOp modOp, writeIncludes(data); os << "\n\n"; - os << "MODULE " << modOp.getSymName() << " ("; + os << "MODULE " << modOp.getSymName() << " (testbench, "; data.writeIO([](const llvm::Twine &name, PortType dir, std::optional type, From bb75abf8d1c429b45a191ca0f0c7cc2018d4b9a6 Mon Sep 17 00:00:00 2001 From: Bas Niekel Date: Wed, 29 Apr 2026 18:03:22 +0200 Subject: [PATCH 14/29] set default testbench to not use dead buffers --- .../include/experimental/Support/CreateSmvFormalTestbench.h | 4 +++- .../tools/rigidification/rigidification-testbench.cpp | 2 +- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/experimental/include/experimental/Support/CreateSmvFormalTestbench.h b/experimental/include/experimental/Support/CreateSmvFormalTestbench.h index 8a28ab2370..031642e6fb 100644 --- a/experimental/include/experimental/Support/CreateSmvFormalTestbench.h +++ b/experimental/include/experimental/Support/CreateSmvFormalTestbench.h @@ -49,7 +49,9 @@ struct SmvTestbenchConfig { // consumed by sinks bool syncOutput = false; - bool deadBufferOutput = true; + // Determines if the output is modelled as a dead buffer (i.e. accepts one + // token, then the output is no longer ready + bool deadBufferOutput = false; }; // Create a wrapper for the provided SMV file. diff --git a/experimental/tools/rigidification/rigidification-testbench.cpp b/experimental/tools/rigidification/rigidification-testbench.cpp index 67c7a08c24..b5fcd22e1c 100644 --- a/experimental/tools/rigidification/rigidification-testbench.cpp +++ b/experimental/tools/rigidification/rigidification-testbench.cpp @@ -101,7 +101,7 @@ integration-tests/fir/out/hdl/ --mlir intregation-tests/fir/out/comp/hw.mlir/n)D .modelSmvName = kernelName, .nrOfTokens = 1, .generateExactNrOfTokens = true, - .syncOutput = true}; + .deadBufferOutput = true}; std::string wrapper = dynamatic::experimental::createSmvFormalTestbench(smvConfig); From f437c3a9f3c0061b3ccab1169628987d7154a4b4 Mon Sep 17 00:00:00 2001 From: Bas Niekel Date: Wed, 29 Apr 2026 18:31:07 +0200 Subject: [PATCH 15/29] format --- experimental/include/experimental/Support/FormalProperty.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/experimental/include/experimental/Support/FormalProperty.h b/experimental/include/experimental/Support/FormalProperty.h index 7339239a73..1810ed6b46 100644 --- a/experimental/include/experimental/Support/FormalProperty.h +++ b/experimental/include/experimental/Support/FormalProperty.h @@ -284,7 +284,7 @@ class IOGSingleToken : public FormalProperty { std::vector> slots, std::vector forks) : FormalProperty(id, tag, TYPE::IOGSingleToken), slots(std::move(slots)), - forks(std::move(forks)){}; + forks(std::move(forks)) {}; ~IOGSingleToken() = default; static bool classof(const FormalProperty *fp) { From bc68eef3a34e088db4c79f016f226ef564991cfe Mon Sep 17 00:00:00 2001 From: Bas Niekel Date: Thu, 30 Apr 2026 13:40:43 +0200 Subject: [PATCH 16/29] change types.mlir unit test --- test/Conversion/HandshakeToHW/types.mlir | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/Conversion/HandshakeToHW/types.mlir b/test/Conversion/HandshakeToHW/types.mlir index 70e692511b..e6c8d9c86f 100644 --- a/test/Conversion/HandshakeToHW/types.mlir +++ b/test/Conversion/HandshakeToHW/types.mlir @@ -7,7 +7,7 @@ // CHECK: hw.instance "sink0" @handshake_sink_0(ins: %[[VAL_0]]: !handshake.channel, clk: %[[VAL_2]]: i1, rst: %[[VAL_3]]: i1) -> () // CHECK: hw.output %[[VAL_1]] : !handshake.control<> // CHECK: } -// CHECK: hw.module.extern @handshake_sink_0(in %[[VAL_5:.*]] : !handshake.channel, in %[[VAL_6:.*]] : i1, in %[[VAL_7:.*]] : i1) attributes {hw.name = "handshake.sink", hw.parameters = {DATA_TYPE = !handshake.channel}} +// CHECK: hw.module.extern @handshake_sink_0(in %[[VAL_5:.*]] : !handshake.channel, in %[[VAL_6:.*]] : i1, in %[[VAL_7:.*]] : i1) attributes {hw.name = "handshake.sink", hw.parameters = {DATA_TYPE = !handshake.channel, IOG_TERMINATOR = (true|false)}} handshake.func @dontChangeTypes(%arg : !handshake.channel, %start: !handshake.control<>) -> !handshake.control<> { sink %arg : end %start : <> From 789d98bbfd3a98fb0370831796d6f1904429ea2b Mon Sep 17 00:00:00 2001 From: Bas Niekel Date: Thu, 30 Apr 2026 15:16:07 +0200 Subject: [PATCH 17/29] attempt fix types.mlir --- test/Conversion/HandshakeToHW/types.mlir | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/Conversion/HandshakeToHW/types.mlir b/test/Conversion/HandshakeToHW/types.mlir index e6c8d9c86f..ec7161153a 100644 --- a/test/Conversion/HandshakeToHW/types.mlir +++ b/test/Conversion/HandshakeToHW/types.mlir @@ -7,7 +7,7 @@ // CHECK: hw.instance "sink0" @handshake_sink_0(ins: %[[VAL_0]]: !handshake.channel, clk: %[[VAL_2]]: i1, rst: %[[VAL_3]]: i1) -> () // CHECK: hw.output %[[VAL_1]] : !handshake.control<> // CHECK: } -// CHECK: hw.module.extern @handshake_sink_0(in %[[VAL_5:.*]] : !handshake.channel, in %[[VAL_6:.*]] : i1, in %[[VAL_7:.*]] : i1) attributes {hw.name = "handshake.sink", hw.parameters = {DATA_TYPE = !handshake.channel, IOG_TERMINATOR = (true|false)}} +// CHECK: hw.module.extern @handshake_sink_0(in %[[VAL_5:.*]] : !handshake.channel, in %[[VAL_6:.*]] : i1, in %[[VAL_7:.*]] : i1) attributes {hw.name = "handshake.sink", hw.parameters = {DATA_TYPE = !handshake.channel, IOG_TERMINATOR = {{(true|false)}}}} handshake.func @dontChangeTypes(%arg : !handshake.channel, %start: !handshake.control<>) -> !handshake.control<> { sink %arg : end %start : <> From 39adf311f2634f7cb6d3d1ffa281bec24e759827 Mon Sep 17 00:00:00 2001 From: Bas Niekel Date: Wed, 6 May 2026 12:02:58 +0200 Subject: [PATCH 18/29] more comments --- .../Support/CreateSmvFormalTestbench.h | 2 +- .../experimental/Support/FormalProperty.h | 12 +++++++++++ .../include/experimental/Support/IOG.h | 20 ++++++++++--------- .../HandshakeAnnotateProperties.cpp | 5 +++++ experimental/lib/Support/IOG.cpp | 9 ++++++++- 5 files changed, 37 insertions(+), 11 deletions(-) diff --git a/experimental/include/experimental/Support/CreateSmvFormalTestbench.h b/experimental/include/experimental/Support/CreateSmvFormalTestbench.h index 031642e6fb..df35a8c7bf 100644 --- a/experimental/include/experimental/Support/CreateSmvFormalTestbench.h +++ b/experimental/include/experimental/Support/CreateSmvFormalTestbench.h @@ -50,7 +50,7 @@ struct SmvTestbenchConfig { bool syncOutput = false; // Determines if the output is modelled as a dead buffer (i.e. accepts one - // token, then the output is no longer ready + // token, then the output is no longer ready) bool deadBufferOutput = false; }; diff --git a/experimental/include/experimental/Support/FormalProperty.h b/experimental/include/experimental/Support/FormalProperty.h index 1810ed6b46..f29b317500 100644 --- a/experimental/include/experimental/Support/FormalProperty.h +++ b/experimental/include/experimental/Support/FormalProperty.h @@ -273,6 +273,11 @@ class ReconvergentPathFlow : public FormalProperty { inline static const StringLiteral EQUATIONS_LIT = "equations"; }; +// An IOG contains a single token at the start (at the entry), and no other +// tokens will ever enter or leave. Tokens can be duplicated by eager forks, but +// they keep track of this within their `sent` state. Because of this, the +// number of occupied slots within an IOG is equal to one plus the number of +// duplicated tokens by fork. class IOGSingleToken : public FormalProperty { public: llvm::json::Value extraInfoToJSON() const override; @@ -299,6 +304,13 @@ class IOGSingleToken : public FormalProperty { inline static const StringLiteral FORKS_LIT = "forks"; }; +// Within an IOG, multiple slots can be occupied when forks duplicate tokens. +// Whereas the previous invariant only states that there needs to be an active +// fork somewhere, this invariant determines where the active fork could be: If +// any two slots are occupied, there must be at least one path connecting them, +// and for some path p, there must be an active fork along p with the start of p +// as the copied slot (i.e. no other slots between the fork and the starting +// slot) class IOGConsecutiveTokens : public FormalProperty { public: llvm::json::Value extraInfoToJSON() const override; diff --git a/experimental/include/experimental/Support/IOG.h b/experimental/include/experimental/Support/IOG.h index ea0ced125b..8faac81ee5 100644 --- a/experimental/include/experimental/Support/IOG.h +++ b/experimental/include/experimental/Support/IOG.h @@ -5,19 +5,13 @@ #include "mlir/IR/Value.h" #include -// An In-order graph (IOG) of a dataflow circuit is a subgraph of the dataflow -// circuit. It contains one and only one entry channel (i.e. an argument of a -// FuncOp) which can reach all other operations using only channels part of the -// IOG. The IOG does not lose or gain any tokens: For any merge/mux, all the -// data inputs must be contained in the IOG, and for any fork, only a single -// output can be part of the IOG. Similarly, all branch outputs are part of the -// IOG, and for each join-operation, only a single input is part of the IOG. -// This way, there is a fixed number of tokens within the IOG. - namespace dynamatic { struct IOG; struct IOGPathSet; +// An IOG path set is a structure that describes a set of paths between two +// operations: For any unit `u` within the IOG, it says whether there exists a +// path going through `u` or not. struct IOGPathSet { IOGPathSet(const IOG &iog, Operation *start, Operation *end); @@ -26,6 +20,14 @@ struct IOGPathSet { Operation *end; }; +// An In-order graph (IOG) of a dataflow circuit is a subgraph of the dataflow +// circuit. It contains one and only one entry channel (i.e. an argument of a +// FuncOp) which can reach all other operations using only channels part of the +// IOG. The IOG does not lose or gain any tokens: For any merge/mux, all the +// data inputs must be contained in the IOG, and for any fork, only a single +// output can be part of the IOG. Similarly, all branch outputs are part of the +// IOG, and for each join-operation, only a single input is part of the IOG. +// This way, there is a fixed number of tokens within the IOG. struct IOG { IOG() = default; std::unordered_set units; diff --git a/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp b/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp index 4499dc4035..98dda3837d 100644 --- a/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp +++ b/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp @@ -293,6 +293,11 @@ HandshakeAnnotatePropertiesPass::annotateReconvergentPathFlow(ModuleOp modOp) { } namespace { +// This function finds appropriate fork sent states for the consecutive tokens +// invariant: Given the IOG and a set of paths from a start buffer to an end +// buffer, it determines all forks for which: +// 1. The start buffer is the copied slot of the fork +// 2. The fork is part of a path from start to end along the IOG std::vector findCopiedSents(const IOG &iog, const IOGPathSet &pathSet) { std::vector sents; diff --git a/experimental/lib/Support/IOG.cpp b/experimental/lib/Support/IOG.cpp index c69777bbc9..2af37b2dc9 100644 --- a/experimental/lib/Support/IOG.cpp +++ b/experimental/lib/Support/IOG.cpp @@ -8,6 +8,8 @@ IOGPathSet::IOGPathSet(const IOG &iog, Operation *startA, Operation *endA) std::vector stack; stack.push_back(start); std::unordered_set forward; + // Find all operations reachable by going forward from the start without going + // through the end operation while (!stack.empty()) { Operation *op = stack.back(); stack.pop_back(); @@ -35,6 +37,9 @@ IOGPathSet::IOGPathSet(const IOG &iog, Operation *startA, Operation *endA) stack.push_back(end); std::unordered_set back; + // Find all operations reachable by going backwards from the end without going + // through the start operation (i.e. all operations that can reach the end + // going forward without going through start) while (!stack.empty()) { Operation *op = stack.back(); stack.pop_back(); @@ -62,6 +67,8 @@ IOGPathSet::IOGPathSet(const IOG &iog, Operation *startA, Operation *endA) } } + // Any operation that can be reached from the start, and that can reach the + // end, is part of a path from start to end for (Operation *op : forward) { if (back.find(op) != back.end()) { units.insert(op); @@ -188,7 +195,7 @@ class IOGFinder { // 1. Pick a candidate IOG to work on // 2. Within this IOG, get the next operation that should be added to the IOG // 3. Handle the operation according to local rules, eliminating the candidate - // or splitting into multiple possible possibilities as necessary + // or splitting into multiple possible candidates as necessary void step() { if (candidates.empty()) return; From 7418c16b74317563ea4df5db958f72c237edc3e8 Mon Sep 17 00:00:00 2001 From: Bas Niekel Date: Wed, 6 May 2026 12:46:39 +0200 Subject: [PATCH 19/29] fixed an issue that made smv module arguments mismatch --- experimental/tools/rigidification/rigidification-testbench.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/experimental/tools/rigidification/rigidification-testbench.cpp b/experimental/tools/rigidification/rigidification-testbench.cpp index b5fcd22e1c..271aecff48 100644 --- a/experimental/tools/rigidification/rigidification-testbench.cpp +++ b/experimental/tools/rigidification/rigidification-testbench.cpp @@ -101,6 +101,7 @@ integration-tests/fir/out/hdl/ --mlir intregation-tests/fir/out/comp/hw.mlir/n)D .modelSmvName = kernelName, .nrOfTokens = 1, .generateExactNrOfTokens = true, + .syncOutput = true, .deadBufferOutput = true}; std::string wrapper = From df03adeb60ddfe1cc54cd4b8059a670c18579725 Mon Sep 17 00:00:00 2001 From: Bas Niekel Date: Wed, 6 May 2026 13:48:26 +0200 Subject: [PATCH 20/29] replace template with ValueRange --- experimental/lib/Support/IOG.cpp | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/experimental/lib/Support/IOG.cpp b/experimental/lib/Support/IOG.cpp index 2af37b2dc9..9c11bb8d57 100644 --- a/experimental/lib/Support/IOG.cpp +++ b/experimental/lib/Support/IOG.cpp @@ -297,8 +297,7 @@ class IOGFinder { // c, it pushes the IOG where *only* channel c is taken, and all the rest are // illegal. Used for forks (which only allow exactly one of its outputs) and // join operations (which only allow exactly one of its inputs) - template - void followSingle(const IOGCandidate &checkpoint, T options) { + void followSingle(const IOGCandidate &checkpoint, ValueRange options) { size_t n = 0; mlir::Value singleTaken = nullptr; for (mlir::Value channel : options) { From e1401b5f569824c6ba522235af85cabc2b87d10e Mon Sep 17 00:00:00 2001 From: Bas Niekel Date: Fri, 8 May 2026 14:14:40 +0200 Subject: [PATCH 21/29] Add dead buffer unit to ends of IOGs: Instead of terminating IOGs with sinks, they are now terminated with dead buffers This way, the extra attribute that propagates through handshake -> hw -> python is no longer necessary --- data/rtl-config-smv.json | 7 ++- .../HandshakeAnnotateProperties.cpp | 13 +++++- experimental/lib/Support/IOG.cpp | 2 +- .../smv/generators/handshake/dead_buffer.py | 44 ++++++++++++++++++ .../smv/generators/handshake/sink.py | 46 ++----------------- .../unit-generators/smv/smv-unit-generator.py | 3 ++ .../Dialect/Handshake/HandshakeOps.td | 36 +++++++++++++-- .../HandshakeToHW/HandshakeToHW.cpp | 6 ++- lib/Dialect/Handshake/HandshakeInterfaces.cpp | 9 ++++ .../HandshakeOpInternalStateNamer.cpp | 7 --- lib/Dialect/Handshake/HandshakeOps.cpp | 12 ----- lib/Support/RTL/RTL.cpp | 8 +--- 12 files changed, 116 insertions(+), 77 deletions(-) create mode 100644 experimental/tools/unit-generators/smv/generators/handshake/dead_buffer.py diff --git a/data/rtl-config-smv.json b/data/rtl-config-smv.json index 756849feef..49f00a8098 100644 --- a/data/rtl-config-smv.json +++ b/data/rtl-config-smv.json @@ -89,7 +89,12 @@ }, { "name": "handshake.sink", - "generator": "python $DYNAMATIC/experimental/tools/unit-generators/smv/smv-unit-generator.py -n $MODULE_NAME -o $OUTPUT_DIR/$MODULE_NAME.smv -t sink -p bitwidth=$BITWIDTH iog_terminator=$IOG_TERMINATOR", + "generator": "python $DYNAMATIC/experimental/tools/unit-generators/smv/smv-unit-generator.py -n $MODULE_NAME -o $OUTPUT_DIR/$MODULE_NAME.smv -t sink -p bitwidth=$BITWIDTH", + "hdl": "smv" + }, + { + "name": "handshake.dead_buffer", + "generator": "python $DYNAMATIC/experimental/tools/unit-generators/smv/smv-unit-generator.py -n $MODULE_NAME -o $OUTPUT_DIR/$MODULE_NAME.smv -t dead_buffer -p bitwidth=$BITWIDTH", "hdl": "smv" }, { diff --git a/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp b/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp index 98dda3837d..b78e9663c0 100644 --- a/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp +++ b/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp @@ -488,9 +488,18 @@ void HandshakeAnnotatePropertiesPass::runDynamaticPass() { } for (SinkOp sink : sinks) { - auto unitAttr = UnitAttr::get(modOp.getContext()); - sink->setAttr("IOG_TERMINATOR", unitAttr); + OpBuilder builder(sink); + DeadBufferOp deadBuffer = + builder.create(sink.getLoc(), sink.getOperand()); + sink.erase(); + for (auto &iog : iogs) { + if (iog.contains(sink)) { + iog.units.erase(sink); + iog.units.insert(deadBuffer); + } + } } + getAnalysis().nameAllUnnamedOps(); if (failed(annotateQueriedProperties(iogs))) { return signalPassFailure(); diff --git a/experimental/lib/Support/IOG.cpp b/experimental/lib/Support/IOG.cpp index 9c11bb8d57..8391f2423f 100644 --- a/experimental/lib/Support/IOG.cpp +++ b/experimental/lib/Support/IOG.cpp @@ -261,7 +261,7 @@ class IOGFinder { } else if (auto arithOp = dyn_cast(op)) { candidate.markFollowed(arithOp->getResults()[0]); followSingle(candidate, arithOp->getOperands()); - } else if (isa(op)) { + } else if (isa(op)) { // These act as terminating units, and no further edges need to be // followed candidates.push_back(candidate); diff --git a/experimental/tools/unit-generators/smv/generators/handshake/dead_buffer.py b/experimental/tools/unit-generators/smv/generators/handshake/dead_buffer.py new file mode 100644 index 0000000000..3da9760f4f --- /dev/null +++ b/experimental/tools/unit-generators/smv/generators/handshake/dead_buffer.py @@ -0,0 +1,44 @@ +from generators.support.utils import * + + +def generate_dead_buffer(name, params): + data_type = SmvScalarType(params[ATTR_BITWIDTH]) + + if data_type.bitwidth == 0: + return _generate_dead_buffer_dataless(name) + else: + return _generate_dead_buffer(name, data_type) + + +def _generate_dead_buffer_dataless(name): + return f""" +MODULE {name}(ins_valid) + VAR + full : boolean; + + ASSIGN + init(full) := FALSE; + next(full) := full | ins_valid; + + -- output + DEFINE + ins_ready := !full; + full_full := full; +""" + + +def _generate_dead_buffer(name, data_type): + return f""" +MODULE {name}(ins, ins_valid) + VAR + full : boolean; + + ASSIGN + init(full) := FALSE; + next(full) := full | ins_valid; + + -- output + DEFINE + ins_ready := !full; + full_full := full; +""" diff --git a/experimental/tools/unit-generators/smv/generators/handshake/sink.py b/experimental/tools/unit-generators/smv/generators/handshake/sink.py index 1311a0b97a..fe8c573ac3 100644 --- a/experimental/tools/unit-generators/smv/generators/handshake/sink.py +++ b/experimental/tools/unit-generators/smv/generators/handshake/sink.py @@ -4,50 +4,10 @@ def generate_sink(name, params): data_type = SmvScalarType(params[ATTR_BITWIDTH]) - if params["iog_terminator"]: - if data_type.bitwidth == 0: - return _generate_iog_terminator_dataless(name) - else: - return _generate_iog_terminator(name, data_type) + if data_type.bitwidth == 0: + return _generate_sink_dataless(name) else: - if data_type.bitwidth == 0: - return _generate_sink_dataless(name) - else: - return _generate_sink(name, data_type) - - -def _generate_iog_terminator_dataless(name): - return f""" -MODULE {name}(ins_valid) - VAR - full : boolean; - - ASSIGN - init(full) := FALSE; - next(full) := full | ins_valid; - - -- output - DEFINE - ins_ready := !full; - full_full := full; -""" - - -def _generate_iog_terminator(name, data_type): - return f""" -MODULE {name}(ins, ins_valid) - VAR - full : boolean; - - ASSIGN - init(full) := FALSE; - next(full) := full | ins_valid; - - -- output - DEFINE - ins_ready := !full; - full_full := full; -""" + return _generate_sink(name, data_type) def _generate_sink_dataless(name): diff --git a/experimental/tools/unit-generators/smv/smv-unit-generator.py b/experimental/tools/unit-generators/smv/smv-unit-generator.py index 5638cecca2..b7e89d4537 100644 --- a/experimental/tools/unit-generators/smv/smv-unit-generator.py +++ b/experimental/tools/unit-generators/smv/smv-unit-generator.py @@ -16,6 +16,7 @@ import generators.handshake.mux as mux import generators.handshake.select as select import generators.handshake.sink as sink +import generators.handshake.dead_buffer as dead_buffer import generators.handshake.source as source import generators.handshake.store as store import generators.handshake.ndwire as ndwire @@ -82,6 +83,8 @@ def generate_code(name, mod_type, parameters): return select.generate_select(name, parameters) case "sink": return sink.generate_sink(name, parameters) + case "dead_buffer": + return dead_buffer.generate_dead_buffer(name, parameters) case "source": return source.generate_source(name, parameters) case "store": diff --git a/include/dynamatic/Dialect/Handshake/HandshakeOps.td b/include/dynamatic/Dialect/Handshake/HandshakeOps.td index 06b4850823..6308f041da 100644 --- a/include/dynamatic/Dialect/Handshake/HandshakeOps.td +++ b/include/dynamatic/Dialect/Handshake/HandshakeOps.td @@ -709,10 +709,6 @@ def SinkOp : Handshake_Op<"sink"> { ``` }]; - let extraClassDeclaration = [{ - bool terminatesIOG(); - BufferSlotFullNamer getTerminatingSlot(); - }]; let arguments = (ins HandshakeType:$operand); let assemblyFormat = [{ $operand attr-dict `:` custom(type($operand)) @@ -730,6 +726,38 @@ def SinkOp : Handshake_Op<"sink"> { }]; } +def DeadBufferOp : Handshake_Op<"dead_buffer", [ + DeclareOpInterfaceMethods + ]> { + let summary = "buffer operation without successor"; + let description = [{ + The dead buffer operation stores an incoming token in its slot, and + then stops accepting tokens. + + Example: + + ```mlir + dead_buffer %data : !handshake.channel + ``` + }]; + + let arguments = (ins HandshakeType:$operand); + let assemblyFormat = [{ + $operand attr-dict `:` custom(type($operand)) + }]; + + let extraClassDefinition = [{ + ::mlir::FailureOr<::llvm::SmallVector<::mlir::NamedAttribute>> + DeadBufferOp::getRTLParameters() { + ::mlir::MLIRContext *ctx = (*this)->getContext(); + return ::llvm::SmallVector<::mlir::NamedAttribute>{ + {::mlir::StringAttr::get(ctx, "BITWIDTH"), + ::mlir::TypeAttr::get(getOperand().getType())} + }; + } + }]; +} + def SourceOp : Handshake_Op<"source", [Pure]> { let summary = "source operation"; let description = [{ diff --git a/lib/Conversion/HandshakeToHW/HandshakeToHW.cpp b/lib/Conversion/HandshakeToHW/HandshakeToHW.cpp index f929b75352..416405699f 100644 --- a/lib/Conversion/HandshakeToHW/HandshakeToHW.cpp +++ b/lib/Conversion/HandshakeToHW/HandshakeToHW.cpp @@ -588,7 +588,10 @@ ModuleDiscriminator::ModuleDiscriminator(Operation *op) { .Case([&](auto) { // Bitwidth addType("DATA_TYPE", op->getOperand(0)); - addBoolean("IOG_TERMINATOR", op->hasAttr("IOG_TERMINATOR")); + }) + .Case([&](auto) { + // Bitwidth + addType("DATA_TYPE", op->getOperand(0)); }) .Case([&](auto) { // Bitwidth @@ -2150,6 +2153,7 @@ class HandshakeToHWPass ConvertToHWInstance, ConvertToHWInstance, ConvertToHWInstance, + ConvertToHWInstance, ConvertToHWInstance, ConvertToHWInstance, ConvertToHWInstance, diff --git a/lib/Dialect/Handshake/HandshakeInterfaces.cpp b/lib/Dialect/Handshake/HandshakeInterfaces.cpp index bf538eb6d1..e7c517fd97 100644 --- a/lib/Dialect/Handshake/HandshakeInterfaces.cpp +++ b/lib/Dialect/Handshake/HandshakeInterfaces.cpp @@ -460,6 +460,15 @@ std::vector BufferOp::getInternalSlotStateNamers() { } return ret; } +std::vector DeadBufferOp::getInternalSlotStateNamers() { + StringAttr nameAttr = + getOperation()->getAttrOfType(NameAnalysis::ATTR_NAME); + assert(nameAttr && + "Cannot get names of slot states for operation without name"); + std::vector ret; + ret.emplace_back(nameAttr.str(), "TMP_DEADBUFFERSLOT", 0); + return ret; +} //===----------------------------------------------------------------------===// // ShiftLikeArithOpInterface diff --git a/lib/Dialect/Handshake/HandshakeOpInternalStateNamer.cpp b/lib/Dialect/Handshake/HandshakeOpInternalStateNamer.cpp index dc5501fe70..edc4f90f79 100644 --- a/lib/Dialect/Handshake/HandshakeOpInternalStateNamer.cpp +++ b/lib/Dialect/Handshake/HandshakeOpInternalStateNamer.cpp @@ -235,13 +235,6 @@ getAllSlotsOfOperation(Operation *op) { ret.push_back(std::make_unique(slot)); } } - if (auto sinkOp = dyn_cast(op)) { - if (sinkOp.terminatesIOG()) { - ret.push_back( - std::make_unique(sinkOp.getTerminatingSlot())); - } - return ret; - } if (auto endOp = dyn_cast(op)) { ret.push_back(std::make_unique("testbench", "end", 0)); diff --git a/lib/Dialect/Handshake/HandshakeOps.cpp b/lib/Dialect/Handshake/HandshakeOps.cpp index a18b3f2230..94a27db12f 100644 --- a/lib/Dialect/Handshake/HandshakeOps.cpp +++ b/lib/Dialect/Handshake/HandshakeOps.cpp @@ -654,18 +654,6 @@ LogicalResult ConstantOp::verify() { } bool JoinOp::isControl() { return true; } -bool SinkOp::terminatesIOG() { - return getOperation()->hasAttr("IOG_TERMINATOR"); -} - -BufferSlotFullNamer SinkOp::getTerminatingSlot() { - assert(terminatesIOG()); - Operation *op = getOperation(); - std::string name = - op->getAttrOfType<::mlir::StringAttr>(NameAnalysis::ATTR_NAME).str(); - return BufferSlotFullNamer(name, "full", 0); -} - /// Based on mlir::func::CallOp::verifySymbolUses LogicalResult InstanceOp::verifySymbolUses(SymbolTableCollection &symbolTable) { // Check that the module attribute was specified. diff --git a/lib/Support/RTL/RTL.cpp b/lib/Support/RTL/RTL.cpp index 3833792bb9..560c66113f 100644 --- a/lib/Support/RTL/RTL.cpp +++ b/lib/Support/RTL/RTL.cpp @@ -286,12 +286,6 @@ LogicalResult RTLMatch::registerParameters(hw::HWModuleExternOp &modOp) { modOp->template getAttrOfType(RTL_NAME_ATTR_NAME).getValue(); auto modType = modOp.getModuleType(); - if (handshakeOp == "handshake.sink") { - bool x = modOp->getAttrOfType(RTL_PARAMETERS_ATTR_NAME) - .contains("IOG_TERMINATOR"); - serializedParams["IOG_TERMINATOR"] = x ? "True" : "False"; - } - LogicalResult gotBitwidth = registerBitwidthParameter(modOp, handshakeOp, modType); LogicalResult gotExtraSignals = @@ -315,6 +309,7 @@ LogicalResult RTLMatch::registerBitwidthParameter(hw::HWModuleExternOp &modOp, handshakeOp == "handshake.merge" || handshakeOp == "handshake.muli" || handshakeOp == "handshake.sink" || + handshakeOp == "handshake.dead_buffer" || handshakeOp == "handshake.subi" || handshakeOp == "handshake.shli" || handshakeOp == "handshake.blocker" || @@ -457,6 +452,7 @@ RTLMatch::registerExtraSignalParameters(hw::HWModuleExternOp &modOp, handshakeOp == "handshake.muli" || handshakeOp == "handshake.select" || handshakeOp == "handshake.sink" || + handshakeOp == "handshake.dead_buffer" || handshakeOp == "handshake.subf" || handshakeOp == "handshake.extui" || handshakeOp == "handshake.shli" || From 4dbefdec2cd4b7ba8de87868ffb7ac6b48f9aca0 Mon Sep 17 00:00:00 2001 From: Bas Niekel Date: Fri, 8 May 2026 15:35:19 +0200 Subject: [PATCH 22/29] fixed some bugs due to merge --- lib/Dialect/Handshake/HandshakeInterfaces.cpp | 2 +- lib/Dialect/Handshake/HandshakeOpInternalStateNamer.cpp | 3 ++- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/lib/Dialect/Handshake/HandshakeInterfaces.cpp b/lib/Dialect/Handshake/HandshakeInterfaces.cpp index 184c0c083d..4739f76513 100644 --- a/lib/Dialect/Handshake/HandshakeInterfaces.cpp +++ b/lib/Dialect/Handshake/HandshakeInterfaces.cpp @@ -494,7 +494,7 @@ std::vector DeadBufferOp::getInternalSlotStateNamers() { assert(nameAttr && "Cannot get names of slot states for operation without name"); std::vector ret; - ret.emplace_back(nameAttr.str(), "TMP_DEADBUFFERSLOT", 0); + ret.emplace_back(nameAttr.str(), "full", "", 0); return ret; } diff --git a/lib/Dialect/Handshake/HandshakeOpInternalStateNamer.cpp b/lib/Dialect/Handshake/HandshakeOpInternalStateNamer.cpp index 865271f26f..eaa6400b3b 100644 --- a/lib/Dialect/Handshake/HandshakeOpInternalStateNamer.cpp +++ b/lib/Dialect/Handshake/HandshakeOpInternalStateNamer.cpp @@ -238,7 +238,8 @@ getAllSlotsOfOperation(Operation *op) { } if (auto endOp = dyn_cast(op)) { - ret.push_back(std::make_unique("testbench", "end", 0)); + ret.push_back( + std::make_unique("testbench", "end", "", 0)); } if (auto loadOp = dyn_cast(op)) { // TODO: Handle LoadOp for MC slot From d0d5f97f53dd1d2fa9694438e5d56d30aa781b55 Mon Sep 17 00:00:00 2001 From: Bas Niekel Date: Fri, 8 May 2026 15:46:11 +0200 Subject: [PATCH 23/29] fixed test case to without attribute --- test/Conversion/HandshakeToHW/types.mlir | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/Conversion/HandshakeToHW/types.mlir b/test/Conversion/HandshakeToHW/types.mlir index ec7161153a..70e692511b 100644 --- a/test/Conversion/HandshakeToHW/types.mlir +++ b/test/Conversion/HandshakeToHW/types.mlir @@ -7,7 +7,7 @@ // CHECK: hw.instance "sink0" @handshake_sink_0(ins: %[[VAL_0]]: !handshake.channel, clk: %[[VAL_2]]: i1, rst: %[[VAL_3]]: i1) -> () // CHECK: hw.output %[[VAL_1]] : !handshake.control<> // CHECK: } -// CHECK: hw.module.extern @handshake_sink_0(in %[[VAL_5:.*]] : !handshake.channel, in %[[VAL_6:.*]] : i1, in %[[VAL_7:.*]] : i1) attributes {hw.name = "handshake.sink", hw.parameters = {DATA_TYPE = !handshake.channel, IOG_TERMINATOR = {{(true|false)}}}} +// CHECK: hw.module.extern @handshake_sink_0(in %[[VAL_5:.*]] : !handshake.channel, in %[[VAL_6:.*]] : i1, in %[[VAL_7:.*]] : i1) attributes {hw.name = "handshake.sink", hw.parameters = {DATA_TYPE = !handshake.channel}} handshake.func @dontChangeTypes(%arg : !handshake.channel, %start: !handshake.control<>) -> !handshake.control<> { sink %arg : end %start : <> From 833fcefe184316df1f3d211bcdd456b4db17d83a Mon Sep 17 00:00:00 2001 From: Bas Niekel Date: Sat, 9 May 2026 13:13:48 +0200 Subject: [PATCH 24/29] flow expresssions now handle dead buffer op --- .../include/experimental/Support/FlowExpression.h | 1 + experimental/lib/Support/FlowExpression.cpp | 14 ++++++++++++++ 2 files changed, 15 insertions(+) diff --git a/experimental/include/experimental/Support/FlowExpression.h b/experimental/include/experimental/Support/FlowExpression.h index 02b43966a7..144d662f36 100644 --- a/experimental/include/experimental/Support/FlowExpression.h +++ b/experimental/include/experimental/Support/FlowExpression.h @@ -308,6 +308,7 @@ struct FlowEquationExtractor { LogicalResult extractBufferOp(BufferOp bufferOp); LogicalResult extractControlMergeOp(ControlMergeOp cmergeOp); LogicalResult extractEndOp(EndOp endOp); + LogicalResult extractDeadBufferOp(DeadBufferOp deadBufferOp); LogicalResult extractForkOp(ForkOp forkOp); LogicalResult extractLoadOp(LoadOp loadOp); LogicalResult extractMemoryControllerOp(MemoryControllerOp memCon); diff --git a/experimental/lib/Support/FlowExpression.cpp b/experimental/lib/Support/FlowExpression.cpp index 550ca1803e..ca0335d960 100644 --- a/experimental/lib/Support/FlowExpression.cpp +++ b/experimental/lib/Support/FlowExpression.cpp @@ -268,6 +268,10 @@ LogicalResult FlowEquationExtractor::extractAll(ModuleOp modOp) { } else if (isa(op)) { // These operations do not place any constraint on incoming/outgoing // lambda channels, and can safely be ignored + } else if (auto deadBufferOp = dyn_cast(op)) { + if (failed(extractDeadBufferOp(deadBufferOp))) { + res = failure(); + } } else if (auto forkOp = dyn_cast(op)) { if (failed(extractForkOp(forkOp))) { res = failure(); @@ -551,6 +555,16 @@ LogicalResult FlowEquationExtractor::extractEndOp(EndOp endOp) { return success(); } +LogicalResult +FlowEquationExtractor::extractDeadBufferOp(DeadBufferOp deadBufferOp) { + FlowVariable in(indexChannelAnalysis, + ChannelLambda(deadBufferOp.getOperand())); + auto slot = FlowVariable( + FlowInternalState(deadBufferOp.getInternalSlotStateNamers()[0])); + equations.push_back(in - slot); + return success(); +} + LogicalResult FlowEquationExtractor::extractForkOp(ForkOp forkOp) { // The input is propagated to all outputs according to eager fork rules FlowVariable in(indexChannelAnalysis, ChannelLambda(forkOp.getOperand())); From 5ed765b88d607f7b24b1ce94490f0c4fd9ff8911 Mon Sep 17 00:00:00 2001 From: Bas Niekel Date: Sat, 9 May 2026 13:37:54 +0200 Subject: [PATCH 25/29] resolved merge-conflicts --- experimental/lib/Support/FlowExpression.cpp | 26 +- experimental/lib/Support/FormalProperty.cpp | 142 ++-------- .../smv/generators/handshake/dead_buffer.py | 4 +- .../Handshake/HandshakeOpInternalStateNamer.h | 107 ++++---- .../HandshakeOpInternalStateNamer.cpp | 253 ++++++++++-------- 5 files changed, 230 insertions(+), 302 deletions(-) diff --git a/experimental/lib/Support/FlowExpression.cpp b/experimental/lib/Support/FlowExpression.cpp index ca0335d960..90ce6d3687 100644 --- a/experimental/lib/Support/FlowExpression.cpp +++ b/experimental/lib/Support/FlowExpression.cpp @@ -145,7 +145,7 @@ llvm::json::Value FlowExpression::toJSON() const { } // int pm = key.pm; jsonTerms.emplace_back( - llvm::json::Object({{STATE_LIT, state->namer->toJSON()}, + llvm::json::Object({{STATE_LIT, state->namer}, {COEFFICIENT_LIT, value}, {CONSTRAINT_LIT, constraintJson}})); } @@ -158,22 +158,16 @@ FlowExpression FlowExpression::fromJSON(const llvm::json::Value &value, const llvm::json::Array *arr = value.getAsArray(); assert(arr && "FlowExpression JSON is not an array"); for (const llvm::json::Value &termJSON : *arr) { - const llvm::json::Object *obj = termJSON.getAsObject(); - assert(obj && "FlowExpression term JSON not an object"); - const llvm::json::Value *state = obj->get(STATE_LIT); - if (!state) { - llvm::report_fatal_error( - "FlowExpression term JSON does not contain STATE_LIT"); - } - std::shared_ptr namer = - InternalStateNamer::fromJSON(*state, path); - FlowVariable var = FlowVariable(FlowInternalState(namer)); - int coef; llvm::json::ObjectMapper mapper(termJSON, path); - if (!mapper || !mapper.map(COEFFICIENT_LIT, coef)) { - llvm::report_fatal_error( - "FlowExpression term JSON does not contain COEFFICIENT_LIT"); - } + std::unique_ptr namer; + int coef; + if (!mapper || !mapper.map(STATE_LIT, namer) || + !mapper.map(COEFFICIENT_LIT, coef)) + llvm::report_fatal_error("Failed FlowExpression term mapping"); + std::shared_ptr sharedNamer = std::move(namer); + FlowVariable var = FlowVariable(FlowInternalState(sharedNamer)); + + auto *obj = termJSON.getAsObject(); const llvm::json::Value *constraint = obj->get(CONSTRAINT_LIT); assert(constraint && "FlowExpression does not contain CONSTRAINT_LIT"); if (auto n = constraint->getAsNull()) { diff --git a/experimental/lib/Support/FormalProperty.cpp b/experimental/lib/Support/FormalProperty.cpp index 6ded93e1ee..f48f847bbe 100644 --- a/experimental/lib/Support/FormalProperty.cpp +++ b/experimental/lib/Support/FormalProperty.cpp @@ -264,11 +264,6 @@ EagerForkNotAllOutputSent::EagerForkNotAllOutputSent( } llvm::json::Value EagerForkNotAllOutputSent::extraInfoToJSON() const { - std::vector channels{}; - // std::string opName = sentStateNamers[0].opName; - for (auto [i, state] : llvm::enumerate(sentStateNamers)) { - channels.push_back(state.toInnerJSON()); - } // Example JSON: // [ // { @@ -292,7 +287,7 @@ llvm::json::Value EagerForkNotAllOutputSent::extraInfoToJSON() const { // "operation": "fork0", // } // ] - return llvm::json::Array(channels); + return llvm::json::Array(sentStateNamers); } std::unique_ptr @@ -301,14 +296,8 @@ EagerForkNotAllOutputSent::fromJSON(const llvm::json::Value &value, auto prop = std::make_unique(); auto info = prop->parseBaseAndExtractInfo(value, path); - llvm::json::Array *array = info.getAsArray(); - assert(array && - "expected info of EFNAO to be an array of eager fork outputs"); - for (auto &stateJSON : *array) { - auto sentStateNamer = - handshake::EagerForkSentNamer::fromInnerJSON(stateJSON, path); - prop->sentStateNamers.push_back(*sentStateNamer); - } + bool success = llvm::json::fromJSON(info, prop->sentStateNamers, path); + assert(success); return prop; } @@ -335,12 +324,8 @@ CopiedSlotsOfActiveForkAreFull::CopiedSlotsOfActiveForkAreFull( } llvm::json::Value CopiedSlotsOfActiveForkAreFull::extraInfoToJSON() const { - std::vector channels{}; - for (auto [i, state] : llvm::enumerate(sentStateNamers)) { - channels.push_back(state.toInnerJSON()); - } return llvm::json::Object( - {{FORK_CHANNELS_LIT, channels}, {COPIED_SLOT_LIT, copiedSlot->toJSON()}}); + {{FORK_CHANNELS_LIT, sentStateNamers}, {COPIED_SLOT_LIT, copiedSlot}}); } std::unique_ptr @@ -350,22 +335,10 @@ CopiedSlotsOfActiveForkAreFull::fromJSON(const llvm::json::Value &value, auto info = prop->parseBaseAndExtractInfo(value, path); - const llvm::json::Object *obj = info.getAsObject(); - assert(obj && "CSOAFAF json info not an object"); - - const llvm::json::Value *channelNameJSON = obj->get(FORK_CHANNELS_LIT); - assert(channelNameJSON && "missing FORK_CHANNELS_LIT in CSOAFAF info"); - const llvm::json::Array *channelNameJSONs = channelNameJSON->getAsArray(); - assert(channelNameJSONs && "FORK_CHANNELS_LIT in CSOAFAF is not an array"); - for (auto &sentJSON : *channelNameJSONs) { - prop->sentStateNamers.push_back( - *handshake::EagerForkSentNamer::fromInnerJSON(sentJSON, path)); - } - - const llvm::json::Value *bufferSlotJSON = obj->get(COPIED_SLOT_LIT); - assert(bufferSlotJSON && "missing COPIED_SLOT_LIT in CSOAFAF json"); - prop->copiedSlot = InternalStateNamer::fromJSON(*bufferSlotJSON, path); - + llvm::json::ObjectMapper mapper(info, path); + if (!mapper || !mapper.map(FORK_CHANNELS_LIT, prop->sentStateNamers) || + !mapper.map(COPIED_SLOT_LIT, prop->copiedSlot)) + return nullptr; return prop; } @@ -404,21 +377,7 @@ ReconvergentPathFlow::fromJSON(const llvm::json::Value &value, // IOGSingleToken llvm::json::Value IOGSingleToken::extraInfoToJSON() const { - std::vector slotsJSON; - slotsJSON.reserve(slots.size()); - for (auto &namer : slots) { - slotsJSON.push_back(namer->toJSON()); - } - llvm::json::Value slotsValue = slotsJSON; - - std::vector forksJSON; - forksJSON.reserve(forks.size()); - for (auto &sent : forks) { - forksJSON.push_back(sent.toInnerJSON()); - } - llvm::json::Value forksValue = forksJSON; - - return llvm::json::Object({{SLOTS_LIT, slotsValue}, {FORKS_LIT, forksValue}}); + return llvm::json::Object({{SLOTS_LIT, slots}, {FORKS_LIT, forks}}); } std::unique_ptr @@ -427,50 +386,18 @@ IOGSingleToken::fromJSON(const llvm::json::Value &value, auto prop = std::make_unique(); llvm::json::Value info = prop->parseBaseAndExtractInfo(value, path); - llvm::json::Object *obj = info.getAsObject(); - assert(obj); - if (auto iter = obj->find(SLOTS_LIT); iter != obj->end()) { - llvm::json::Array *slotsArray = iter->second.getAsArray(); - assert(slotsArray); - prop->slots.reserve(slotsArray->size()); - for (const llvm::json::Value &sentValue : *slotsArray) { - auto json = InternalStateNamer::fromJSON(sentValue, path); - assert(json); - prop->slots.push_back(std::move(json)); - } - } else { - path.report(json::ERR_MISSING_VALUE); - return nullptr; - } - if (auto iter = obj->find(FORKS_LIT); iter != obj->end()) { - llvm::json::Array *forksArray = iter->second.getAsArray(); - assert(forksArray); - prop->forks.reserve(forksArray->size()); - for (const llvm::json::Value &sentValue : *forksArray) { - auto innerJSON = EagerForkSentNamer::fromInnerJSON(sentValue, path); - assert(innerJSON); - prop->forks.push_back(*innerJSON); - } - } else { - path.report(json::ERR_MISSING_VALUE); + llvm::json::ObjectMapper mapper(info, path); + if (!mapper || !mapper.map(SLOTS_LIT, prop->slots) || + !mapper.map(FORKS_LIT, prop->forks)) return nullptr; - } return prop; } // IOGConsecutiveTokens llvm::json::Value IOGConsecutiveTokens::extraInfoToJSON() const { - std::vector sentsJSON; - sentsJSON.reserve(sents.size()); - for (auto &sent : sents) { - sentsJSON.push_back(sent.toInnerJSON()); - } - llvm::json::Value sentsValue = sentsJSON; - - return llvm::json::Object({{SLOT1_LIT, slot1->toJSON()}, - {SLOT2_LIT, slot2->toJSON()}, - {SENTS_LIT, sentsValue}}); + return llvm::json::Object( + {{SLOT1_LIT, slot1}, {SLOT2_LIT, slot2}, {SENTS_LIT, sents}}); } std::unique_ptr @@ -479,44 +406,11 @@ IOGConsecutiveTokens::fromJSON(const llvm::json::Value &value, auto prop = std::make_unique(); llvm::json::Value info = prop->parseBaseAndExtractInfo(value, path); - llvm::json::Object *obj = info.getAsObject(); - assert(obj); - if (auto iter = obj->find(SLOT1_LIT); iter != obj->end()) { - prop->slot1 = InternalStateNamer::fromJSON(iter->second, path); - } else { - path.report(json::ERR_MISSING_VALUE); - return nullptr; - } - - if (auto iter = obj->find(SLOT2_LIT); iter != obj->end()) { - prop->slot2 = InternalStateNamer::fromJSON(iter->second, path); - } else { - path.report(json::ERR_MISSING_VALUE); - return nullptr; - } - - if (auto iter = obj->find(SENTS_LIT); iter != obj->end()) { - llvm::json::Array *sentsArray = iter->second.getAsArray(); - assert(sentsArray); - prop->sents.reserve(sentsArray->size()); - for (const llvm::json::Value &sentValue : *sentsArray) { - auto innerJSON = EagerForkSentNamer::fromInnerJSON(sentValue, path); - assert(innerJSON); - prop->sents.push_back(*innerJSON); - } - } else { - path.report(json::ERR_MISSING_VALUE); - } - - /* - auto prop = std::make_unique(); - auto info = prop->parseBaseAndExtractInfo(value, path); - - const llvm::json::Object *obj = info.getAsObject(); - if (!obj) + llvm::json::ObjectMapper mapper(info, path); + if (!mapper || !mapper.map(SLOT1_LIT, prop->slot1) || + !mapper.map(SLOT2_LIT, prop->slot2) || + !mapper.map(SENTS_LIT, prop->sents)) return nullptr; - assert(false && "TODO"); - */ return prop; } diff --git a/experimental/tools/unit-generators/smv/generators/handshake/dead_buffer.py b/experimental/tools/unit-generators/smv/generators/handshake/dead_buffer.py index 3da9760f4f..650eab3293 100644 --- a/experimental/tools/unit-generators/smv/generators/handshake/dead_buffer.py +++ b/experimental/tools/unit-generators/smv/generators/handshake/dead_buffer.py @@ -23,7 +23,7 @@ def _generate_dead_buffer_dataless(name): -- output DEFINE ins_ready := !full; - full_full := full; + slotted_token_count := count(full); """ @@ -40,5 +40,5 @@ def _generate_dead_buffer(name, data_type): -- output DEFINE ins_ready := !full; - full_full := full; + slotted_token_count := count(full); """ diff --git a/include/dynamatic/Dialect/Handshake/HandshakeOpInternalStateNamer.h b/include/dynamatic/Dialect/Handshake/HandshakeOpInternalStateNamer.h index cbe31575a1..b783e70807 100644 --- a/include/dynamatic/Dialect/Handshake/HandshakeOpInternalStateNamer.h +++ b/include/dynamatic/Dialect/Handshake/HandshakeOpInternalStateNamer.h @@ -51,24 +51,16 @@ struct InternalStateNamer { virtual std::string getSMVName() const = 0; virtual llvm::json::Value toInnerJSON() const = 0; - inline llvm::json::Value toJSON() const { - // Example: - // { - // "type": "EagerForkSent", - // "inner": { - // "operation": "fork1", - // "channel_name": "outs_1", - // "channel_size": 2 - // } - // } - return llvm::json::Object({ - {TYPE_LIT, typeToStr(type)}, - {INNER_LIT, toInnerJSON()}, - }); - } - - std::unique_ptr static fromJSON( - const llvm::json::Value &value, llvm::json::Path path); + friend llvm::json::Value + toJSON(const std::unique_ptr &namer); + friend llvm::json::Value + toJSON(const std::shared_ptr &namer); + friend bool fromJSON(const llvm::json::Value &value, + std::unique_ptr &namer, + llvm::json::Path path); + friend bool fromJSON(const llvm::json::Value &value, + std::shared_ptr &namer, + llvm::json::Path path); InternalStateNamer() = default; InternalStateNamer(TYPE type) : type(type) {} @@ -109,24 +101,27 @@ struct ConstrainedNamer : InternalStateNamer { // This assumes the internal state being named is represented as an object. // Example for fork8 output 0 constrained to 0: // { - // "channel_name": "outs_0", - // "channel_size": 1, - // "operation": "fork8", + // "inner": { + // "channel_name": "outs_0", + // "channel_size": 1, + // "operation": "fork8", + // }, + // "type": "EagerForkSent", // "value": 0 // } - llvm::json::Object *objP = getUnconstrained()->toJSON().getAsObject(); - assert(objP && "internal state namer is a json object"); + llvm::json::Object *objP = toJSON(getUnconstrained()).getAsObject(); + assert(objP && "internal state namer should be a json object"); llvm::json::Object &obj = *objP; - obj[CONSTRAINT_VALUE] = value; + obj[CONSTRAINT_VALUE_LIT] = value; return llvm::json::Object(obj); } - - std::unique_ptr static fromInnerJSON( - const llvm::json::Value &value, llvm::json::Path path); + friend bool fromJSON(const llvm::json::Value &value, ConstrainedNamer &namer, + llvm::json::Path path); int32_t value; - static constexpr llvm::StringLiteral CONSTRAINT_VALUE = "value"; + static constexpr llvm::StringLiteral CONSTRAINT_VALUE_LIT = + "constrained_value"; }; // To define a `sent` state of an eager fork, the exact channel that contains @@ -155,8 +150,8 @@ struct EagerForkSentNamer : InternalStateNamer { {CHANNEL_SIZE_LIT, channelSize}}); } - std::unique_ptr static fromInnerJSON( - const llvm::json::Value &value, llvm::json::Path path); + friend bool fromJSON(const llvm::json::Value &value, + EagerForkSentNamer &namer, llvm::json::Path path); std::string opName; std::string channelName; @@ -233,8 +228,8 @@ struct BufferSlotFullNamer : InternalStateNamer { }); } - std::unique_ptr static fromInnerJSON( - const llvm::json::Value &value, llvm::json::Path path); + friend bool fromJSON(const llvm::json::Value &value, + BufferSlotFullNamer &namer, llvm::json::Path path); std::string opName; std::string slotName; @@ -261,11 +256,6 @@ struct ConstrainedBufferSlotFullNamer : ConstrainedNamer { .str(); } - inline llvm::json::Value toInnerJSON() const override { - llvm::json::Value obj = base.toInnerJSON(); - return llvm::json::Object({{BASE_LIT, obj}, {VALUE_LIT, value}}); - } - inline std::unique_ptr getUnconstrained() const override { return std::make_unique(base); } @@ -299,8 +289,9 @@ struct PipelineSlotNamer : InternalStateNamer { {{OPERATION_LIT, opName}, {SLOT_INDEX_LIT, slotIndex}}); } - std::unique_ptr static fromInnerJSON( - const llvm::json::Value &value, llvm::json::Path path); + friend bool fromJSON(const llvm::json::Value &value, PipelineSlotNamer &namer, + llvm::json::Path path); + std::string opName; unsigned slotIndex; static constexpr llvm::StringLiteral OPERATION_LIT = "operation"; @@ -327,8 +318,8 @@ struct PipelineTokenCountNamer : InternalStateNamer { return llvm::json::Object({{OPERATION_LIT, opName}}); } - std::unique_ptr static fromInnerJSON( - const llvm::json::Value &value, llvm::json::Path path); + friend bool fromJSON(const llvm::json::Value &value, + PipelineTokenCountNamer &namer, llvm::json::Path path); std::string opName; static constexpr llvm::StringLiteral OPERATION_LIT = "operation"; @@ -352,8 +343,8 @@ struct TokenCountNamer : InternalStateNamer { return llvm::json::Object({{OPERATION_LIT, opName}}); } - std::unique_ptr static fromInnerJSON( - const llvm::json::Value &value, llvm::json::Path path); + friend bool fromJSON(const llvm::json::Value &value, TokenCountNamer &namer, + llvm::json::Path path); std::string opName; static constexpr llvm::StringLiteral OPERATION_LIT = "operation"; @@ -395,8 +386,8 @@ struct MemoryControllerSlotNamer : InternalStateNamer { {PORT_TYPE_LIT, (int)portType}, {LOADLESS_LIT, loadless}}); } - std::unique_ptr static fromInnerJSON( - const llvm::json::Value &value, llvm::json::Path path); + friend bool fromJSON(const llvm::json::Value &value, + MemoryControllerSlotNamer &namer, llvm::json::Path path); std::string opName; size_t slotIndex; @@ -430,11 +421,33 @@ struct EntrySlotNamer : InternalStateNamer { inline llvm::json::Value toInnerJSON() const override { return llvm::json::Object({{ARG_NAME_LIT, argName}}); } - std::unique_ptr static fromInnerJSON( - const llvm::json::Value &value, llvm::json::Path path); + + friend bool fromJSON(const llvm::json::Value &value, EntrySlotNamer &namer, + llvm::json::Path path); + std::string argName; static constexpr llvm::StringLiteral ARG_NAME_LIT = "arg_name"; }; +// Specialize llvm::json toJSON template for each namer so that they can be +// converted to json automatically by llvm where necessary +inline llvm::json::Value toJSON(const EagerForkSentNamer &namer) { + return namer.toInnerJSON(); +} +inline llvm::json::Value toJSON(const BufferSlotFullNamer &namer) { + return namer.toInnerJSON(); +} +inline llvm::json::Value toJSON(const PipelineSlotNamer &namer) { + return namer.toInnerJSON(); +} +inline llvm::json::Value toJSON(const MemoryControllerSlotNamer &namer) { + return namer.toInnerJSON(); +} +inline llvm::json::Value toJSON(const ConstrainedNamer &namer) { + return namer.toInnerJSON(); +} +inline llvm::json::Value toJSON(const EntrySlotNamer &namer) { + return namer.toInnerJSON(); +} } // namespace handshake } // namespace dynamatic diff --git a/lib/Dialect/Handshake/HandshakeOpInternalStateNamer.cpp b/lib/Dialect/Handshake/HandshakeOpInternalStateNamer.cpp index eaa6400b3b..6b25caca56 100644 --- a/lib/Dialect/Handshake/HandshakeOpInternalStateNamer.cpp +++ b/lib/Dialect/Handshake/HandshakeOpInternalStateNamer.cpp @@ -1,6 +1,7 @@ #include "dynamatic/Dialect/Handshake/HandshakeOpInternalStateNamer.h" #include "dynamatic/Dialect/Handshake/HandshakeInterfaces.h" #include "dynamatic/Dialect/Handshake/HandshakeOps.h" +#include "llvm/Support/Casting.h" namespace dynamatic { namespace handshake { @@ -47,60 +48,111 @@ std::string InternalStateNamer::typeToStr(TYPE t) { } } -std::unique_ptr -InternalStateNamer::fromJSON(const llvm::json::Value &value, - llvm::json::Path path) { +llvm::json::Value toJSON(const std::unique_ptr &namer) { + // Example: + // { + // "type": "EagerForkSent", + // "inner": { + // "operation": "fork1", + // "channel_name": "outs_1", + // "channel_size": 2 + // } + // } + return llvm::json::Object({ + {InternalStateNamer::TYPE_LIT, + InternalStateNamer::typeToStr(namer->type)}, + {InternalStateNamer::INNER_LIT, namer->toInnerJSON()}, + }); +} + +llvm::json::Value toJSON(const std::shared_ptr &namer) { + return llvm::json::Object({ + {InternalStateNamer::TYPE_LIT, + InternalStateNamer::typeToStr(namer->type)}, + {InternalStateNamer::INNER_LIT, namer->toInnerJSON()}, + }); +} + +bool fromJSON(const llvm::json::Value &value, + std::shared_ptr &namer, + llvm::json::Path path) { + std::unique_ptr unique; + + if (!fromJSON(value, unique, path)) + return false; + namer = std::move(unique); + return true; +} + +bool fromJSON(const llvm::json::Value &value, + std::unique_ptr &namer, + llvm::json::Path path) { std::string typeStr; llvm::json::ObjectMapper mapper(value, path); - if (!mapper || !mapper.map(TYPE_LIT, typeStr)) - return nullptr; + if (!mapper || !mapper.map(InternalStateNamer::TYPE_LIT, typeStr)) + return false; - auto typeOpt = typeFromStr(typeStr); + auto typeOpt = InternalStateNamer::typeFromStr(typeStr); if (!typeOpt) - return nullptr; - TYPE type = *typeOpt; - llvm::json::Value inner = nullptr; - if (const auto *obj = value.getAsObject()) { - auto it = obj->find(INNER_LIT); - if (it != obj->end()) - inner = it->second; - } - std::unique_ptr prop = nullptr; + return false; + InternalStateNamer::TYPE type = *typeOpt; + namer = nullptr; + EagerForkSentNamer ef; + BufferSlotFullNamer bs; + PipelineSlotNamer ps; + MemoryControllerSlotNamer mc; + TokenCountNamer tc; + PipelineTokenCountNamer ptc; + EntrySlotNamer es; switch (type) { - case TYPE::EagerForkSent: - prop = EagerForkSentNamer::fromInnerJSON(inner, path); - assert(prop && "inner eager fork failed"); + case InternalStateNamer::TYPE::EagerForkSent: + ef = EagerForkSentNamer(); + if (!mapper.map(InternalStateNamer::INNER_LIT, ef)) + return false; + namer = std::make_unique(std::move(ef)); break; - case TYPE::BufferSlotFull: - prop = BufferSlotFullNamer::fromInnerJSON(inner, path); - assert(prop && "inner buffer slot failed"); + case InternalStateNamer::TYPE::BufferSlotFull: + bs = BufferSlotFullNamer(); + if (!mapper.map(InternalStateNamer::INNER_LIT, bs)) + return false; + namer = std::make_unique(std::move(bs)); break; - case TYPE::PipelineSlot: - prop = PipelineSlotNamer::fromInnerJSON(inner, path); - assert(prop && "inner latency slot failed"); + case InternalStateNamer::TYPE::PipelineSlot: + ps = PipelineSlotNamer(); + if (!mapper.map(InternalStateNamer::INNER_LIT, ps)) + return false; + namer = std::make_unique(std::move(ps)); break; - case TYPE::Constrained: + case InternalStateNamer::TYPE::Constrained: assert(false && "todo"); break; - case TYPE::TokenCount: - prop = TokenCountNamer::fromInnerJSON(inner, path); - assert(prop && "inner token count failed"); + case InternalStateNamer::TYPE::MemoryControllerSlot: + mc = MemoryControllerSlotNamer(); + if (!mapper.map(InternalStateNamer::INNER_LIT, mc)) + return false; + namer = std::make_unique(std::move(mc)); break; - case TYPE::PipelineTokenCount: - prop = PipelineTokenCountNamer::fromInnerJSON(inner, path); - assert(prop && "pipeline token count failed"); + case InternalStateNamer::TYPE::TokenCount: + tc = TokenCountNamer(); + if (!mapper.map(InternalStateNamer::INNER_LIT, tc)) + return false; + namer = std::make_unique(std::move(tc)); break; - case TYPE::MemoryControllerSlot: - prop = MemoryControllerSlotNamer::fromInnerJSON(inner, path); - assert(prop && "mc slot failed"); + case InternalStateNamer::TYPE::PipelineTokenCount: + ptc = PipelineTokenCountNamer(); + if (!mapper.map(InternalStateNamer::INNER_LIT, ptc)) + return false; + namer = std::make_unique(std::move(ptc)); break; - case TYPE::EntrySlot: - prop = EntrySlotNamer::fromInnerJSON(inner, path); - assert(prop && "entry slot failed"); + case InternalStateNamer::TYPE::EntrySlot: + es = EntrySlotNamer(); + if (!mapper.map(InternalStateNamer::INNER_LIT, es)) + return false; + namer = std::make_unique(std::move(es)); break; } - prop->type = type; - return prop; + namer->type = type; + return true; } std::unique_ptr @@ -117,16 +169,13 @@ InternalStateNamer::tryConstrain(int32_t value) { return nullptr; } -std::unique_ptr -EagerForkSentNamer::fromInnerJSON(const llvm::json::Value &value, - llvm::json::Path path) { +bool fromJSON(const llvm::json::Value &value, EagerForkSentNamer &namer, + llvm::json::Path path) { llvm::json::ObjectMapper mapper(value, path); - auto prop = std::make_unique(); - if (!mapper || !mapper.map(OPERATION_LIT, prop->opName) || - !mapper.map(CHANNEL_NAME_LIT, prop->channelName) || - !mapper.map(CHANNEL_SIZE_LIT, prop->channelSize)) - return nullptr; - return prop; + return mapper && + mapper.map(EagerForkSentNamer::OPERATION_LIT, namer.opName) && + mapper.map(EagerForkSentNamer::CHANNEL_NAME_LIT, namer.channelName) && + mapper.map(EagerForkSentNamer::CHANNEL_SIZE_LIT, namer.channelSize); } ConstrainedEagerForkSentNamer EagerForkSentNamer::constrain(int32_t value) { @@ -134,17 +183,14 @@ ConstrainedEagerForkSentNamer EagerForkSentNamer::constrain(int32_t value) { return p; } -std::unique_ptr -BufferSlotFullNamer::fromInnerJSON(const llvm::json::Value &value, - llvm::json::Path path) { +bool fromJSON(const llvm::json::Value &value, BufferSlotFullNamer &namer, + llvm::json::Path path) { llvm::json::ObjectMapper mapper(value, path); - auto prop = std::make_unique(); - if (!mapper || !mapper.map(OPERATION_LIT, prop->opName) || - !mapper.map(SLOT_NAME_LIT, prop->slotName) || - !mapper.map(DATA_NAME_LIT, prop->dataName) || - !mapper.map(SLOT_SIZE_LIT, prop->slotSize)) - return nullptr; - return prop; + return mapper && + mapper.map(BufferSlotFullNamer::OPERATION_LIT, namer.opName) && + mapper.map(BufferSlotFullNamer::SLOT_NAME_LIT, namer.slotName) && + mapper.map(BufferSlotFullNamer::DATA_NAME_LIT, namer.dataName) && + mapper.map(BufferSlotFullNamer::SLOT_SIZE_LIT, namer.slotSize); } ConstrainedBufferSlotFullNamer BufferSlotFullNamer::constrain(int32_t value) { @@ -152,79 +198,60 @@ ConstrainedBufferSlotFullNamer BufferSlotFullNamer::constrain(int32_t value) { return p; } -std::unique_ptr -PipelineSlotNamer::fromInnerJSON(const llvm::json::Value &value, - llvm::json::Path path) { +bool fromJSON(const llvm::json::Value &value, PipelineSlotNamer &namer, + llvm::json::Path path) { llvm::json::ObjectMapper mapper(value, path); - auto prop = std::make_unique(); int index; - if (!mapper || !mapper.map(OPERATION_LIT, prop->opName) || - !mapper.map(SLOT_INDEX_LIT, index)) - return nullptr; - prop->slotIndex = index; - return prop; + if (!mapper || !mapper.map(PipelineSlotNamer::OPERATION_LIT, namer.opName) || + !mapper.map(PipelineSlotNamer::SLOT_INDEX_LIT, index)) + return false; + namer.slotIndex = index; + return true; } -std::unique_ptr -PipelineTokenCountNamer::fromInnerJSON(const llvm::json::Value &value, - llvm::json::Path path) { +bool fromJSON(const llvm::json::Value &value, PipelineTokenCountNamer &namer, + llvm::json::Path path) { llvm::json::ObjectMapper mapper(value, path); - auto prop = std::make_unique(); - if (!mapper || !mapper.map(OPERATION_LIT, prop->opName)) - return nullptr; - return prop; + return mapper && + mapper.map(PipelineTokenCountNamer::OPERATION_LIT, namer.opName); } -std::unique_ptr -TokenCountNamer::fromInnerJSON(const llvm::json::Value &value, - llvm::json::Path path) { +bool fromJSON(const llvm::json::Value &value, TokenCountNamer &namer, + llvm::json::Path path) { llvm::json::ObjectMapper mapper(value, path); - auto prop = std::make_unique(); - if (!mapper || !mapper.map(OPERATION_LIT, prop->opName)) - return nullptr; - return prop; + return mapper && mapper.map(TokenCountNamer::OPERATION_LIT, namer.opName); } -std::unique_ptr -ConstrainedNamer::fromInnerJSON(const llvm::json::Value &value, - llvm::json::Path path) { - auto namer = InternalStateNamer::fromJSON(value, path); - assert(namer && "inner json must be an internal state"); +bool fromJSON(const llvm::json::Value &value, ConstrainedNamer &namer, + llvm::json::Path path) { auto mapper = llvm::json::ObjectMapper(value, path); + std::unique_ptr inner; int32_t val; - if (!mapper || !mapper.map(CONSTRAINT_VALUE, val)) - return nullptr; - - if (auto eagerFork = dyn_cast(namer)) { - return std::make_unique( - eagerFork->constrain(val)); - } - return nullptr; + if (!mapper || !mapper.map(ConstrainedNamer::CONSTRAINT_VALUE_LIT, val) || + !mapper.map(ConstrainedNamer::INNER_LIT, inner)) + return false; + namer = *inner->tryConstrain(val); + return true; } -std::unique_ptr -MemoryControllerSlotNamer::fromInnerJSON(const llvm::json::Value &value, - llvm::json::Path path) { +bool fromJSON(const llvm::json::Value &value, MemoryControllerSlotNamer &namer, + llvm::json::Path path) { llvm::json::ObjectMapper mapper(value, path); - auto prop = std::make_unique(); int t; - if (!mapper || !mapper.map(OPERATION_LIT, prop->opName) || - !mapper.map(SLOT_INDEX_LIT, prop->slotIndex) || - !mapper.map(PORT_TYPE_LIT, t) || - !mapper.map(LOADLESS_LIT, prop->loadless)) - return nullptr; - prop->portType = (PortType)t; - return prop; + if (!mapper || + !mapper.map(MemoryControllerSlotNamer::OPERATION_LIT, namer.opName) || + !mapper.map(MemoryControllerSlotNamer::SLOT_INDEX_LIT, namer.slotIndex) || + !mapper.map(MemoryControllerSlotNamer::PORT_TYPE_LIT, t) || + !mapper.map(MemoryControllerSlotNamer::LOADLESS_LIT, namer.loadless)) + return false; + namer.portType = (MemoryControllerSlotNamer::PortType)t; + return true; } -std::unique_ptr -EntrySlotNamer::fromInnerJSON(const llvm::json::Value &value, - llvm::json::Path path) { +bool fromJSON(const llvm::json::Value &value, EntrySlotNamer &namer, + llvm::json::Path path) { llvm::json::ObjectMapper mapper(value, path); - auto prop = std::make_unique(); - if (!mapper || !mapper.map(ARG_NAME_LIT, prop->argName)) - return nullptr; - return prop; + return mapper && mapper.map(EntrySlotNamer::ARG_NAME_LIT, namer.argName); } std::vector> @@ -239,7 +266,7 @@ getAllSlotsOfOperation(Operation *op) { if (auto endOp = dyn_cast(op)) { ret.push_back( - std::make_unique("testbench", "end", "", 0)); + std::make_unique("testbench", "end_full", "", 0)); } if (auto loadOp = dyn_cast(op)) { // TODO: Handle LoadOp for MC slot From c23946732a4b408796970c0073cc8a9027968912 Mon Sep 17 00:00:00 2001 From: Bas Niekel Date: Sat, 9 May 2026 14:34:47 +0200 Subject: [PATCH 26/29] more logical TokenCountNamer which does not need special smv definitions --- .../include/experimental/Support/FormalProperty.h | 9 ++++----- .../HandshakeAnnotateProperties.cpp | 4 +--- experimental/lib/Support/FormalProperty.cpp | 10 ++++------ .../generators/handshake/buffers/one_slot_break_dv.py | 2 -- .../generators/handshake/buffers/one_slot_break_r.py | 3 --- .../smv/generators/handshake/dead_buffer.py | 2 -- .../unit-generators/smv/generators/handshake/load.py | 2 -- .../smv/generators/support/delay_buffer.py | 1 - tools/export-rtl/export-rtl.cpp | 4 +--- 9 files changed, 10 insertions(+), 27 deletions(-) diff --git a/experimental/include/experimental/Support/FormalProperty.h b/experimental/include/experimental/Support/FormalProperty.h index f29b317500..bba123b5b3 100644 --- a/experimental/include/experimental/Support/FormalProperty.h +++ b/experimental/include/experimental/Support/FormalProperty.h @@ -318,9 +318,8 @@ class IOGConsecutiveTokens : public FormalProperty { fromJSON(const llvm::json::Value &value, llvm::json::Path path); IOGConsecutiveTokens() = default; - IOGConsecutiveTokens(unsigned long id, TAG tag, - std::shared_ptr slot1, - std::shared_ptr slot2, + IOGConsecutiveTokens(unsigned long id, TAG tag, const TokenCountNamer &slot1, + const TokenCountNamer &slot2, std::vector sents); ~IOGConsecutiveTokens() = default; @@ -328,8 +327,8 @@ class IOGConsecutiveTokens : public FormalProperty { return fp->getType() == TYPE::IOGConsecutiveTokens; } - std::shared_ptr slot1; - std::shared_ptr slot2; + TokenCountNamer slot1; + TokenCountNamer slot2; std::vector sents; private: diff --git a/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp b/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp index b78e9663c0..997392ca5e 100644 --- a/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp +++ b/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp @@ -371,12 +371,10 @@ HandshakeAnnotatePropertiesPass::annotateIOGSingleToken(const IOG &iog) { LogicalResult HandshakeAnnotatePropertiesPass::annotateIOGConsecutiveTokens(const IOG &iog) { - std::vector>> - slotOps; + std::vector> slotOps; for (auto &op : iog.units) { auto slotCountNamer = getTokenCountNamerOfOperation(op); if (slotCountNamer.has_value()) { - assert(*slotCountNamer); slotOps.push_back({op, std::move(*slotCountNamer)}); } } diff --git a/experimental/lib/Support/FormalProperty.cpp b/experimental/lib/Support/FormalProperty.cpp index f48f847bbe..26894a74f8 100644 --- a/experimental/lib/Support/FormalProperty.cpp +++ b/experimental/lib/Support/FormalProperty.cpp @@ -415,12 +415,10 @@ IOGConsecutiveTokens::fromJSON(const llvm::json::Value &value, } IOGConsecutiveTokens::IOGConsecutiveTokens( - unsigned long id, TAG tag, std::shared_ptr slot1, - std::shared_ptr slot2, - std::vector sents) - : FormalProperty(id, tag, TYPE::IOGConsecutiveTokens), - slot1(std::move(slot1)), slot2(std::move(slot2)), - sents(std::move(sents)) {} + unsigned long id, TAG tag, const TokenCountNamer &slot1, + const TokenCountNamer &slot2, std::vector sents) + : FormalProperty(id, tag, TYPE::IOGConsecutiveTokens), slot1(slot1), + slot2(slot2), sents(std::move(sents)) {} LogicalResult FormalPropertyTable::addPropertiesFromJSON(StringRef filepath) { // Open the properties' database diff --git a/experimental/tools/unit-generators/smv/generators/handshake/buffers/one_slot_break_dv.py b/experimental/tools/unit-generators/smv/generators/handshake/buffers/one_slot_break_dv.py index 133328d3e8..50bdaac337 100644 --- a/experimental/tools/unit-generators/smv/generators/handshake/buffers/one_slot_break_dv.py +++ b/experimental/tools/unit-generators/smv/generators/handshake/buffers/one_slot_break_dv.py @@ -24,7 +24,6 @@ def _generate_one_slot_break_dv_dataless(name): DEFINE ins_ready := !outs_valid_i | outs_ready; outs_valid := outs_valid_i; - slotted_token_count := count(outs_valid_i); """ @@ -48,7 +47,6 @@ def _generate_one_slot_break_dv(name, data_type): outs_valid := inner_one_slot_break_dv.outs_valid; outs_valid_i := inner_one_slot_break_dv.outs_valid_i; outs := data; - slotted_token_count := inner_one_slot_break_dv.slotted_token_count; {_generate_one_slot_break_dv_dataless(f"{name}__one_slot_break_dv_dataless")} """ diff --git a/experimental/tools/unit-generators/smv/generators/handshake/buffers/one_slot_break_r.py b/experimental/tools/unit-generators/smv/generators/handshake/buffers/one_slot_break_r.py index f3e4de34a7..2390188055 100644 --- a/experimental/tools/unit-generators/smv/generators/handshake/buffers/one_slot_break_r.py +++ b/experimental/tools/unit-generators/smv/generators/handshake/buffers/one_slot_break_r.py @@ -24,8 +24,6 @@ def _generate_one_slot_break_r_dataless(name): DEFINE ins_ready := !full; outs_valid := ins_valid | full; - - slotted_token_count := count(full); """ @@ -46,7 +44,6 @@ def _generate_one_slot_break_r(name, data_type): outs_valid := inner_one_slot_break_r.outs_valid; outs := inner_one_slot_break_r.full ? data : ins; - slotted_token_count := inner_one_slot_break_r.slotted_token_count; full := inner_one_slot_break_r.full; {_generate_one_slot_break_r_dataless(f"{name}__one_slot_break_r_dataless")} diff --git a/experimental/tools/unit-generators/smv/generators/handshake/dead_buffer.py b/experimental/tools/unit-generators/smv/generators/handshake/dead_buffer.py index 650eab3293..dc1fee0592 100644 --- a/experimental/tools/unit-generators/smv/generators/handshake/dead_buffer.py +++ b/experimental/tools/unit-generators/smv/generators/handshake/dead_buffer.py @@ -23,7 +23,6 @@ def _generate_dead_buffer_dataless(name): -- output DEFINE ins_ready := !full; - slotted_token_count := count(full); """ @@ -40,5 +39,4 @@ def _generate_dead_buffer(name, data_type): -- output DEFINE ins_ready := !full; - slotted_token_count := count(full); """ diff --git a/experimental/tools/unit-generators/smv/generators/handshake/load.py b/experimental/tools/unit-generators/smv/generators/handshake/load.py index d10e72ba35..ea736d9128 100644 --- a/experimental/tools/unit-generators/smv/generators/handshake/load.py +++ b/experimental/tools/unit-generators/smv/generators/handshake/load.py @@ -28,8 +28,6 @@ def _generate_load(name, data_type, addr_type): addr_full := inner_addr_one_slot_break_r.full; data_full := inner_data_one_slot_break_r.full; - slotted_token_count := count(addr_full, data_full); - {generate_one_slot_break_r(f"{name}__addr_one_slot_break_r", {ATTR_BITWIDTH: addr_type.bitwidth})} {generate_one_slot_break_r(f"{name}__data_one_slot_break_r", {ATTR_BITWIDTH: data_type.bitwidth})} """ diff --git a/experimental/tools/unit-generators/smv/generators/support/delay_buffer.py b/experimental/tools/unit-generators/smv/generators/support/delay_buffer.py index 7780377940..19a896278c 100644 --- a/experimental/tools/unit-generators/smv/generators/support/delay_buffer.py +++ b/experimental/tools/unit-generators/smv/generators/support/delay_buffer.py @@ -55,7 +55,6 @@ def _generate_delay_buffer(name, latency): DEFINE outs_valid := inner_one_slot_break_dv.outs_valid; DEFINE v{no_one_slot_break_dv_latency} := inner_one_slot_break_dv.outs_valid_i; - DEFINE pipeline_token_count := count({", ".join([f"v{n}" for n in range(latency)])}); {generate_one_slot_break_dv(f"{name}__one_slot_break_dv_dataless", {ATTR_BITWIDTH: 0})} """ diff --git a/tools/export-rtl/export-rtl.cpp b/tools/export-rtl/export-rtl.cpp index 7c27c453c3..1d5620770e 100644 --- a/tools/export-rtl/export-rtl.cpp +++ b/tools/export-rtl/export-rtl.cpp @@ -1340,11 +1340,9 @@ LogicalResult SMVWriter::createProperties(WriteModData &data) const { } right = llvm::join(sentNames, " | "); } - assert(p->slot1); - assert(p->slot2); std::string propertyString = llvm::formatv("(({0} > 0) & ({1} > 0)) -> ({2})", - p->slot1->getSMVName(), p->slot2->getSMVName(), right); + p->slot1.getSMVName(), p->slot2.getSMVName(), right); data.properties[p->getId()] = {propertyString, propertyTag}; } else { llvm::errs() << "Formal property Type not known\n"; From b227f81236077d0def240027e0a8d90bf766214c Mon Sep 17 00:00:00 2001 From: Bas Niekel Date: Sat, 9 May 2026 15:51:03 +0200 Subject: [PATCH 27/29] formatting --- lib/Dialect/Handshake/HandshakeOpInternalStateNamer.cpp | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/lib/Dialect/Handshake/HandshakeOpInternalStateNamer.cpp b/lib/Dialect/Handshake/HandshakeOpInternalStateNamer.cpp index 1f9c8c0c9f..a9929f3aa3 100644 --- a/lib/Dialect/Handshake/HandshakeOpInternalStateNamer.cpp +++ b/lib/Dialect/Handshake/HandshakeOpInternalStateNamer.cpp @@ -289,8 +289,7 @@ getAllSlotsOfOperation(Operation *op) { return ret; } -std::optional -getTokenCountNamerOfOperation(Operation *op) { +std::optional getTokenCountNamerOfOperation(Operation *op) { auto tokens = getAllSlotsOfOperation(op); if (tokens.empty()) { return std::nullopt; From 4ee3a5dac3d2b69c33c690ef5dae8ee0db2b8d7c Mon Sep 17 00:00:00 2001 From: Bas Niekel Date: Mon, 11 May 2026 21:02:30 +0200 Subject: [PATCH 28/29] comments --- .../Support/CreateSmvFormalTestbench.h | 6 +++-- .../HandshakeAnnotateProperties.cpp | 22 ++++++++++++++----- .../lib/Support/CreateSmvFormalTestbench.cpp | 6 +++-- 3 files changed, 24 insertions(+), 10 deletions(-) diff --git a/experimental/include/experimental/Support/CreateSmvFormalTestbench.h b/experimental/include/experimental/Support/CreateSmvFormalTestbench.h index df35a8c7bf..95f51b7ba1 100644 --- a/experimental/include/experimental/Support/CreateSmvFormalTestbench.h +++ b/experimental/include/experimental/Support/CreateSmvFormalTestbench.h @@ -49,8 +49,10 @@ struct SmvTestbenchConfig { // consumed by sinks bool syncOutput = false; - // Determines if the output is modelled as a dead buffer (i.e. accepts one - // token, then the output is no longer ready) + // Determines if the result of the join operation is modelled as a dead buffer + // (i.e. accepts one token, then the output is no longer ready) rather than + // always ready. + // Note: This only works if syncOutput is true bool deadBufferOutput = false; }; diff --git a/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp b/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp index 997392ca5e..1227956bad 100644 --- a/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp +++ b/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp @@ -293,9 +293,9 @@ HandshakeAnnotatePropertiesPass::annotateReconvergentPathFlow(ModuleOp modOp) { } namespace { -// This function finds appropriate fork sent states for the consecutive tokens -// invariant: Given the IOG and a set of paths from a start buffer to an end -// buffer, it determines all forks for which: +// This function finds appropriate fork sent state namers for the consecutive +// tokens invariant: Given the IOG and a set of paths from a start buffer to an +// end buffer, it determines all forks for which: // 1. The start buffer is the copied slot of the fork // 2. The fork is part of a path from start to end along the IOG std::vector findCopiedSents(const IOG &iog, @@ -307,10 +307,14 @@ std::vector findCopiedSents(const IOG &iog, while (!stack.empty()) { Operation *cur = stack.back(); stack.pop_back(); + // Skip the check for slots for the first operation, as the first operation + // contains the starting slot but should not terminate the search if (!first) { auto slots = getAllSlotsOfOperation(cur); if (!slots.empty()) { - return sents; + // Stop following this path if it contains a buffer, as following forks + // will not have the start buffer as copied slot + continue; } } first = false; @@ -318,7 +322,7 @@ std::vector findCopiedSents(const IOG &iog, if (!iog.contains(forward)) { continue; } - Operation *next = forward.getUses().begin()->getOwner(); + Operation *next = *forward.getUsers().begin(); assert(iog.contains(next)); if (pathSet.units.find(next) == pathSet.units.end()) { continue; @@ -344,8 +348,11 @@ HandshakeAnnotatePropertiesPass::annotateIOGSingleToken(const IOG &iog) { op->getAttrOfType("argNames")[iog.entry.getArgNumber()]; std::string name = dyn_cast(nameAttr).str(); + // We model the entry node as a buffer that initially has one token. slots.push_back(std::make_unique(name)); std::vector forks(0); + // Collecting the slots and sents inside the IOG. The invariant relation of + // num(slots) = 1 + num(eager fork sents) for (auto &op : iog.units) { for (auto &slot : getAllSlotsOfOperation(op)) { slots.push_back(std::move(slot)); @@ -380,9 +387,12 @@ HandshakeAnnotatePropertiesPass::annotateIOGConsecutiveTokens(const IOG &iog) { } for (auto slot1 = slotOps.begin(); slot1 != slotOps.end(); ++slot1) { for (auto slot2 = slot1 + 1; slot2 != slotOps.end(); ++slot2) { - if (slot1 == slot2) { + if (slot1->first == slot2->first) { // TODO: Handle loops, i.e. if the slot contains >=2 tokens, there // should be a copied fork within a loop + if (slot1->second.slots->size() >= 2) { + slot1->first->emitWarning("Should annotate self-loop"); + } continue; } diff --git a/experimental/lib/Support/CreateSmvFormalTestbench.cpp b/experimental/lib/Support/CreateSmvFormalTestbench.cpp index 67f4c855da..f3db2c9ec4 100644 --- a/experimental/lib/Support/CreateSmvFormalTestbench.cpp +++ b/experimental/lib/Support/CreateSmvFormalTestbench.cpp @@ -33,8 +33,10 @@ static std::string instantiateModuleUnderTest( const SmallVector> &arguments, const SmallVector> &results, bool syncOutput = false) { - SmallVector inputVariables; - inputVariables.push_back("self"); + // NOTE: self is a keyword in nuXmv that refers to the module it is written + // in. This way, the context of the testbench is passed to the inner module + // without cluttering the arguments. See nuXmv user manual 2.3.12 + SmallVector inputVariables = {"self"}; for (const auto &argument : arguments) { // The current handshake2smv conversion also creates a dataOut port when it // is of type control From 3fce970dcfe70c2a44e0b5a983fe0746eca1901f Mon Sep 17 00:00:00 2001 From: Bas Niekel Date: Tue, 12 May 2026 18:41:44 +0200 Subject: [PATCH 29/29] small fixes for clarity --- .../include/experimental/Support/IOG.h | 4 +++- .../HandshakeAnnotateProperties.cpp | 18 +++++++-------- experimental/lib/Support/IOG.cpp | 23 ++++++++++--------- .../HandshakeOpInternalStateNamer.cpp | 8 ++++--- 4 files changed, 29 insertions(+), 24 deletions(-) diff --git a/experimental/include/experimental/Support/IOG.h b/experimental/include/experimental/Support/IOG.h index 8faac81ee5..00811df789 100644 --- a/experimental/include/experimental/Support/IOG.h +++ b/experimental/include/experimental/Support/IOG.h @@ -13,7 +13,7 @@ struct IOGPathSet; // operations: For any unit `u` within the IOG, it says whether there exists a // path going through `u` or not. struct IOGPathSet { - IOGPathSet(const IOG &iog, Operation *start, Operation *end); + IOGPathSet(Operation *start, Operation *end) : start(start), end(end) {} std::unordered_set units; Operation *start; @@ -34,6 +34,8 @@ struct IOG { llvm::DenseSet channels; BlockArgument entry; + IOGPathSet findAllPaths(Operation *startOp, Operation *endOp) const; + inline bool contains(Operation *op) const { auto iter = units.find(op); return iter != units.end(); diff --git a/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp b/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp index 1227956bad..d3e87f9f3b 100644 --- a/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp +++ b/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp @@ -294,12 +294,13 @@ HandshakeAnnotatePropertiesPass::annotateReconvergentPathFlow(ModuleOp modOp) { namespace { // This function finds appropriate fork sent state namers for the consecutive -// tokens invariant: Given the IOG and a set of paths from a start buffer to an -// end buffer, it determines all forks for which: +// tokens invariant: Given the IOG, a starting slot, and an ending slot, it +// determines all forks for which: // 1. The start buffer is the copied slot of the fork // 2. The fork is part of a path from start to end along the IOG -std::vector findCopiedSents(const IOG &iog, - const IOGPathSet &pathSet) { +std::vector +findCopiedSents(const IOG &iog, Operation *startSlot, Operation *endSlot) { + auto pathSet = iog.findAllPaths(startSlot, endSlot); std::vector sents; std::vector stack; stack.push_back(pathSet.start); @@ -396,13 +397,12 @@ HandshakeAnnotatePropertiesPass::annotateIOGConsecutiveTokens(const IOG &iog) { continue; } - IOGPathSet pathSet12(iog, slot1->first, slot2->first); - std::vector copiedSents = - findCopiedSents(iog, pathSet12); + findCopiedSents(iog, slot1->first, slot2->first); + + std::vector extra = + findCopiedSents(iog, slot2->first, slot1->first); - IOGPathSet pathSet21(iog, slot2->first, slot1->first); - std::vector extra = findCopiedSents(iog, pathSet21); copiedSents.insert(copiedSents.end(), extra.begin(), extra.end()); // Note: diff --git a/experimental/lib/Support/IOG.cpp b/experimental/lib/Support/IOG.cpp index 8391f2423f..4aff0329c7 100644 --- a/experimental/lib/Support/IOG.cpp +++ b/experimental/lib/Support/IOG.cpp @@ -3,10 +3,10 @@ #include "mlir/IR/BuiltinOps.h" namespace dynamatic { -IOGPathSet::IOGPathSet(const IOG &iog, Operation *startA, Operation *endA) - : start(startA), end(endA) { +IOGPathSet IOG::findAllPaths(Operation *startOp, Operation *endOp) const { + IOGPathSet paths = IOGPathSet(startOp, endOp); std::vector stack; - stack.push_back(start); + stack.push_back(paths.start); std::unordered_set forward; // Find all operations reachable by going forward from the start without going // through the end operation @@ -20,21 +20,21 @@ IOGPathSet::IOGPathSet(const IOG &iog, Operation *startA, Operation *endA) forward.insert(op); - if (op == end) { + if (op == paths.end) { continue; } for (auto channel : op->getResults()) { - if (!iog.contains(channel)) { + if (!contains(channel)) { continue; } Operation *next = channel.getUses().begin()->getOwner(); - assert(iog.contains(next)); + assert(contains(next)); stack.push_back(next); } } - stack.push_back(end); + stack.push_back(paths.end); std::unordered_set back; // Find all operations reachable by going backwards from the end without going @@ -50,19 +50,19 @@ IOGPathSet::IOGPathSet(const IOG &iog, Operation *startA, Operation *endA) back.insert(op); - if (op == start) { + if (op == paths.start) { continue; } for (auto channel : op->getOperands()) { - if (!iog.contains(channel)) { + if (!contains(channel)) { continue; } Operation *next = channel.getDefiningOp(); if (next == nullptr) { continue; } - assert(iog.contains(next)); + assert(contains(next)); stack.push_back(next); } } @@ -71,9 +71,10 @@ IOGPathSet::IOGPathSet(const IOG &iog, Operation *startA, Operation *endA) // end, is part of a path from start to end for (Operation *op : forward) { if (back.find(op) != back.end()) { - units.insert(op); + paths.units.insert(op); } } + return paths; } namespace { diff --git a/lib/Dialect/Handshake/HandshakeOpInternalStateNamer.cpp b/lib/Dialect/Handshake/HandshakeOpInternalStateNamer.cpp index a9929f3aa3..25601b2d07 100644 --- a/lib/Dialect/Handshake/HandshakeOpInternalStateNamer.cpp +++ b/lib/Dialect/Handshake/HandshakeOpInternalStateNamer.cpp @@ -259,12 +259,14 @@ getAllSlotsOfOperation(Operation *op) { std::make_unique("testbench", "end_full", "", 0)); } if (auto loadOp = dyn_cast(op)) { - // TODO: Handle LoadOp for MC slot auto slots = loadOp.getInternalSlotStateNamers(); auto *mcOp = loadOp.getAddressResult().getUses().begin()->getOwner(); - assert(mcOp); auto mc = dyn_cast(mcOp); - assert(mc); + if (!mc) { + op->emitError("Cannot get slot of LoadOp that is not connected to Memory " + "Controller Op"); + llvm::report_fatal_error("Unhandled LoadOp"); + } size_t nLoads = mc.getNumLoadPorts(); std::optional mcSlot; for (size_t i = 0; i < nLoads; ++i) {