[Formal][Property Annotation] Annotating Exit Token Invariants by Basmet0 · Pull Request #922 · EPFL-LAP/dynamatic

Basmet0 · 2026-05-18T10:22:32Z

An exit token - meaning a token that decides whether a loop exits or continues - can only occur once. There will be other decider tokens before an exit token, and, given that there is an exit token, no ancestors of the decider will contain a token.

1. Within an IOG, find all deciding branches (between looping or never coming back) 2. Find the decider operation making the condition 3. Search forward for all branches coming out of the decider. These are all exit branches.

…tation rather than recomputing

Jiahui17 · 2026-05-21T10:47:09Z

+struct BranchOpDecision {
+  // true -> this branch loops towards itself
+  // false -> this branch exits
+  bool trueLoop;
+  bool falseLoop;
+
+  inline bool isExitBranch() { return trueLoop != falseLoop; }
+};
+
+BranchOpDecision findBranchLoops(const IOG &iog, ConditionalBranchOp branch) {
+  BranchOpDecision ret;
+  Operation *opTrue = *branch.getTrueResult().getUsers().begin();
+  auto paths = iog.findAllPaths(opTrue, branch);
+  ret.trueLoop = !(paths.units.find(branch) == paths.units.end());
+
+  Operation *opFalse = *branch.getFalseResult().getUsers().begin();
+  paths = iog.findAllPaths(opFalse, branch);
+  ret.falseLoop = !(paths.units.find(branch) == paths.units.end());
+  return ret;
+}


Suggestions:

Maybe just call it isIOGLoopExitBranch(..) (returns a Boolean value instead)? We can omit the new custom type in that case

Could be declared as a class method of IOG

Jiahui17 · 2026-05-21T10:56:48Z

+Operation *getDecider(ConditionalBranchOp branch) {
+  std::vector<mlir::Value> stack;
+  stack.push_back(branch.getConditionOperand());
+  Operation *dec = branch;
+  while (!stack.empty()) {
+    mlir::Value cur = stack.back();
+    stack.pop_back();
+    Operation *op = cur.getDefiningOp();
+
+    if (!op) {
+      continue;
+    }
+    dec = op;
+
+    if (auto forkOp = dyn_cast<ForkOp>(op)) {
+      stack.push_back(forkOp.getOperand());
+    }
+    if (auto buffer = dyn_cast<BufferOp>(op)) {
+      stack.push_back(buffer.getOperand());
+    }
+  }
+  return dec;
+}


Suggestions:

// a decider is ....

we could return a std::optional<Operation *> (or llvm::FailureOr<Operation*>) and encode "we didn't find a decider" as nullopt

The parent function returns failure() if no decider was discovered

use else if

For instance, if op is somehow a nullptr we should return a nullopt

Jiahui17 · 2026-05-21T11:08:14Z

remove this from the PR

comments for decider/unstartedPath

Jiahui17 · 2026-05-23T11:44:06Z

+          iogBranch = slots.end;
+        }
+      }
+      assert(iogBranch);


return failure()

Jiahui17 · 2026-05-23T11:54:10Z

+    Operation *dec = *getDecider(branch);
+    deciders.insert({dec, exitValue});
+  }
+  for (auto [dec, exitValue] : deciders) {


The loop body here is quite long, i think it makes sense to put some markers to visually separate the code for different invariants:

// [START Enumerating ExitTokenOrder invariants] for (const auto &slots : slotPaths) { ... propertyTable.push_back(p.toJSON()); } // [END Enumerating ExitTokenOrder invariants] // [START Enumerating ExitTokenNoAncestors invariants] // [END Enumerating ExitTokenNoAncestors invariants]

Jiahui17 · 2026-05-23T12:02:29Z

  inline static const StringLiteral PATH_CM_LIT = "cmerge_mux_path";
 };

+// In a path between a decider unit and a branch, only the first token along the


I think it helps to include an example like this in the comment to make the description easier to understand

Also the UnstartedPath can reference this diagram/example

BTW Slot followed by any number of EForks can be shortened with EffectiveSlot

BTW the descriptions you added there are informative, it is just that the thing we want to describe is generally quite convoluted and we want to visualize this part for the reader

Jiahui17 · 2026-05-23T12:08:18Z

