[FTD] Introduce Single-Occurrence MUX Trees for Suppression #613

QinYuan2000 · 2025-10-07T01:00:58Z

Motivation

This PR redesigns the suppression logic used in the Fast Token Delivery (FTD) flow.
Previously, the suppression circuit was generated from a Shannon-expansion–based MUX tree,
where the same condition variable could appear multiple times along different paths.
This duplication required additional “suppression” steps to eliminate redundant conditions.

We introduce a new Single-Occurrence MUX Tree built from a read-once Reduced Ordered Binary
Decision Diagram (ROBDD):

The ROBDD
A minimized BDD where each boolean variable is represented by exactly one node (read-once property).
It is constructed from an already minimized BoolExpression under a user-provided variable order.
Single-Occurrence MUX Tree
Using the ROBDD, we generate a MUX tree in which each condition variable
appears exactly once. The resulting circuit requires only a single suppression step
for each token delivery, simplifying both the FTD logic and the generated hardware.

Implementation

Added a class with several functions in BDD.{h,cpp} to build and analyze ROBDDs.
Implemented enumeration of vertex pairs that cover all the paths from the root to either terminal in the
BDD subgraph to guide MUX tree construction.
Updated FtdImplementation to build the new single-occurrence MUX tree directly from the
ROBDD, avoiding repeated conditions and redundant suppression.

AyaElAkhras · 2025-10-24T12:13:16Z

Thanks, Yuan! As discussed in our meeting, let's review more literature to determine whether we can replace your Read-Once BDD with the standard Reduced-Order BDD. After that, I will start reviewing the PR. :)

QinYuan2000 · 2025-11-04T22:05:50Z

@AyaElAkhras This is ready for review.
In this update, I’ve merged the ROBDD class into BDD.h. For simplicity, I kept the original lightweight ROBDD construction approach, instead of the canonical one that starts from an OBDD and merges identical subgraphs.

QinYuan2000 · 2025-11-04T23:31:22Z

I haven’t merged with the main branch yet because my changes would remove the channelification logic introduced in #604.
According to that update,

In addition, in boolVariableToCircuit, conditions generated for gates with multiple exiting blocks do not require channelification.

However, that behavior was based on the old approach for constructing circuits from BDDs, and I’ve now replaced all the related functions. I have to figure out what that actually means before merging.

experimental/lib/Support/FtdImplementation.cpp

experimental/include/experimental/Support/BooleanLogic/BDD.h

AyaElAkhras · 2025-11-05T20:34:58Z

experimental/include/experimental/Support/BooleanLogic/ROBDD.h

+  /// Variables in `varOrder` that do not appear in the expression are ignored.
+  /// Returns `success()` on success, or `failure()` if the input is invalid.
+  ///
+  /// This is a simple method that assumes each variable appears only once in


I find this comment somewhat ambiguous. The function itself creates the ROBDD, so it doesn’t make any assumptions about it. Did you mean something like “the function constructs an ROBDD structure in which each node is unique, with every node representing a single variable and no two nodes representing the same variable”?

I also find the connection to “whether a basic block in the CFG can be reached” unclear and in need of further elaboration. You might want to refer to the properties of an ROBDD—specifically, that it contains no duplicate equivalent subtrees and no two nodes with identical children. By construction, this ensures that no two nodes can correspond to the same variable (i.e., CFG basic block), assuming it’s not possible for two nodes representing the same variable to have different children, which is a valid assumption given that we start from CFGs? Does that interpretation make sense, or am I misunderstanding your point?

You are right that a general ROBDD allows multiple nodes for the same variable (representing different sub-functions). However, for this specific use case (CFG reachability analysis), the structure is simpler.

I implemented a lightweight version where each variable in the order maps to exactly one node in the BDD structure (or is skipped). This exploits the property that in our CFG analysis, we don't need the full expressiveness of a general ROBDD, allowing for a more efficient, linear-sized construction. I will clarify this 'single-node-per-variable' design constraint in the comments.

experimental/include/experimental/Support/BooleanLogic/ROBDD.h

experimental/lib/Support/BooleanLogic/BDD.cpp

AyaElAkhras · 2025-11-05T21:05:53Z

experimental/lib/Support/BooleanLogic/ROBDD.cpp

