From 5661257a43767a7ff9cbe1975769a0f642da3573 Mon Sep 17 00:00:00 2001 From: Bas Niekel Date: Thu, 15 Jan 2026 14:36:47 +0100 Subject: [PATCH 01/10] invariant 3 boilerplate --- .../experimental/Support/FormalProperty.h | 27 +++++++++++++++++++ experimental/lib/Support/FormalProperty.cpp | 26 ++++++++++++++++++ 2 files changed, 53 insertions(+) diff --git a/experimental/include/experimental/Support/FormalProperty.h b/experimental/include/experimental/Support/FormalProperty.h index 11d5b181df..b28bf00984 100644 --- a/experimental/include/experimental/Support/FormalProperty.h +++ b/experimental/include/experimental/Support/FormalProperty.h @@ -228,6 +228,33 @@ class CopiedSlotsOfActiveForkAreFull : public FormalProperty { inline static const StringLiteral BUFFER_SLOT_LIT = "buffer_slot"; }; +class PathSingleSentForkOutput : public FormalProperty { +public: + std::vector getForkOps() { return forkOps; } + std::vector getOutputIdxs() { return outputIdxs; } + + llvm::json::Value extraInfoToJSON() const override; + + static std::unique_ptr + fromJSON(const llvm::json::Value &value, llvm::json::Path path); + + PathSingleSentForkOutput() = default; + PathSingleSentForkOutput(unsigned long id, TAG tag, + std::vector &forkOps, + std::vector &outputIdxs); + ~PathSingleSentForkOutput() = default; + + static bool classof(const FormalProperty *fp) { + return fp->getType() == TYPE::CSOAFAF; + } + +private: + std::vector forkOps; + std::vector outputIdxs; + inline static const StringLiteral FORK_OPS_LIT = "fork_ops"; + inline static const StringLiteral OUTPUT_IDXS_LIT = "output_idxs"; +}; + class FormalPropertyTable { public: FormalPropertyTable() = default; diff --git a/experimental/lib/Support/FormalProperty.cpp b/experimental/lib/Support/FormalProperty.cpp index 94cca64a9d..1584fb5dbb 100644 --- a/experimental/lib/Support/FormalProperty.cpp +++ b/experimental/lib/Support/FormalProperty.cpp @@ -304,6 +304,32 @@ CopiedSlotsOfActiveForkAreFull::fromJSON(const llvm::json::Value &value, return prop; } +PathSingleSentForkOutput::PathSingleSentForkOutput( + unsigned long id, TAG tag, std::vector &forkOps, + std::vector &outputIdxs) + : FormalProperty(id, tag, TYPE::CSOAFAF), forkOps{forkOps}, + outputIdxs{outputIdxs} {} + +llvm::json::Value PathSingleSentForkOutput::extraInfoToJSON() const { + return llvm::json::Object( + {{FORK_OPS_LIT, forkOps}, {OUTPUT_IDXS_LIT, outputIdxs}}); +} + +std::unique_ptr +PathSingleSentForkOutput::fromJSON(const llvm::json::Value &value, + llvm::json::Path path) { + auto prop = std::make_unique(); + + auto info = prop->parseBaseAndExtractInfo(value, path); + llvm::json::ObjectMapper mapper(info, path); + + if (!mapper || !mapper.map(FORK_OPS_LIT, prop->forkOps) || + !mapper.map(OUTPUT_IDXS_LIT, prop->outputIdxs)) + return nullptr; + + return prop; +} + LogicalResult FormalPropertyTable::addPropertiesFromJSON(StringRef filepath) { // Open the properties' database std::ifstream inputFile(filepath.str()); From e20fccec15024303437f9201c15ac9b91ecce68f Mon Sep 17 00:00:00 2001 From: Bas Niekel Date: Fri, 16 Jan 2026 15:44:33 +0100 Subject: [PATCH 02/10] invariant 3 annotation and generation --- .../experimental/Support/FormalProperty.h | 7 +- .../HandshakeAnnotateProperties.cpp | 109 ++++++++++++++++++ experimental/lib/Support/FormalProperty.cpp | 12 +- tools/export-rtl/export-rtl.cpp | 17 +++ 4 files changed, 139 insertions(+), 6 deletions(-) diff --git a/experimental/include/experimental/Support/FormalProperty.h b/experimental/include/experimental/Support/FormalProperty.h index b28bf00984..74cde2dc39 100644 --- a/experimental/include/experimental/Support/FormalProperty.h +++ b/experimental/include/experimental/Support/FormalProperty.h @@ -29,6 +29,7 @@ class FormalProperty { VEQ /* Valid EQuivalence */, EFNAO /* Eager Fork Not All Output sent */, CSOAFAF, /* Copied Slots Of Active Forks Are Full */ + PSSFO, /* Path Single Sent Fork Output */ }; TAG getTag() const { return tag; } @@ -240,12 +241,12 @@ class PathSingleSentForkOutput : public FormalProperty { PathSingleSentForkOutput() = default; PathSingleSentForkOutput(unsigned long id, TAG tag, - std::vector &forkOps, - std::vector &outputIdxs); + const std::vector &forkOps, + const std::vector &outputIdxs); ~PathSingleSentForkOutput() = default; static bool classof(const FormalProperty *fp) { - return fp->getType() == TYPE::CSOAFAF; + return fp->getType() == TYPE::PSSFO; } private: diff --git a/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp b/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp index 92e6b6b94e..18d98f67d0 100644 --- a/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp +++ b/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp @@ -73,6 +73,21 @@ struct HandshakeAnnotatePropertiesPass Operation &curOp); LogicalResult annotateCopiedSlots(Operation &op); LogicalResult annotateCopiedSlotsOfAllForks(ModuleOp modOp); + + LogicalResult + annotatePathSingleForkSentFinal(const std::vector &prevForks, + const std::vector &prevIdxs); + LogicalResult + annotatePathSingleForkSentRec(std::unordered_set visitedSet, + const std::vector &prevForks, + const std::vector &prevIdxs, + Operation &curOp); + LogicalResult annotatePathSingleForkSentGoNext( + const std::unordered_set &visitedSet, + const std::vector &prevForks, + const std::vector &prevIdxs, Operation &curOp, + bool annotateIdxs); + LogicalResult annotatePathSingleForkSent(ModuleOp modOp); bool isChannelToBeChecked(OpResult res); }; } // namespace @@ -223,6 +238,98 @@ HandshakeAnnotatePropertiesPass::annotateCopiedSlotsOfAllForks(ModuleOp modOp) { return success(); } +LogicalResult HandshakeAnnotatePropertiesPass::annotatePathSingleForkSentFinal( + const std::vector &prevForks, + const std::vector &prevIdxs) { + if (prevForks.size() != prevIdxs.size()) { + llvm::errs() << "Different Indexs size and forks size\n"; + return failure(); + } + // No need to annotate properties of length 1 or lower + if (prevForks.size() <= 1) { + return success(); + } + PathSingleSentForkOutput p(uid, FormalProperty::TAG::INVAR, prevForks, + prevIdxs); + propertyTable.push_back(p.toJSON()); + uid++; + return success(); +} + +LogicalResult HandshakeAnnotatePropertiesPass::annotatePathSingleForkSentRec( + std::unordered_set visitedSet, + const std::vector &prevForks, + const std::vector &prevIdxs, Operation &curOp) { + + // If this operation has been visited, there is nothing to do + std::string id = getUniqueName(&curOp).str(); + if (auto iter = visitedSet.find(id); iter != visitedSet.end()) { + return success(); + } + visitedSet.insert(id); + + // Found a slot, which marks the end of this path + if (auto bufOp = dyn_cast(curOp)) { + return success(); + } + + if (auto forkOp = dyn_cast(curOp)) { + auto nextForks = prevForks; + nextForks.push_back(id); + return annotatePathSingleForkSentGoNext(visitedSet, nextForks, prevIdxs, + curOp, true); + } + return annotatePathSingleForkSentGoNext(visitedSet, prevForks, prevIdxs, + curOp, false); +} + +LogicalResult HandshakeAnnotatePropertiesPass::annotatePathSingleForkSentGoNext( + const std::unordered_set &visitedSet, + const std::vector &prevForks, + const std::vector &prevIdxs, Operation &curOp, + bool annotateIdxs) { + llvm::errs() << "visited: " << visitedSet.size() << "\n"; + llvm::errs() << "forks: " << prevForks.size() << " idxs: " << prevIdxs.size() + << " annotateIdxs: " << annotateIdxs << "\n"; + for (auto [i, res] : llvm::enumerate(curOp.getResults())) { + std::vector nextIdxs = prevIdxs; + if (annotateIdxs) { + nextIdxs.push_back(i); + if (failed(annotatePathSingleForkSentFinal(prevForks, nextIdxs))) { + return failure(); + } + } + for (auto *op : res.getUsers()) { + llvm::errs() << "from " << getUniqueName(&curOp) << " to " + << getUniqueName(op) << "\n"; + if (failed(annotatePathSingleForkSentRec(visitedSet, prevForks, nextIdxs, + *op))) { + return failure(); + } + } + } + return success(); +} + +LogicalResult +HandshakeAnnotatePropertiesPass::annotatePathSingleForkSent(ModuleOp modOp) { + for (handshake::FuncOp funcOp : modOp.getOps()) { + for (Operation &op : funcOp.getOps()) { + if (auto forkOp = dyn_cast(op)) { + std::vector names{}; + std::vector outputs{}; + std::unordered_set visited{}; + names.push_back(getUniqueName(&op).str()); + if (failed(annotatePathSingleForkSentGoNext(visited, names, outputs, op, + true))) { + return failure(); + } + } + } + } + return success(); +} + void HandshakeAnnotatePropertiesPass::runDynamaticPass() { ModuleOp modOp = getOperation(); @@ -235,6 +342,8 @@ void HandshakeAnnotatePropertiesPass::runDynamaticPass() { return signalPassFailure(); if (failed(annotateCopiedSlotsOfAllForks(modOp))) return signalPassFailure(); + if (failed(annotatePathSingleForkSent(modOp))) + return signalPassFailure(); } llvm::json::Value jsonVal(std::move(propertyTable)); diff --git a/experimental/lib/Support/FormalProperty.cpp b/experimental/lib/Support/FormalProperty.cpp index 1584fb5dbb..7a23b2c450 100644 --- a/experimental/lib/Support/FormalProperty.cpp +++ b/experimental/lib/Support/FormalProperty.cpp @@ -31,6 +31,8 @@ FormalProperty::typeFromStr(const std::string &s) { return FormalProperty::TYPE::EFNAO; if (s == "CSOAFAF") return FormalProperty::TYPE::CSOAFAF; + if (s == "PSSFO") + return FormalProperty::TYPE::PSSFO; return std::nullopt; } @@ -45,6 +47,8 @@ std::string FormalProperty::typeToStr(TYPE t) { return "EFNAO"; case TYPE::CSOAFAF: return "CSOAFAF"; + case TYPE::PSSFO: + return "PSSFO"; } } @@ -102,6 +106,8 @@ FormalProperty::fromJSON(const llvm::json::Value &value, case TYPE::CSOAFAF: return CopiedSlotsOfActiveForkAreFull::fromJSON(value, path.field(INFO_LIT)); + case TYPE::PSSFO: + return PathSingleSentForkOutput::fromJSON(value, path.field(INFO_LIT)); } } @@ -305,9 +311,9 @@ CopiedSlotsOfActiveForkAreFull::fromJSON(const llvm::json::Value &value, } PathSingleSentForkOutput::PathSingleSentForkOutput( - unsigned long id, TAG tag, std::vector &forkOps, - std::vector &outputIdxs) - : FormalProperty(id, tag, TYPE::CSOAFAF), forkOps{forkOps}, + unsigned long id, TAG tag, const std::vector &forkOps, + const std::vector &outputIdxs) + : FormalProperty(id, tag, TYPE::PSSFO), forkOps{forkOps}, outputIdxs{outputIdxs} {} llvm::json::Value PathSingleSentForkOutput::extraInfoToJSON() const { diff --git a/tools/export-rtl/export-rtl.cpp b/tools/export-rtl/export-rtl.cpp index f047f8f5c8..b9257adf39 100644 --- a/tools/export-rtl/export-rtl.cpp +++ b/tools/export-rtl/export-rtl.cpp @@ -1286,6 +1286,23 @@ LogicalResult SMVWriter::createProperties(WriteModData &data) const { bufferFull) .str(); data.properties[p->getId()] = {propertyString, propertyTag}; + } else if (auto *p = + llvm::dyn_cast(property.get())) { + // e.g. count(fork0.sent_0, fork1.sent_1, fork2.sent_0) <= 2 + auto names = p->getForkOps(); + auto idxs = p->getOutputIdxs(); + if (names.size() != idxs.size()) { + llvm::errs() << "Expected equal number of forks and fork outputs in " + "PathSingleSentForkOutput invariant\n"; + return failure(); + } + std::vector forkOutNames{names.size()}; + for (size_t i = 0; i < names.size(); ++i) { + forkOutNames[i] = llvm::formatv("{0}.sent_{1}", names[i], idxs[i]); + } + std::string propertyString = + llvm::formatv("count({0}) <= 1", llvm::join(forkOutNames, ", ")); + data.properties[p->getId()] = {propertyString, propertyTag}; } else { llvm::errs() << "Formal property Type not known\n"; return failure(); From 5d8a65de830fc97ebc904d91f5f7f7cad3d12256 Mon Sep 17 00:00:00 2001 From: Bas Niekel Date: Mon, 19 Jan 2026 12:24:27 +0100 Subject: [PATCH 03/10] comment explaining the invariant --- experimental/include/experimental/Support/FormalProperty.h | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/experimental/include/experimental/Support/FormalProperty.h b/experimental/include/experimental/Support/FormalProperty.h index 74cde2dc39..cba5c36cf0 100644 --- a/experimental/include/experimental/Support/FormalProperty.h +++ b/experimental/include/experimental/Support/FormalProperty.h @@ -229,6 +229,13 @@ class CopiedSlotsOfActiveForkAreFull : public FormalProperty { inline static const StringLiteral BUFFER_SLOT_LIT = "buffer_slot"; }; +// For any path that does not contain any slots, only at most a single fork +// output along that path can be in the `sent` state. In other words, if there +// is a path containing two fork outputs in the `sent` state, there has to be a +// slot containing a token between them, as the earlier `sent` output duplicated +// a token onto this path, and the later `sent` output blocks the token from +// leaving the path. See invariant 3 of +// https://ieeexplore.ieee.org/document/10323796 for more details class PathSingleSentForkOutput : public FormalProperty { public: std::vector getForkOps() { return forkOps; } From 8d0c16ae818b62c8aa8ac7a5a6ed3406d829741c Mon Sep 17 00:00:00 2001 From: Bas Niekel Date: Wed, 21 Jan 2026 12:48:54 +0100 Subject: [PATCH 04/10] removed debug prints --- .../FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp | 5 ----- 1 file changed, 5 deletions(-) diff --git a/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp b/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp index 18d98f67d0..ea3ea9ca41 100644 --- a/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp +++ b/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp @@ -288,9 +288,6 @@ LogicalResult HandshakeAnnotatePropertiesPass::annotatePathSingleForkSentGoNext( const std::vector &prevForks, const std::vector &prevIdxs, Operation &curOp, bool annotateIdxs) { - llvm::errs() << "visited: " << visitedSet.size() << "\n"; - llvm::errs() << "forks: " << prevForks.size() << " idxs: " << prevIdxs.size() - << " annotateIdxs: " << annotateIdxs << "\n"; for (auto [i, res] : llvm::enumerate(curOp.getResults())) { std::vector nextIdxs = prevIdxs; if (annotateIdxs) { @@ -300,8 +297,6 @@ LogicalResult HandshakeAnnotatePropertiesPass::annotatePathSingleForkSentGoNext( } } for (auto *op : res.getUsers()) { - llvm::errs() << "from " << getUniqueName(&curOp) << " to " - << getUniqueName(op) << "\n"; if (failed(annotatePathSingleForkSentRec(visitedSet, prevForks, nextIdxs, *op))) { return failure(); From 7e4442166875a30d05cd0249f1ea8f53e89821bf Mon Sep 17 00:00:00 2001 From: Bas Niekel Date: Wed, 21 Jan 2026 13:02:55 +0100 Subject: [PATCH 05/10] added consistent naming of load operator slots in the smv unit generator added example for what invariant2 looks like in smv --- .../tools/unit-generators/smv/generators/handshake/load.py | 2 ++ tools/export-rtl/export-rtl.cpp | 2 ++ 2 files changed, 4 insertions(+) diff --git a/experimental/tools/unit-generators/smv/generators/handshake/load.py b/experimental/tools/unit-generators/smv/generators/handshake/load.py index 3314328ce1..c486de307f 100644 --- a/experimental/tools/unit-generators/smv/generators/handshake/load.py +++ b/experimental/tools/unit-generators/smv/generators/handshake/load.py @@ -24,6 +24,8 @@ def _generate_load(name, data_type, addr_type): dataFromMem_ready := inner_data_one_slot_break_r.ins_ready; dataOut := inner_data_one_slot_break_r.outs; dataOut_valid := inner_data_one_slot_break_r.outs_valid; + full_0 := inner_addr_one_slot_break_r.full_0; + full_1 := inner_data_one_slot_break_r.full_0; {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/tools/export-rtl/export-rtl.cpp b/tools/export-rtl/export-rtl.cpp index b9257adf39..6ecc7c0f56 100644 --- a/tools/export-rtl/export-rtl.cpp +++ b/tools/export-rtl/export-rtl.cpp @@ -1285,6 +1285,8 @@ LogicalResult SMVWriter::createProperties(WriteModData &data) const { llvm::formatv("({0}) -> {1}", llvm::join(forkOutNames, " | "), bufferFull) .str(); + // e.g. (fork6.sent_0 | fork6.sent_1) -> load1.full_1 + // when the second slot of load1 is a copied slot of fork6 data.properties[p->getId()] = {propertyString, propertyTag}; } else if (auto *p = llvm::dyn_cast(property.get())) { From d59e069381d70f3e6186d9759bad4dcd860eb6b0 Mon Sep 17 00:00:00 2001 From: Bas Niekel Date: Wed, 21 Jan 2026 13:37:49 +0100 Subject: [PATCH 06/10] better naming of functions --- .../HandshakeAnnotateProperties.cpp | 22 +++++++++---------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp b/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp index ea3ea9ca41..c116cbe98b 100644 --- a/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp +++ b/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp @@ -75,14 +75,14 @@ struct HandshakeAnnotatePropertiesPass LogicalResult annotateCopiedSlotsOfAllForks(ModuleOp modOp); LogicalResult - annotatePathSingleForkSentFinal(const std::vector &prevForks, + annotatePathSingleForkSentPushProperty(const std::vector &prevForks, const std::vector &prevIdxs); LogicalResult - annotatePathSingleForkSentRec(std::unordered_set visitedSet, + annotatePathSingleForkSentDecide(std::unordered_set visitedSet, const std::vector &prevForks, const std::vector &prevIdxs, Operation &curOp); - LogicalResult annotatePathSingleForkSentGoNext( + LogicalResult annotatePathSingleForkSentIterate( const std::unordered_set &visitedSet, const std::vector &prevForks, const std::vector &prevIdxs, Operation &curOp, @@ -238,7 +238,7 @@ HandshakeAnnotatePropertiesPass::annotateCopiedSlotsOfAllForks(ModuleOp modOp) { return success(); } -LogicalResult HandshakeAnnotatePropertiesPass::annotatePathSingleForkSentFinal( +LogicalResult HandshakeAnnotatePropertiesPass::annotatePathSingleForkSentPushProperty( const std::vector &prevForks, const std::vector &prevIdxs) { if (prevForks.size() != prevIdxs.size()) { @@ -256,7 +256,7 @@ LogicalResult HandshakeAnnotatePropertiesPass::annotatePathSingleForkSentFinal( return success(); } -LogicalResult HandshakeAnnotatePropertiesPass::annotatePathSingleForkSentRec( +LogicalResult HandshakeAnnotatePropertiesPass::annotatePathSingleForkSentDecide( std::unordered_set visitedSet, const std::vector &prevForks, const std::vector &prevIdxs, Operation &curOp) { @@ -276,14 +276,14 @@ LogicalResult HandshakeAnnotatePropertiesPass::annotatePathSingleForkSentRec( if (auto forkOp = dyn_cast(curOp)) { auto nextForks = prevForks; nextForks.push_back(id); - return annotatePathSingleForkSentGoNext(visitedSet, nextForks, prevIdxs, + return annotatePathSingleForkSentIterate(visitedSet, nextForks, prevIdxs, curOp, true); } - return annotatePathSingleForkSentGoNext(visitedSet, prevForks, prevIdxs, + return annotatePathSingleForkSentIterate(visitedSet, prevForks, prevIdxs, curOp, false); } -LogicalResult HandshakeAnnotatePropertiesPass::annotatePathSingleForkSentGoNext( +LogicalResult HandshakeAnnotatePropertiesPass::annotatePathSingleForkSentIterate( const std::unordered_set &visitedSet, const std::vector &prevForks, const std::vector &prevIdxs, Operation &curOp, @@ -292,12 +292,12 @@ LogicalResult HandshakeAnnotatePropertiesPass::annotatePathSingleForkSentGoNext( std::vector nextIdxs = prevIdxs; if (annotateIdxs) { nextIdxs.push_back(i); - if (failed(annotatePathSingleForkSentFinal(prevForks, nextIdxs))) { + if (failed(annotatePathSingleForkSentPushProperty(prevForks, nextIdxs))) { return failure(); } } for (auto *op : res.getUsers()) { - if (failed(annotatePathSingleForkSentRec(visitedSet, prevForks, nextIdxs, + if (failed(annotatePathSingleForkSentDecide(visitedSet, prevForks, nextIdxs, *op))) { return failure(); } @@ -315,7 +315,7 @@ HandshakeAnnotatePropertiesPass::annotatePathSingleForkSent(ModuleOp modOp) { std::vector outputs{}; std::unordered_set visited{}; names.push_back(getUniqueName(&op).str()); - if (failed(annotatePathSingleForkSentGoNext(visited, names, outputs, op, + if (failed(annotatePathSingleForkSentIterate(visited, names, outputs, op, true))) { return failure(); } From bc8b531f8c14575df4d6546a4410f1516e278853 Mon Sep 17 00:00:00 2001 From: Bas Niekel Date: Wed, 21 Jan 2026 17:05:06 +0100 Subject: [PATCH 07/10] formatting --- .../HandshakeAnnotateProperties.cpp | 30 ++++++++++--------- 1 file changed, 16 insertions(+), 14 deletions(-) diff --git a/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp b/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp index c116cbe98b..a3df927ea5 100644 --- a/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp +++ b/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp @@ -74,14 +74,14 @@ struct HandshakeAnnotatePropertiesPass LogicalResult annotateCopiedSlots(Operation &op); LogicalResult annotateCopiedSlotsOfAllForks(ModuleOp modOp); - LogicalResult - annotatePathSingleForkSentPushProperty(const std::vector &prevForks, - const std::vector &prevIdxs); + LogicalResult annotatePathSingleForkSentPushProperty( + const std::vector &prevForks, + const std::vector &prevIdxs); LogicalResult annotatePathSingleForkSentDecide(std::unordered_set visitedSet, - const std::vector &prevForks, - const std::vector &prevIdxs, - Operation &curOp); + const std::vector &prevForks, + const std::vector &prevIdxs, + Operation &curOp); LogicalResult annotatePathSingleForkSentIterate( const std::unordered_set &visitedSet, const std::vector &prevForks, @@ -238,7 +238,8 @@ HandshakeAnnotatePropertiesPass::annotateCopiedSlotsOfAllForks(ModuleOp modOp) { return success(); } -LogicalResult HandshakeAnnotatePropertiesPass::annotatePathSingleForkSentPushProperty( +LogicalResult +HandshakeAnnotatePropertiesPass::annotatePathSingleForkSentPushProperty( const std::vector &prevForks, const std::vector &prevIdxs) { if (prevForks.size() != prevIdxs.size()) { @@ -277,13 +278,14 @@ LogicalResult HandshakeAnnotatePropertiesPass::annotatePathSingleForkSentDecide( auto nextForks = prevForks; nextForks.push_back(id); return annotatePathSingleForkSentIterate(visitedSet, nextForks, prevIdxs, - curOp, true); + curOp, true); } return annotatePathSingleForkSentIterate(visitedSet, prevForks, prevIdxs, - curOp, false); + curOp, false); } -LogicalResult HandshakeAnnotatePropertiesPass::annotatePathSingleForkSentIterate( +LogicalResult +HandshakeAnnotatePropertiesPass::annotatePathSingleForkSentIterate( const std::unordered_set &visitedSet, const std::vector &prevForks, const std::vector &prevIdxs, Operation &curOp, @@ -297,8 +299,8 @@ LogicalResult HandshakeAnnotatePropertiesPass::annotatePathSingleForkSentIterate } } for (auto *op : res.getUsers()) { - if (failed(annotatePathSingleForkSentDecide(visitedSet, prevForks, nextIdxs, - *op))) { + if (failed(annotatePathSingleForkSentDecide(visitedSet, prevForks, + nextIdxs, *op))) { return failure(); } } @@ -315,8 +317,8 @@ HandshakeAnnotatePropertiesPass::annotatePathSingleForkSent(ModuleOp modOp) { std::vector outputs{}; std::unordered_set visited{}; names.push_back(getUniqueName(&op).str()); - if (failed(annotatePathSingleForkSentIterate(visited, names, outputs, op, - true))) { + if (failed(annotatePathSingleForkSentIterate(visited, names, outputs, + op, true))) { return failure(); } } From 1944debbfa16553b12955c895f3002476f08051e Mon Sep 17 00:00:00 2001 From: Bas Niekel Date: Thu, 5 Feb 2026 15:39:06 +0100 Subject: [PATCH 08/10] expand acronyms --- .../experimental/Support/FormalProperty.h | 12 +++++----- experimental/lib/Support/FormalProperty.cpp | 24 +++++++++---------- 2 files changed, 18 insertions(+), 18 deletions(-) diff --git a/experimental/include/experimental/Support/FormalProperty.h b/experimental/include/experimental/Support/FormalProperty.h index cba5c36cf0..7e1b07b1e3 100644 --- a/experimental/include/experimental/Support/FormalProperty.h +++ b/experimental/include/experimental/Support/FormalProperty.h @@ -27,9 +27,9 @@ class FormalProperty { enum class TYPE { AOB /* Absence Of Backpressure */, VEQ /* Valid EQuivalence */, - EFNAO /* Eager Fork Not All Output sent */, - CSOAFAF, /* Copied Slots Of Active Forks Are Full */ - PSSFO, /* Path Single Sent Fork Output */ + EagerForkNotAllOutputSent, /* Eager Fork Not All Output sent */ + CopiedSlotsOfActiveForksAreFull, /* Copied Slots Of Active Forks Are Full */ + PathSingleSentForkOutput, /* Path Single Sent Fork Output */ }; TAG getTag() const { return tag; } @@ -179,7 +179,7 @@ class EagerForkNotAllOutputSent : public FormalProperty { ~EagerForkNotAllOutputSent() = default; static bool classof(const FormalProperty *fp) { - return fp->getType() == TYPE::EFNAO; + return fp->getType() == TYPE::EagerForkNotAllOutputSent; } private: @@ -215,7 +215,7 @@ class CopiedSlotsOfActiveForkAreFull : public FormalProperty { ~CopiedSlotsOfActiveForkAreFull() = default; static bool classof(const FormalProperty *fp) { - return fp->getType() == TYPE::CSOAFAF; + return fp->getType() == TYPE::CopiedSlotsOfActiveForksAreFull; } private: @@ -253,7 +253,7 @@ class PathSingleSentForkOutput : public FormalProperty { ~PathSingleSentForkOutput() = default; static bool classof(const FormalProperty *fp) { - return fp->getType() == TYPE::PSSFO; + return fp->getType() == TYPE::PathSingleSentForkOutput; } private: diff --git a/experimental/lib/Support/FormalProperty.cpp b/experimental/lib/Support/FormalProperty.cpp index 7a23b2c450..93e4906051 100644 --- a/experimental/lib/Support/FormalProperty.cpp +++ b/experimental/lib/Support/FormalProperty.cpp @@ -28,11 +28,11 @@ FormalProperty::typeFromStr(const std::string &s) { if (s == "VEQ") return FormalProperty::TYPE::VEQ; if (s == "EFNAO") - return FormalProperty::TYPE::EFNAO; + return FormalProperty::TYPE::EagerForkNotAllOutputSent; if (s == "CSOAFAF") - return FormalProperty::TYPE::CSOAFAF; + return FormalProperty::TYPE::CopiedSlotsOfActiveForksAreFull; if (s == "PSSFO") - return FormalProperty::TYPE::PSSFO; + return FormalProperty::TYPE::PathSingleSentForkOutput; return std::nullopt; } @@ -43,11 +43,11 @@ std::string FormalProperty::typeToStr(TYPE t) { return "AOB"; case TYPE::VEQ: return "VEQ"; - case TYPE::EFNAO: + case TYPE::EagerForkNotAllOutputSent: return "EFNAO"; - case TYPE::CSOAFAF: + case TYPE::CopiedSlotsOfActiveForksAreFull: return "CSOAFAF"; - case TYPE::PSSFO: + case TYPE::PathSingleSentForkOutput: return "PSSFO"; } } @@ -101,12 +101,12 @@ FormalProperty::fromJSON(const llvm::json::Value &value, return AbsenceOfBackpressure::fromJSON(value, path.field(INFO_LIT)); case TYPE::VEQ: return ValidEquivalence::fromJSON(value, path.field(INFO_LIT)); - case TYPE::EFNAO: + case TYPE::EagerForkNotAllOutputSent: return EagerForkNotAllOutputSent::fromJSON(value, path.field(INFO_LIT)); - case TYPE::CSOAFAF: + case TYPE::CopiedSlotsOfActiveForksAreFull: return CopiedSlotsOfActiveForkAreFull::fromJSON(value, path.field(INFO_LIT)); - case TYPE::PSSFO: + case TYPE::PathSingleSentForkOutput: return PathSingleSentForkOutput::fromJSON(value, path.field(INFO_LIT)); } } @@ -249,7 +249,7 @@ ValidEquivalence::fromJSON(const llvm::json::Value &value, EagerForkNotAllOutputSent::EagerForkNotAllOutputSent( unsigned long id, TAG tag, handshake::EagerForkLikeOpInterface &forkOp) - : FormalProperty(id, tag, TYPE::EFNAO) { + : FormalProperty(id, tag, TYPE::EagerForkNotAllOutputSent) { ownerOp = getUniqueName(forkOp).str(); numEagerForkOutputs = forkOp.getNumEagerOutputs(); } @@ -279,7 +279,7 @@ EagerForkNotAllOutputSent::fromJSON(const llvm::json::Value &value, CopiedSlotsOfActiveForkAreFull::CopiedSlotsOfActiveForkAreFull( unsigned long id, TAG tag, handshake::BufferLikeOpInterface &bufferOpI, handshake::EagerForkLikeOpInterface &forkOpI) - : FormalProperty(id, tag, TYPE::CSOAFAF) { + : FormalProperty(id, tag, TYPE::CopiedSlotsOfActiveForksAreFull) { forkOp = getUniqueName(forkOpI).str(); numEagerForkOutputs = forkOpI.getNumEagerOutputs(); bufferOp = getUniqueName(bufferOpI).str(); @@ -313,7 +313,7 @@ CopiedSlotsOfActiveForkAreFull::fromJSON(const llvm::json::Value &value, PathSingleSentForkOutput::PathSingleSentForkOutput( unsigned long id, TAG tag, const std::vector &forkOps, const std::vector &outputIdxs) - : FormalProperty(id, tag, TYPE::PSSFO), forkOps{forkOps}, + : FormalProperty(id, tag, TYPE::PathSingleSentForkOutput), forkOps{forkOps}, outputIdxs{outputIdxs} {} llvm::json::Value PathSingleSentForkOutput::extraInfoToJSON() const { From 023be439a94f39246ce3193e9fdd23a4f623c00b Mon Sep 17 00:00:00 2001 From: Bas Niekel Date: Thu, 5 Feb 2026 16:43:02 +0100 Subject: [PATCH 09/10] combined everything into a single function --- .../HandshakeAnnotateProperties.cpp | 96 +++++++------------ 1 file changed, 35 insertions(+), 61 deletions(-) diff --git a/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp b/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp index a3df927ea5..f0f42f1dbf 100644 --- a/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp +++ b/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp @@ -74,15 +74,7 @@ struct HandshakeAnnotatePropertiesPass LogicalResult annotateCopiedSlots(Operation &op); LogicalResult annotateCopiedSlotsOfAllForks(ModuleOp modOp); - LogicalResult annotatePathSingleForkSentPushProperty( - const std::vector &prevForks, - const std::vector &prevIdxs); - LogicalResult - annotatePathSingleForkSentDecide(std::unordered_set visitedSet, - const std::vector &prevForks, - const std::vector &prevIdxs, - Operation &curOp); - LogicalResult annotatePathSingleForkSentIterate( + LogicalResult annotatePathSingleForkSentRec( const std::unordered_set &visitedSet, const std::vector &prevForks, const std::vector &prevIdxs, Operation &curOp, @@ -239,53 +231,7 @@ HandshakeAnnotatePropertiesPass::annotateCopiedSlotsOfAllForks(ModuleOp modOp) { } LogicalResult -HandshakeAnnotatePropertiesPass::annotatePathSingleForkSentPushProperty( - const std::vector &prevForks, - const std::vector &prevIdxs) { - if (prevForks.size() != prevIdxs.size()) { - llvm::errs() << "Different Indexs size and forks size\n"; - return failure(); - } - // No need to annotate properties of length 1 or lower - if (prevForks.size() <= 1) { - return success(); - } - PathSingleSentForkOutput p(uid, FormalProperty::TAG::INVAR, prevForks, - prevIdxs); - propertyTable.push_back(p.toJSON()); - uid++; - return success(); -} - -LogicalResult HandshakeAnnotatePropertiesPass::annotatePathSingleForkSentDecide( - std::unordered_set visitedSet, - const std::vector &prevForks, - const std::vector &prevIdxs, Operation &curOp) { - - // If this operation has been visited, there is nothing to do - std::string id = getUniqueName(&curOp).str(); - if (auto iter = visitedSet.find(id); iter != visitedSet.end()) { - return success(); - } - visitedSet.insert(id); - - // Found a slot, which marks the end of this path - if (auto bufOp = dyn_cast(curOp)) { - return success(); - } - - if (auto forkOp = dyn_cast(curOp)) { - auto nextForks = prevForks; - nextForks.push_back(id); - return annotatePathSingleForkSentIterate(visitedSet, nextForks, prevIdxs, - curOp, true); - } - return annotatePathSingleForkSentIterate(visitedSet, prevForks, prevIdxs, - curOp, false); -} - -LogicalResult -HandshakeAnnotatePropertiesPass::annotatePathSingleForkSentIterate( +HandshakeAnnotatePropertiesPass::annotatePathSingleForkSentRec( const std::unordered_set &visitedSet, const std::vector &prevForks, const std::vector &prevIdxs, Operation &curOp, @@ -294,14 +240,42 @@ HandshakeAnnotatePropertiesPass::annotatePathSingleForkSentIterate( std::vector nextIdxs = prevIdxs; if (annotateIdxs) { nextIdxs.push_back(i); - if (failed(annotatePathSingleForkSentPushProperty(prevForks, nextIdxs))) { + if (prevForks.size() != nextIdxs.size()) { + llvm::errs() << "Different Indexs size and forks size\n"; return failure(); } + // No need to annotate properties of length 1 or lower + if (prevForks.size() > 1) { + PathSingleSentForkOutput p(uid, FormalProperty::TAG::INVAR, prevForks, + nextIdxs); + propertyTable.push_back(p.toJSON()); + uid++; + } } for (auto *op : res.getUsers()) { - if (failed(annotatePathSingleForkSentDecide(visitedSet, prevForks, - nextIdxs, *op))) { - return failure(); + // If this operation has been visited, there is nothing to do + std::string id = getUniqueName(op).str(); + if (auto iter = visitedSet.find(id); iter != visitedSet.end()) { + continue; + } + std::unordered_set newVisited = visitedSet; + newVisited.insert(id); + + // Found a slot, which marks the end of this path + if (auto bufOp = dyn_cast(op)) { + continue; + } + + if (auto forkOp = dyn_cast(op)) { + auto nextForks = prevForks; + nextForks.push_back(id); + if (failed(annotatePathSingleForkSentRec(newVisited, nextForks, nextIdxs, *op, true))) { + return failure(); + } + } else { + if (failed(annotatePathSingleForkSentRec(newVisited, prevForks, nextIdxs, *op, false))) { + return failure(); + } } } } @@ -317,7 +291,7 @@ HandshakeAnnotatePropertiesPass::annotatePathSingleForkSent(ModuleOp modOp) { std::vector outputs{}; std::unordered_set visited{}; names.push_back(getUniqueName(&op).str()); - if (failed(annotatePathSingleForkSentIterate(visited, names, outputs, + if (failed(annotatePathSingleForkSentRec(visited, names, outputs, op, true))) { return failure(); } From baeb978af278de8b11afc47ead2152f2f9862cb2 Mon Sep 17 00:00:00 2001 From: Bas Niekel Date: Thu, 5 Feb 2026 16:45:06 +0100 Subject: [PATCH 10/10] formatting --- .../HandshakeAnnotateProperties.cpp | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp b/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp index f0f42f1dbf..7790d0b72d 100644 --- a/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp +++ b/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp @@ -230,8 +230,7 @@ HandshakeAnnotatePropertiesPass::annotateCopiedSlotsOfAllForks(ModuleOp modOp) { return success(); } -LogicalResult -HandshakeAnnotatePropertiesPass::annotatePathSingleForkSentRec( +LogicalResult HandshakeAnnotatePropertiesPass::annotatePathSingleForkSentRec( const std::unordered_set &visitedSet, const std::vector &prevForks, const std::vector &prevIdxs, Operation &curOp, @@ -269,11 +268,13 @@ HandshakeAnnotatePropertiesPass::annotatePathSingleForkSentRec( if (auto forkOp = dyn_cast(op)) { auto nextForks = prevForks; nextForks.push_back(id); - if (failed(annotatePathSingleForkSentRec(newVisited, nextForks, nextIdxs, *op, true))) { + if (failed(annotatePathSingleForkSentRec(newVisited, nextForks, + nextIdxs, *op, true))) { return failure(); } } else { - if (failed(annotatePathSingleForkSentRec(newVisited, prevForks, nextIdxs, *op, false))) { + if (failed(annotatePathSingleForkSentRec(newVisited, prevForks, + nextIdxs, *op, false))) { return failure(); } } @@ -291,8 +292,8 @@ HandshakeAnnotatePropertiesPass::annotatePathSingleForkSent(ModuleOp modOp) { std::vector outputs{}; std::unordered_set visited{}; names.push_back(getUniqueName(&op).str()); - if (failed(annotatePathSingleForkSentRec(visited, names, outputs, - op, true))) { + if (failed(annotatePathSingleForkSentRec(visited, names, outputs, op, + true))) { return failure(); } }