[Formal][PropertyAnnotation] Annotating IOG-based invariants

experimental/include/experimental/Support/CreateSmvFormalTestbench.h

@@ -48,6 +48,12 @@ struct SmvTestbenchConfig {
   // Determines if the outputs are synchronized with a join or if they are
   // consumed by sinks
   bool syncOutput = false;
+
+  // 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;
 };
 
 // Create a wrapper for the provided SMV file.
@@ -157,4 +163,4 @@ MODULE sink(ins_valid)
   DEFINE ins_ready := TRUE;)DELIM";
 
 } // namespace dynamatic::experimental
-#endif // DYNAMATIC_EXPERIMENTAL_ELASTIC_MITER_CREATE_FORMAL_TESTBENCH_H
+#endif // DYNAMATIC_EXPERIMENTAL_ELASTIC_MITER_CREATE_FORMAL_TESTBENCH_H

experimental/include/experimental/Support/FormalProperty.h

@@ -33,6 +33,8 @@ class FormalProperty {
     EagerForkNotAllOutputSent,
     CopiedSlotsOfActiveForksAreFull,
     ReconvergentPathFlow,
+    IOGSingleToken,
+    IOGConsecutiveTokens,
   };
 
   TAG getTag() const { return tag; }
@@ -271,6 +273,70 @@ 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;
+  static std::unique_ptr<IOGSingleToken>
+  fromJSON(const llvm::json::Value &value, llvm::json::Path path);
+
+  IOGSingleToken() = default;
+  IOGSingleToken(unsigned long id, TAG tag,
+                 std::vector<std::unique_ptr<InternalStateNamer>> slots,
+                 std::vector<EagerForkSentNamer> 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<std::unique_ptr<InternalStateNamer>> slots;
+  std::vector<EagerForkSentNamer> forks;
+
+private:
+  inline static const StringLiteral SLOTS_LIT = "slots";
+  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;
+  static std::unique_ptr<IOGConsecutiveTokens>
+  fromJSON(const llvm::json::Value &value, llvm::json::Path path);
+
+  IOGConsecutiveTokens() = default;
+  IOGConsecutiveTokens(unsigned long id, TAG tag, const TokenCountNamer &slot1,
+                       const TokenCountNamer &slot2,
+                       std::vector<EagerForkSentNamer> sents);
+  ~IOGConsecutiveTokens() = default;
+
+  static bool classof(const FormalProperty *fp) {
+    return fp->getType() == TYPE::IOGConsecutiveTokens;
+  }
+
+  TokenCountNamer slot1;
+  TokenCountNamer slot2;
+  std::vector<EagerForkSentNamer> 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;

experimental/include/experimental/Support/IOG.h

@@ -0,0 +1,81 @@
+#pragma once
+
+#include "dynamatic/Analysis/NameAnalysis.h"
+#include "dynamatic/Support/LLVM.h"
+#include "mlir/IR/Value.h"
+#include <unordered_set>
+
+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(Operation *start, Operation *end) : start(start), end(end) {}
+
+  std::unordered_set<Operation *> units;
+  Operation *start;
+  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<Operation *> units;
+  llvm::DenseSet<mlir::Value> 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();
+  }
+
+  inline bool contains(mlir::Value channel) const {
+    auto iter = channels.find(channel);
+    return iter != channels.end();
+  }
+
+  void debug() const {
+    std::vector<mlir::Value> stack;
+    llvm::DenseSet<mlir::Value> 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<IOG> findAllIOGs(ModuleOp modOp);
+
+} // namespace dynamatic