+    }
+
+    Operation *op = cur.channel.getDefiningOp();
+    if (!op || !iog.contains(op) || op == exit ||


Suggestions

Order the cases as generating more returns paths (each input of a multi-input unit), populating one return path (Buffer), and terminination condition

Explain the termination condition in more detail?

Use if .. else if

In this function, the operations are not handled case-by-case, but instead using their interfaces as any operation is allowed here. The order cannot be changed without breaking the behaviour:
First, terminate in bad cases (otherwise potentially too many things are annotated).
Second, if applicable, an eager fork output is added as a copied sent to the next slot.
Third, slots are annotated.
Lastly, all inputs are followed backwards (regardless of the number of inputs, can be 1 for buffer or fork, or 2 for arithmetic operations or loads)
I added some comments to explain this in code as well

Yes, comment added

Similar to 1., if .. else if does not make sense here as I am not handling different cases but instead following the same four steps for any operation.

Jiahui17 · 2026-05-23T12:09:24Z

+    std::vector<EffectiveSlotNamer> backPath;
+    std::vector<EagerForkSentNamer> backSents;


forward vs. backward: conceptually which one do you call forward?

Jiahui17 · 2026-05-23T12:12:02Z

+    stack.pop_back();
+
+    Operation *next = *path.cur.getUsers().begin();
+    if (auto branch = dyn_cast<ConditionalBranchOp>(next)) {


Same suggestions as the other similar loop:

Suggestions

Order the cases as generating more returns paths (each input of a multi-input unit), populating one return path (Buffer), and terminination condition

Explain the termination condition in more detail?

Use if .. else if

Here that does make sense yes

Jiahui17 · 2026-05-23T12:13:11Z

+  }
+}
+
+// Paths from decider to the branch might contain a fork before they contain a


remember to backreference the diagram I added in the other comment

Bas Niekel added 27 commits April 30, 2026 19:04

boilerplate for effective slot namers

1257f0f

annotate entry token order

48d930b

export-rtl for entry token order invariant

ede91d4

determine which value is the entry value

387ed2d

fixed smv generation to expect later slots empty

ab3e5ee

Merge branch 'main' into invariant7

de5cff5

cleanup of debug logs, cleanup and verification of smv output

3d75415

json using updated json

f80acfa

annotate invariant 8

ce23950

invariant to smv

56317e2

fixed some bugs with json parsing of invariant

2974425

removed git merge conflict

381d6af

fixed json, verification of invariant 8

7bdd09a

pathfinding and logic for invariant 9

9110ce6

formal property struct and type boilerplate

851c6fa

attempt of fixing exit-branch detection by finding condition input

318eadc

Merge branch 'main' into invariant9

05984c3

New algorithm for finding exit branches:

6469528

1. Within an IOG, find all deciding branches (between looping or never coming back) 2. Find the decider operation making the condition 3. Search forward for all branches coming out of the decider. These are all exit branches.

Merge branch 'main' into invariant7

ec42c7b

Merge branch 'invariant7' into invariant8

1dc5bd2

entry slot namer now performs BlockArgument name lookup internally

2a05d33

Merge branch 'invariant8' into invariant9

a88c073

cleaned up unused functions, pass IOG as argument to exit-token compu…

9d399a7

…tation rather than recomputing

finding ancestors of deciders, annotating appropriate paths

85afc18

generate smv for exit-token-no-ancestors invariant

ccaccfa

fix: No longer annotate paths of length 0

4dd8db8

formatting

e5ed814

Basmet0 changed the base branch from main to invariant8 May 19, 2026 14:51

Bas Niekel added 2 commits May 21, 2026 10:20

Merge branch 'main' into invariant10

bea03ce

descriptions of invariants

3bc19ea

Basmet0 changed the base branch from invariant8 to main May 21, 2026 08:34

Basmet0 changed the title ~~[Formal][Property Annotation] Annotating invariants 7,8,9,10~~ [Formal][Property Annotation] Annotating Exit Token Invariants May 21, 2026

Basmet0 requested a review from Jiahui17 May 21, 2026 08:39

Jiahui17 reviewed May 22, 2026

View reviewed changes

Bas Niekel added 2 commits May 22, 2026 19:07

fixes according to PR: Restructuring of branch loop finding,

eee01c1

comments for decider/unstartedPath

Merge branch 'main' into invariant10

c504080

Jiahui17 reviewed May 23, 2026

View reviewed changes

more comments

bbfa08e

		std::vector<EffectiveSlotNamer> backPath;
		std::vector<EagerForkSentNamer> backSents;

Conversation

Basmet0 commented May 18, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Basmet0 commented May 18, 2026 •

edited

Loading