+  // Minimize the whole expression once before starting.
+  BoolExpression *rootExpr = expr->boolMinimize();
+
+  // If the expression itself is constant, build only two terminals.


I'm confused here: if the expression is a constant, why do you create two nodes instead of just one?

And, why do you write to trueSucc and falseSucc? Shouldn't it be a single node with no predecessors or successors?

Good catch regarding the successors. Terminals indeed act as leaves, so I've updated the code to set their successors to an invalid marker (UINT_MAX) instead of creating self-loops.

Regarding the two nodes: While strictly speaking only one node is reachable for a constant expression, I instantiate both 0 and 1 terminals to maintain internal consistency for the zeroIndex and oneIndex members of the ROBDD class. This ensures that helper methods accessing these terminals always find valid nodes, avoiding edge-case logic elsewhere.

experimental/lib/Support/BooleanLogic/ROBDD.cpp

AyaElAkhras · 2025-11-05T21:21:39Z

I haven’t merged with the main branch yet because my changes would remove the channelification logic introduced in #604. According to that update,
In addition, in boolVariableToCircuit, conditions generated for gates with multiple exiting blocks do not require channelification.
However, that behavior was based on the old approach for constructing circuits from BDDs, and I’ve now replaced all the related functions. I have to figure out what that actually means before merging.

I think it will be easier to discuss this when we meet, so please bring it up in our next meeting.

AyaElAkhras · 2025-11-05T21:22:53Z

@AyaElAkhras This is ready for review. In this update, I’ve merged the ROBDD class into BDD.h. For simplicity, I kept the original lightweight ROBDD construction approach, instead of the canonical one that starts from an OBDD and merges identical subgraphs.

Thanks @QinYuan2000! I did an initial round and left a few comments. I still plan to do another round tomorrow because I did not get to go through everything now.

AyaElAkhras

A tiny second round :)

I still need to review buildMuxTree and then should be done. Will try to do it in the next few hours...

AyaElAkhras · 2025-11-07T10:59:33Z

experimental/lib/Support/BooleanLogic/ROBDD.cpp

