From b99fb8d81e300e71d46cbb68250306e62d30e7d8 Mon Sep 17 00:00:00 2001 From: Bas Niekel Date: Tue, 30 Dec 2025 17:35:32 +0100 Subject: [PATCH 1/8] start of invariant 2 (copied slots of partially sent forks are full) --- .../experimental/Support/FormalProperty.h | 34 +++++++++++++++ .../HandshakeAnnotateProperties.cpp | 34 +++++++++++++++ experimental/lib/Support/FormalProperty.cpp | 41 +++++++++++++++++++ 3 files changed, 109 insertions(+) diff --git a/experimental/include/experimental/Support/FormalProperty.h b/experimental/include/experimental/Support/FormalProperty.h index 58dbef60a..246e7bb88 100644 --- a/experimental/include/experimental/Support/FormalProperty.h +++ b/experimental/include/experimental/Support/FormalProperty.h @@ -28,6 +28,7 @@ class FormalProperty { AOB /* Absence Of Backpressure */, VEQ /* Valid EQuivalence */, EFNAO /* Eager Fork Not All Output sent */, + INV2, }; TAG getTag() const { return tag; } @@ -187,6 +188,39 @@ class EagerForkNotAllOutputSent : public FormalProperty { inline static const StringLiteral NUM_EAGER_OUTPUTS_LIT = "num_eager_outputs"; }; +class Invariant2 : public FormalProperty { +public: + std::string getForkOp() { return forkOp; } + unsigned getNumEagerForkOutputs() { return numEagerForkOutputs; } + std::string getBufferOp() { return bufferOp; } + unsigned getBufferSlot() { return bufferSlot; } + + llvm::json::Value extraInfoToJSON() const override; + + static std::unique_ptr fromJSON(const llvm::json::Value &value, + llvm::json::Path path); + + Invariant2() = default; + Invariant2(unsigned long id, TAG tag, + handshake::BufferLikeOpInterface &bufferOp, + handshake::EagerForkLikeOpInterface &forkOp); + ~Invariant2() = default; + + static bool classof(const FormalProperty *fp) { + return fp->getType() == TYPE::INV2; + } + +private: + std::string forkOp; + unsigned numEagerForkOutputs; + std::string bufferOp; + unsigned bufferSlot; + inline static const StringLiteral FORK_OP_LIT = "fork_op"; + inline static const StringLiteral NUM_EAGER_OUTPUTS_LIT = "num_eager_outputs"; + inline static const StringLiteral BUFFER_OP_LIT = "buffer_op"; + inline static const StringLiteral BUFFER_SLOT_LIT = "buffer_slot"; +}; + class FormalPropertyTable { public: FormalPropertyTable() = default; diff --git a/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp b/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp index 25bb9275a..e69bd9ace 100644 --- a/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp +++ b/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp @@ -66,6 +66,9 @@ struct HandshakeAnnotatePropertiesPass LogicalResult annotateValidEquivalenceBetweenOps(Operation &op1, Operation &op2); LogicalResult annotateEagerForkNotAllOutputSent(ModuleOp modOp); + LogicalResult annotateCopiedSlots(handshake::EagerForkLikeOpInterface &forkOp, + Operation &op); + LogicalResult annotateInvariant2(ModuleOp modOp); bool isChannelToBeChecked(OpResult res); }; } // namespace @@ -153,6 +156,35 @@ HandshakeAnnotatePropertiesPass::annotateEagerForkNotAllOutputSent( return success(); } +LogicalResult HandshakeAnnotatePropertiesPass::annotateCopiedSlots( + handshake::EagerForkLikeOpInterface &originFork, Operation &curOp) { + if (auto bufferOp = dyn_cast(curOp)) { + Invariant2 p(uid, FormalProperty::TAG::INVAR, bufferOp, originFork); + propertyTable.push_back(p.toJSON()); + uid++; + } + + if (auto mergeOp = dyn_cast(curOp)) { + // TODO: Which of the previous paths should be followed? + return failure(); + } + + return success(); +} + +LogicalResult +HandshakeAnnotatePropertiesPass::annotateInvariant2(ModuleOp modOp) { + for (handshake::FuncOp funcOp : modOp.getOps()) { + for (Operation &op : funcOp.getOps()) { + if (auto forkOp = dyn_cast(op)) { + if (failed(annotateCopiedSlots(forkOp, op))) + return failure(); + } + } + } + return success(); +} + void HandshakeAnnotatePropertiesPass::runDynamaticPass() { ModuleOp modOp = getOperation(); @@ -163,6 +195,8 @@ void HandshakeAnnotatePropertiesPass::runDynamaticPass() { if (annotateInvariants) { if (failed(annotateEagerForkNotAllOutputSent(modOp))) return signalPassFailure(); + if (failed(annotateInvariant2(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 1cca1acc2..654e38a39 100644 --- a/experimental/lib/Support/FormalProperty.cpp +++ b/experimental/lib/Support/FormalProperty.cpp @@ -29,6 +29,8 @@ FormalProperty::typeFromStr(const std::string &s) { return FormalProperty::TYPE::VEQ; if (s == "EFNAO") return FormalProperty::TYPE::EFNAO; + if (s == "INV2") + return FormalProperty::TYPE::INV2; return std::nullopt; } @@ -41,6 +43,8 @@ std::string FormalProperty::typeToStr(TYPE t) { return "VEQ"; case TYPE::EFNAO: return "EFNAO"; + case TYPE::INV2: + return "INV2"; } } @@ -95,6 +99,8 @@ FormalProperty::fromJSON(const llvm::json::Value &value, return ValidEquivalence::fromJSON(value, path.field(INFO_LIT)); case TYPE::EFNAO: return EagerForkNotAllOutputSent::fromJSON(value, path.field(INFO_LIT)); + case TYPE::INV2: + return Invariant2::fromJSON(value, path.field(INFO_LIT)); } } @@ -261,6 +267,41 @@ EagerForkNotAllOutputSent::fromJSON(const llvm::json::Value &value, return prop; } +// Invariant 2 -- see https://ieeexplore.ieee.org/document/10323796 + +Invariant2::Invariant2(unsigned long id, TAG tag, + handshake::BufferLikeOpInterface &bufferOpI, + handshake::EagerForkLikeOpInterface &forkOpI) + : FormalProperty(id, tag, TYPE::INV2) { + forkOp = getUniqueName(forkOpI).str(); + numEagerForkOutputs = forkOpI.getNumEagerOutputs(); + bufferOp = getUniqueName(bufferOpI).str(); + bufferSlot = bufferOpI.getNumSlots() - 1; +} + +llvm::json::Value Invariant2::extraInfoToJSON() const { + return llvm::json::Object({{FORK_OP_LIT, forkOp}, + {NUM_EAGER_OUTPUTS_LIT, numEagerForkOutputs}, + {BUFFER_OP_LIT, bufferOp}, + {BUFFER_SLOT_LIT, bufferSlot}}); +} + +std::unique_ptr Invariant2::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_OP_LIT, prop->forkOp) || + !mapper.map(NUM_EAGER_OUTPUTS_LIT, prop->numEagerForkOutputs) || + !mapper.map(BUFFER_OP_LIT, prop->bufferOp) || + !mapper.map(BUFFER_SLOT_LIT, prop->bufferSlot)) + return nullptr; + + return prop; +} + LogicalResult FormalPropertyTable::addPropertiesFromJSON(StringRef filepath) { // Open the properties' database std::ifstream inputFile(filepath.str()); From 1cea330e69de93eb4c4f389ecb3da785e6324e64 Mon Sep 17 00:00:00 2001 From: Bas Niekel Date: Fri, 2 Jan 2026 16:02:26 +0100 Subject: [PATCH 2/8] traverse to copied slots without loop checking --- .../HandshakeAnnotateProperties.cpp | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) diff --git a/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp b/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp index e69bd9ace..20fe521dc 100644 --- a/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp +++ b/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp @@ -67,7 +67,7 @@ struct HandshakeAnnotatePropertiesPass Operation &op2); LogicalResult annotateEagerForkNotAllOutputSent(ModuleOp modOp); LogicalResult annotateCopiedSlots(handshake::EagerForkLikeOpInterface &forkOp, - Operation &op); + Operation &curOp); LogicalResult annotateInvariant2(ModuleOp modOp); bool isChannelToBeChecked(OpResult res); }; @@ -158,6 +158,8 @@ HandshakeAnnotatePropertiesPass::annotateEagerForkNotAllOutputSent( LogicalResult HandshakeAnnotatePropertiesPass::annotateCopiedSlots( handshake::EagerForkLikeOpInterface &originFork, Operation &curOp) { + // TODO: avoid loops by checking if curOp has been visited already + if (auto bufferOp = dyn_cast(curOp)) { Invariant2 p(uid, FormalProperty::TAG::INVAR, bufferOp, originFork); propertyTable.push_back(p.toJSON()); @@ -169,6 +171,20 @@ LogicalResult HandshakeAnnotatePropertiesPass::annotateCopiedSlots( return failure(); } + // Only JoinLikeOps or single-operand ops are remaining, but ideally a + // dyn_cast would happen for either case + for (auto value : curOp.getOperands()) { + Operation *prevOpPtr = value.getDefiningOp(); + if (prevOpPtr == nullptr) + // if there is no defining op, the value must be a constant, and does not + // need to be annotated + continue; + Operation &prevOp = *prevOpPtr; + if (failed(annotateCopiedSlots(originFork, prevOp))) { + return failure(); + } + } + return success(); } From e3528489ee21965896a95d211c968e076017a8f9 Mon Sep 17 00:00:00 2001 From: Bas Niekel Date: Fri, 2 Jan 2026 17:03:29 +0100 Subject: [PATCH 3/8] loop detection --- .../HandshakeAnnotateProperties.cpp | 47 ++++++++++++++----- 1 file changed, 34 insertions(+), 13 deletions(-) diff --git a/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp b/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp index 20fe521dc..44f927a0a 100644 --- a/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp +++ b/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp @@ -35,6 +35,7 @@ #include "llvm/Support/JSON.h" #include #include +#include using namespace llvm; using namespace mlir; @@ -66,9 +67,12 @@ struct HandshakeAnnotatePropertiesPass LogicalResult annotateValidEquivalenceBetweenOps(Operation &op1, Operation &op2); LogicalResult annotateEagerForkNotAllOutputSent(ModuleOp modOp); - LogicalResult annotateCopiedSlots(handshake::EagerForkLikeOpInterface &forkOp, - Operation &curOp); - LogicalResult annotateInvariant2(ModuleOp modOp); + LogicalResult + annotateCopiedSlotsRec(std::unordered_set &visitedSet, + handshake::EagerForkLikeOpInterface &originFork, + Operation &curOp); + LogicalResult annotateCopiedSlots(Operation &op); + LogicalResult annotateCopiedSlotsOfAllForks(ModuleOp modOp); bool isChannelToBeChecked(OpResult res); }; } // namespace @@ -156,19 +160,29 @@ HandshakeAnnotatePropertiesPass::annotateEagerForkNotAllOutputSent( return success(); } -LogicalResult HandshakeAnnotatePropertiesPass::annotateCopiedSlots( +LogicalResult HandshakeAnnotatePropertiesPass::annotateCopiedSlotsRec( + std::unordered_set &visitedSet, handshake::EagerForkLikeOpInterface &originFork, Operation &curOp) { - // TODO: avoid loops by checking if curOp has been visited already + // 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); + + // If this operation contains a slot, the copied slot has been found and can + // be annotated if (auto bufferOp = dyn_cast(curOp)) { Invariant2 p(uid, FormalProperty::TAG::INVAR, bufferOp, originFork); propertyTable.push_back(p.toJSON()); uid++; + return success(); } if (auto mergeOp = dyn_cast(curOp)) { // TODO: Which of the previous paths should be followed? - return failure(); + return success(); } // Only JoinLikeOps or single-operand ops are remaining, but ideally a @@ -180,7 +194,7 @@ LogicalResult HandshakeAnnotatePropertiesPass::annotateCopiedSlots( // need to be annotated continue; Operation &prevOp = *prevOpPtr; - if (failed(annotateCopiedSlots(originFork, prevOp))) { + if (failed(annotateCopiedSlotsRec(visitedSet, originFork, prevOp))) { return failure(); } } @@ -189,13 +203,20 @@ LogicalResult HandshakeAnnotatePropertiesPass::annotateCopiedSlots( } LogicalResult -HandshakeAnnotatePropertiesPass::annotateInvariant2(ModuleOp modOp) { +HandshakeAnnotatePropertiesPass::annotateCopiedSlots(Operation &op) { + std::unordered_set visitedSet = {}; + if (auto forkOp = dyn_cast(op)) { + return annotateCopiedSlotsRec(visitedSet, forkOp, op); + } + return success(); +} + +LogicalResult +HandshakeAnnotatePropertiesPass::annotateCopiedSlotsOfAllForks(ModuleOp modOp) { for (handshake::FuncOp funcOp : modOp.getOps()) { for (Operation &op : funcOp.getOps()) { - if (auto forkOp = dyn_cast(op)) { - if (failed(annotateCopiedSlots(forkOp, op))) - return failure(); - } + if (failed(annotateCopiedSlots(op))) + return failure(); } } return success(); @@ -211,7 +232,7 @@ void HandshakeAnnotatePropertiesPass::runDynamaticPass() { if (annotateInvariants) { if (failed(annotateEagerForkNotAllOutputSent(modOp))) return signalPassFailure(); - if (failed(annotateInvariant2(modOp))) + if (failed(annotateCopiedSlotsOfAllForks(modOp))) return signalPassFailure(); } From e8e950a7a9705403ea359a760e2489c90358f129 Mon Sep 17 00:00:00 2001 From: Bas Niekel Date: Sat, 3 Jan 2026 13:37:57 +0100 Subject: [PATCH 4/8] outputting invariant 2 to the smv model --- tools/export-rtl/export-rtl.cpp | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/tools/export-rtl/export-rtl.cpp b/tools/export-rtl/export-rtl.cpp index 61ae48936..fab9ce593 100644 --- a/tools/export-rtl/export-rtl.cpp +++ b/tools/export-rtl/export-rtl.cpp @@ -1268,6 +1268,22 @@ LogicalResult SMVWriter::createProperties(WriteModData &data) const { // e.g. count(fork0.sent_0, fork0.sent_1) < 2 // for operation "fork0" with 2 eager outputs data.properties[p->getId()] = {propertyString, propertyTag}; + } else if (auto *p = llvm::dyn_cast(property.get())) { + unsigned numOut = p->getNumEagerForkOutputs(); + std::string forkName = p->getForkOp(); + std::string bufferName = p->getBufferOp(); + int bufferSlot = p->getBufferSlot(); + std::vector forkOutNames{numOut}; + for (unsigned i = 0; i < numOut; ++i) { + forkOutNames[i] = llvm::formatv("{0}.sent_{1}", forkName, i).str(); + } + std::string bufferFull = + llvm::formatv("{0}.full_{1}", bufferName, bufferSlot).str(); + std::string propertyString = + llvm::formatv("({0}) -> {1}", llvm::join(forkOutNames, " | "), + bufferFull) + .str(); + data.properties[p->getId()] = {propertyString, propertyTag}; } else { llvm::errs() << "Formal property Type not known\n"; return failure(); From 4b1b7a3cd0adeffac265ed784b5a6820073fc7e3 Mon Sep 17 00:00:00 2001 From: Bas Niekel Date: Sat, 3 Jan 2026 13:54:43 +0100 Subject: [PATCH 5/8] full_0 naming of single-slot buffers (including control merges) --- .../smv/generators/handshake/buffers/one_slot_break_dv.py | 1 + .../smv/generators/handshake/buffers/one_slot_break_r.py | 2 ++ .../unit-generators/smv/generators/handshake/control_merge.py | 2 ++ 3 files changed, 5 insertions(+) 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 4d349bff8..9b9caf079 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 @@ -46,6 +46,7 @@ def _generate_one_slot_break_dv(name, data_type): ins_ready := inner_one_slot_break_dv.ins_ready; outs_valid := inner_one_slot_break_dv.outs_valid; outs := data; + full_0 := inner_one_slot_break_dv.outs_valid_i; {_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 772c81d3c..e5e8a3195 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,6 +24,7 @@ def _generate_one_slot_break_r_dataless(name): DEFINE ins_ready := !full; outs_valid := ins_valid | full; + full_0 := full; """ @@ -43,6 +44,7 @@ def _generate_one_slot_break_r(name, data_type): ins_ready := inner_one_slot_break_r.ins_ready; outs_valid := inner_one_slot_break_r.outs_valid; outs := inner_one_slot_break_r.full ? data : ins; + full_0 := 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/control_merge.py b/experimental/tools/unit-generators/smv/generators/handshake/control_merge.py index ae88f8eec..8220eac74 100644 --- a/experimental/tools/unit-generators/smv/generators/handshake/control_merge.py +++ b/experimental/tools/unit-generators/smv/generators/handshake/control_merge.py @@ -36,6 +36,7 @@ def _generate_control_merge_dataless(name, size, index_type): outs_valid := inner_fork.outs_0_valid; index_valid := inner_fork.outs_1_valid; index := inner_one_slot_break_r.outs; + full_0 := inner_one_slot_break_r.full_0; {generate_merge(f"{name}__merge_dataless", {ATTR_SIZE: size, ATTR_BITWIDTH: 0})} {generate_one_slot_break_r(f"{name}__one_slot_break_r", {ATTR_BITWIDTH: index_type.bitwidth})} @@ -62,6 +63,7 @@ def _generate_control_merge(name, size, index_type, data_type): index_valid := inner_control_merge.index_valid; outs := data; index := inner_control_merge.index; + full_0 := inner_control_merge.full_0; {_generate_control_merge_dataless(f"{name}__control_merge_dataless", size, index_type)} """ From 4d2caac33ea0ec303b54a7d611439116ace58336 Mon Sep 17 00:00:00 2001 From: Bas Niekel Date: Tue, 6 Jan 2026 10:29:08 +0100 Subject: [PATCH 6/8] sensible naming of invariant 2 --- .../experimental/Support/FormalProperty.h | 20 ++++++------- .../HandshakeAnnotateProperties.cpp | 3 +- experimental/lib/Support/FormalProperty.cpp | 30 ++++++++++--------- tools/export-rtl/export-rtl.cpp | 3 +- 4 files changed, 30 insertions(+), 26 deletions(-) diff --git a/experimental/include/experimental/Support/FormalProperty.h b/experimental/include/experimental/Support/FormalProperty.h index 246e7bb88..c6eb33ea9 100644 --- a/experimental/include/experimental/Support/FormalProperty.h +++ b/experimental/include/experimental/Support/FormalProperty.h @@ -28,7 +28,7 @@ class FormalProperty { AOB /* Absence Of Backpressure */, VEQ /* Valid EQuivalence */, EFNAO /* Eager Fork Not All Output sent */, - INV2, + CSOAFAF, /* Copied Slots Of Active Forks Are Full */ }; TAG getTag() const { return tag; } @@ -188,7 +188,7 @@ class EagerForkNotAllOutputSent : public FormalProperty { inline static const StringLiteral NUM_EAGER_OUTPUTS_LIT = "num_eager_outputs"; }; -class Invariant2 : public FormalProperty { +class CopiedSlotsOfActiveForkAreFull : public FormalProperty { public: std::string getForkOp() { return forkOp; } unsigned getNumEagerForkOutputs() { return numEagerForkOutputs; } @@ -197,17 +197,17 @@ class Invariant2 : public FormalProperty { llvm::json::Value extraInfoToJSON() const override; - static std::unique_ptr fromJSON(const llvm::json::Value &value, - llvm::json::Path path); + static std::unique_ptr + fromJSON(const llvm::json::Value &value, llvm::json::Path path); - Invariant2() = default; - Invariant2(unsigned long id, TAG tag, - handshake::BufferLikeOpInterface &bufferOp, - handshake::EagerForkLikeOpInterface &forkOp); - ~Invariant2() = default; + CopiedSlotsOfActiveForkAreFull() = default; + CopiedSlotsOfActiveForkAreFull(unsigned long id, TAG tag, + handshake::BufferLikeOpInterface &bufferOp, + handshake::EagerForkLikeOpInterface &forkOp); + ~CopiedSlotsOfActiveForkAreFull() = default; static bool classof(const FormalProperty *fp) { - return fp->getType() == TYPE::INV2; + return fp->getType() == TYPE::CSOAFAF; } private: diff --git a/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp b/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp index 44f927a0a..92e6b6b94 100644 --- a/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp +++ b/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp @@ -174,7 +174,8 @@ LogicalResult HandshakeAnnotatePropertiesPass::annotateCopiedSlotsRec( // If this operation contains a slot, the copied slot has been found and can // be annotated if (auto bufferOp = dyn_cast(curOp)) { - Invariant2 p(uid, FormalProperty::TAG::INVAR, bufferOp, originFork); + CopiedSlotsOfActiveForkAreFull p(uid, FormalProperty::TAG::INVAR, bufferOp, + originFork); propertyTable.push_back(p.toJSON()); uid++; return success(); diff --git a/experimental/lib/Support/FormalProperty.cpp b/experimental/lib/Support/FormalProperty.cpp index 654e38a39..94cca64a9 100644 --- a/experimental/lib/Support/FormalProperty.cpp +++ b/experimental/lib/Support/FormalProperty.cpp @@ -29,8 +29,8 @@ FormalProperty::typeFromStr(const std::string &s) { return FormalProperty::TYPE::VEQ; if (s == "EFNAO") return FormalProperty::TYPE::EFNAO; - if (s == "INV2") - return FormalProperty::TYPE::INV2; + if (s == "CSOAFAF") + return FormalProperty::TYPE::CSOAFAF; return std::nullopt; } @@ -43,8 +43,8 @@ std::string FormalProperty::typeToStr(TYPE t) { return "VEQ"; case TYPE::EFNAO: return "EFNAO"; - case TYPE::INV2: - return "INV2"; + case TYPE::CSOAFAF: + return "CSOAFAF"; } } @@ -99,8 +99,9 @@ FormalProperty::fromJSON(const llvm::json::Value &value, return ValidEquivalence::fromJSON(value, path.field(INFO_LIT)); case TYPE::EFNAO: return EagerForkNotAllOutputSent::fromJSON(value, path.field(INFO_LIT)); - case TYPE::INV2: - return Invariant2::fromJSON(value, path.field(INFO_LIT)); + case TYPE::CSOAFAF: + return CopiedSlotsOfActiveForkAreFull::fromJSON(value, + path.field(INFO_LIT)); } } @@ -269,26 +270,27 @@ EagerForkNotAllOutputSent::fromJSON(const llvm::json::Value &value, // Invariant 2 -- see https://ieeexplore.ieee.org/document/10323796 -Invariant2::Invariant2(unsigned long id, TAG tag, - handshake::BufferLikeOpInterface &bufferOpI, - handshake::EagerForkLikeOpInterface &forkOpI) - : FormalProperty(id, tag, TYPE::INV2) { +CopiedSlotsOfActiveForkAreFull::CopiedSlotsOfActiveForkAreFull( + unsigned long id, TAG tag, handshake::BufferLikeOpInterface &bufferOpI, + handshake::EagerForkLikeOpInterface &forkOpI) + : FormalProperty(id, tag, TYPE::CSOAFAF) { forkOp = getUniqueName(forkOpI).str(); numEagerForkOutputs = forkOpI.getNumEagerOutputs(); bufferOp = getUniqueName(bufferOpI).str(); bufferSlot = bufferOpI.getNumSlots() - 1; } -llvm::json::Value Invariant2::extraInfoToJSON() const { +llvm::json::Value CopiedSlotsOfActiveForkAreFull::extraInfoToJSON() const { return llvm::json::Object({{FORK_OP_LIT, forkOp}, {NUM_EAGER_OUTPUTS_LIT, numEagerForkOutputs}, {BUFFER_OP_LIT, bufferOp}, {BUFFER_SLOT_LIT, bufferSlot}}); } -std::unique_ptr Invariant2::fromJSON(const llvm::json::Value &value, - llvm::json::Path path) { - auto prop = std::make_unique(); +std::unique_ptr +CopiedSlotsOfActiveForkAreFull::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); diff --git a/tools/export-rtl/export-rtl.cpp b/tools/export-rtl/export-rtl.cpp index fab9ce593..66f782651 100644 --- a/tools/export-rtl/export-rtl.cpp +++ b/tools/export-rtl/export-rtl.cpp @@ -1268,7 +1268,8 @@ LogicalResult SMVWriter::createProperties(WriteModData &data) const { // e.g. count(fork0.sent_0, fork0.sent_1) < 2 // for operation "fork0" with 2 eager outputs data.properties[p->getId()] = {propertyString, propertyTag}; - } else if (auto *p = llvm::dyn_cast(property.get())) { + } else if (auto *p = llvm::dyn_cast( + property.get())) { unsigned numOut = p->getNumEagerForkOutputs(); std::string forkName = p->getForkOp(); std::string bufferName = p->getBufferOp(); From 2bb1ca67292d7562b7c12eefa07d82ad713f46cf Mon Sep 17 00:00:00 2001 From: Bas Niekel Date: Thu, 15 Jan 2026 13:57:01 +0100 Subject: [PATCH 7/8] invariants are usually turned off, unless flag is given --- experimental/include/experimental/Analysis/Passes.td | 2 +- experimental/tools/rigidification/rigidification.sh | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/experimental/include/experimental/Analysis/Passes.td b/experimental/include/experimental/Analysis/Passes.td index c49af6cc2..ef4c4fefe 100644 --- a/experimental/include/experimental/Analysis/Passes.td +++ b/experimental/include/experimental/Analysis/Passes.td @@ -26,7 +26,7 @@ def HandshakeAnnotateProperties : DynamaticPass< "handshake-annotate-properties" let constructor = "dynamatic::experimental::formalprop::createAnnotateProperties()"; let options = [ Option<"jsonPath", "json-path", "std::string", "", "Path to JSON-formatted file where the properties' information is stored.">, - Option<"annotateInvariants", "annotate-invariants", "bool", "true", + Option<"annotateInvariants", "annotate-invariants", "bool", "false", "Annotate invariants to assist k-inductive proofs">]; } diff --git a/experimental/tools/rigidification/rigidification.sh b/experimental/tools/rigidification/rigidification.sh index 153fee744..8e870e674 100644 --- a/experimental/tools/rigidification/rigidification.sh +++ b/experimental/tools/rigidification/rigidification.sh @@ -34,7 +34,7 @@ rm -rf "$FORMAL_DIR" && mkdir -p "$FORMAL_DIR" # Annotate properties "$DYNAMATIC_OPT_BIN" "$F_HANDSHAKE_EXPORT" \ - --handshake-annotate-properties=json-path=$F_FORMAL_PROP \ + --handshake-annotate-properties="json-path=$F_FORMAL_PROP annotate-invariants" \ > /dev/null # handshake level -> hw level From e5863f137fcc89790413ae80de6c28029e3ed4fb Mon Sep 17 00:00:00 2001 From: Bas Niekel Date: Thu, 15 Jan 2026 14:10:30 +0100 Subject: [PATCH 8/8] explaining comment for 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 c6eb33ea9..11d5b181d 100644 --- a/experimental/include/experimental/Support/FormalProperty.h +++ b/experimental/include/experimental/Support/FormalProperty.h @@ -188,6 +188,13 @@ class EagerForkNotAllOutputSent : public FormalProperty { inline static const StringLiteral NUM_EAGER_OUTPUTS_LIT = "num_eager_outputs"; }; +// When an eager fork is `sent` state for at least one of its outputs, it is +// considered `active`. When transitioning to the `active` state, the `ready` +// signal is false, and the incoming token is blocked. Because of this, all +// slots immediately before the fork (i.e. copied slots) must be full. More +// formally, a copied slot of a fork is defined as a slot that has a path +// towards the fork without any other slots on it. See invariant 2 of +// https://ieeexplore.ieee.org/document/10323796 for more details class CopiedSlotsOfActiveForkAreFull : public FormalProperty { public: std::string getForkOp() { return forkOp; }