+      continue;
+
+    // Abort if we accidentally reach the global terminals.
+    if (u == zeroIndex || u == oneIndex) {


Isn't this redundant with the u >= nodes.size() done above?

Actually, it is not redundant. In my implementation, the global terminals (zeroIndex and oneIndex) are stored as the last two elements of the nodes vector, so they are valid indices and satisfy u < nodes.size().

AyaElAkhras · 2025-11-07T11:18:11Z

experimental/lib/Support/BooleanLogic/BDD.cpp

+  zeroIndex = n;
+  oneIndex = n + 1;
+  for (unsigned i = 0; i < n; ++i)
+    nodes[i] = BDDNode{order[i], zeroIndex, oneIndex, {}};


Worth mentioning that here you just create a new node for every entry in order and that you initialize the trueSucc and falseSucc with some dummy values that you later overwrite in expandFrom.

Why do you even initialize with zeroIndex and oneIndex? Why not with -1, for instance? This is also related to my earlier comment about what should be the value of trueSucc and falseSucc for leaf nodes. Why do not we use -1 for all these cases?

Agreed. Using zeroIndex/oneIndex as default values was indeed misleading as it implied a default connectivity that doesn't exist.

I have updated the initialization to use UINT_MAX (acting as -1 for unsigned) for both the temporary internal node values and the terminal successors. This explicitly marks them as 'uninitialized' or 'invalid' until they are properly set during expansion. I also added a comment clarifying that these internal node values are placeholders.

AyaElAkhras · 2025-12-05T21:49:00Z

experimental/lib/Support/FtdImplementation.cpp

+    // Wrap the two vertices in the pair into InputSpec objects.
+    InputSpec A = nodeToSpec(u), B = nodeToSpec(v);
+
+    // Direct edge -> successor becomes constant.


Are we guaranteed that u and v will always be directly connected?

Not necessarily. u and v might not be directly connected. I added a comment to clarify that this if-else block specifically handles the direct edge case. If there is no direct edge, this block is skipped.

AyaElAkhras · 2025-12-05T21:53:01Z

experimental/lib/Support/FtdImplementation.cpp

+          chosenP = predU[iu];
+        ++iu;
+        ++iv;
+      } else if (predU[iu] < predV[iv]) {


Check the coding style conventions since they omit braces from bodies made up of a single line.

Thanks for the comment. I double-checked the LLVM Coding Standards, which state that we must avoid 'Inconsistent bracing within if/else if/else chains (if one block requires braces, all must)'.

AyaElAkhras · 2025-12-05T22:33:23Z

experimental/lib/Support/FtdImplementation.cpp

+  std::vector<MuxSpec> muxChain;
+  muxChain.reserve(pairs.size());
+
+  for (auto [u, v] : pairs) {


I believe each element in pairs is a path-covering pair at a different point in the recursion, correct? In other words, pairs does not contain all alternative path-covering pairs for the global ROBDD; rather, it includes the path-covering pairs for the global ROBDD as well as those from other recursive regions.

If my understanding is correct, I would suggest adding a brief comment to clarify this.

You are absolutely correct. The pairs vector represents a topological sequence of path-covering pairs within the current subgraph. They are not alternatives but sequential stages used to build a cascaded MUX chain, where each MUX feeds the selection signal of the next.

I have added a comment to clarify that this loop constructs a sequential chain based on these sorted pairs.

QinYuan2000 added 2 commits October 7, 2025 02:41

Main

bd7b7fd

Merge remote-tracking branch 'upstream/main' into mux-tree

ec50f7e

QinYuan2000 marked this pull request as draft October 7, 2025 01:01

QinYuan2000 changed the title ~~[Experimental][FTD] Add Read-Once BDD builder and Single-Occurrence MUX Tree for Suppression~~ [Experimental][FTD] Introduce Single-Occurrence MUX Trees for Suppression Oct 7, 2025

QinYuan2000 added 3 commits October 8, 2025 01:11

Main Update

ea2ec1b

Main Update

2a21222

Main Update

24c9af2

QinYuan2000 marked this pull request as ready for review October 7, 2025 23:33

Merge remote-tracking branch 'upstream/main' into mux-tree

9bd5ea8

QinYuan2000 requested review from AyaElAkhras and pcineverdies October 7, 2025 23:40

QinYuan2000 added 5 commits October 8, 2025 01:52

Update

ae15fb3

Fix Bug

c9422bd

Merge remote-tracking branch 'upstream/main' into mux-tree

c58bf82

Add condition

f96fe31

Update

7119233

QinYuan2000 changed the title ~~[Experimental][FTD] Introduce Single-Occurrence MUX Trees for Suppression~~ [FTD] Introduce Single-Occurrence MUX Trees for Suppression Oct 22, 2025

Merge BDD files

75fb8f1

Update

14b047c

QinYuan2000 force-pushed the mux-tree branch from 24fc13d to 14b047c Compare November 4, 2025 22:33

AyaElAkhras requested changes Nov 5, 2025

View reviewed changes

AyaElAkhras requested changes Nov 7, 2025

View reviewed changes

AyaElAkhras requested changes Dec 5, 2025

View reviewed changes

QinYuan2000 added 2 commits December 7, 2025 21:39

change name to robdd

0bf710c

review changes

0ad744c

QinYuan2000 added 9 commits December 7, 2025 22:15

clang-format

5d32285

give meaningful names

e08ba8b

leaf nodes update

3f024ce

name polishment and remove brackets

0304305

initialization update

1956b9b

polishment

21be2de

polish naming and comment in buildmuxtree

cc37d95

update comment

32a73ee

small polishment

885ba25

[FTD] Introduce Single-Occurrence MUX Trees for Suppression #613

Are you sure you want to change the base?

[FTD] Introduce Single-Occurrence MUX Trees for Suppression #613

Uh oh!

Conversation

QinYuan2000 commented Oct 7, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Motivation

Implementation

Uh oh!

AyaElAkhras commented Oct 24, 2025

Uh oh!

QinYuan2000 commented Nov 4, 2025

Uh oh!

QinYuan2000 commented Nov 4, 2025

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

AyaElAkhras commented Nov 5, 2025

Uh oh!

AyaElAkhras commented Nov 5, 2025

Uh oh!

AyaElAkhras left a comment

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

QinYuan2000 commented Oct 7, 2025 •

edited

Loading