[Formal][PropertyAnnotation] Annotating IOG-based invariants

data/rtl-config-smv.json

@@ -89,7 +89,7 @@
   },
   {
     "name": "handshake.sink",
-    "generator": "python $DYNAMATIC/experimental/tools/unit-generators/smv/smv-unit-generator.py -n $MODULE_NAME -o $OUTPUT_DIR/$MODULE_NAME.smv -t sink -p bitwidth=$BITWIDTH",
+    "generator": "python $DYNAMATIC/experimental/tools/unit-generators/smv/smv-unit-generator.py -n $MODULE_NAME -o $OUTPUT_DIR/$MODULE_NAME.smv -t sink -p bitwidth=$BITWIDTH iog_terminator=$IOG_TERMINATOR",
     "hdl": "smv"
   },
   {
@@ -298,4 +298,4 @@
     "generator": "python $DYNAMATIC/experimental/tools/unit-generators/smv/smv-unit-generator.py -n $MODULE_NAME -o $OUTPUT_DIR/$MODULE_NAME.smv -t lsq -p data_bitwidth=$DATA_BITWIDTH addr_bitwidth=$ADDR_BITWIDTH config_file=\"'$OUTPUT_DIR/$MODULE_NAME.json'\"",
     "hdl": "smv"
   }
-]
+]

experimental/include/experimental/Support/CreateSmvFormalTestbench.h

@@ -48,6 +48,10 @@ struct SmvTestbenchConfig {
   // Determines if the outputs are synchronized with a join or if they are
   // consumed by sinks
   bool syncOutput = false;
+
+  // Determines if the output is modelled as a dead buffer (i.e. accepts one
+  // token, then the output is no longer ready
+  bool deadBufferOutput = false;
 };
 
 // Create a wrapper for the provided SMV file.
@@ -157,4 +161,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,59 @@ class ReconvergentPathFlow : public FormalProperty {
   inline static const StringLiteral EQUATIONS_LIT = "equations";
 };
 
+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";
+};
+
+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,
+                       std::shared_ptr<InternalStateNamer> slot1,
+                       std::shared_ptr<InternalStateNamer> slot2,
+                       std::vector<EagerForkSentNamer> sents);
+  ~IOGConsecutiveTokens() = default;
+
+  static bool classof(const FormalProperty *fp) {
+    return fp->getType() == TYPE::IOGConsecutiveTokens;
+  }
+
+  std::shared_ptr<InternalStateNamer> slot1;
+  std::shared_ptr<InternalStateNamer> 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,77 @@
+#pragma once
+
+#include "dynamatic/Analysis/NameAnalysis.h"
+#include "dynamatic/Support/LLVM.h"
+#include "mlir/IR/Value.h"
+#include <unordered_set>
+
+// 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.
+
+namespace dynamatic {
+struct IOG;
+struct IOGPathSet;
+
+struct IOGPathSet {
+  IOGPathSet(const IOG &iog, Operation *start, Operation *end);
+
+  std::unordered_set<Operation *> units;
+  Operation *start;
+  Operation *end;
+};
+
+struct IOG {
+  IOG() = default;
+  std::unordered_set<Operation *> units;
+  llvm::DenseSet<mlir::Value> channels;
+  BlockArgument entry;
+
+  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

experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp

@@ -26,6 +26,7 @@
 #include "dynamatic/Support/TimingModels.h"
 #include "dynamatic/Transforms/BufferPlacement/CFDFC.h"
 #include "experimental/Support/FormalProperty.h"
+#include "experimental/Support/IOG.h"
 #include "mlir/IR/Value.h"
 #include "mlir/Pass/Pass.h"
 #include "mlir/Pass/PassManager.h"
@@ -57,7 +58,6 @@ namespace experimental {
 // [END Boilerplate code for the MLIR pass]
 
 namespace {
-
 struct HandshakeAnnotatePropertiesPass
     : public dynamatic::experimental::impl::HandshakeAnnotatePropertiesBase<
           HandshakeAnnotatePropertiesPass> {
@@ -71,7 +71,7 @@ struct HandshakeAnnotatePropertiesPass
   json::Array propertyTable;
 
   LogicalResult annotateProperty(ModuleOp modOp, FormalProperty::TYPE t);
-  LogicalResult annotateQueriedProperties();
+  LogicalResult annotateQueriedProperties(const std::vector<IOG> &iogs);
   LogicalResult annotateAbsenceOfBackpressure(ModuleOp modOp);
   LogicalResult annotateValidEquivalence(ModuleOp modOp);
   LogicalResult annotateValidEquivalenceBetweenOps(Operation &op1,
@@ -84,6 +84,8 @@ struct HandshakeAnnotatePropertiesPass
   LogicalResult annotateCopiedSlots(Operation &op);
   LogicalResult annotateCopiedSlotsOfAllForks(ModuleOp modOp);
   LogicalResult annotateReconvergentPathFlow(ModuleOp modOp);
+  LogicalResult annotateIOGSingleToken(const IOG &iog);
+  LogicalResult annotateIOGConsecutiveTokens(const IOG &iog);
 };
 
 bool isChannelToBeChecked(OpResult res) {
@@ -290,6 +292,120 @@ HandshakeAnnotatePropertiesPass::annotateReconvergentPathFlow(ModuleOp modOp) {
   return success();
 }
 
+namespace {
+std::vector<EagerForkSentNamer> findCopiedSents(const IOG &iog,
+                                                const IOGPathSet &pathSet) {
+  std::vector<EagerForkSentNamer> sents;
+  std::vector<Operation *> stack;
+  stack.push_back(pathSet.start);
+  bool first = true;
+  while (!stack.empty()) {
+    Operation *cur = stack.back();
+    stack.pop_back();
+    if (!first) {
+      auto slots = getAllSlotsOfOperation(cur);
+      if (!slots.empty()) {
+        return sents;
+      }
+    }
+    first = false;
+    for (OpResult forward : cur->getResults()) {
+      if (!iog.contains(forward)) {
+        continue;
+      }
+      Operation *next = forward.getUses().begin()->getOwner();
+      assert(iog.contains(next));
+      if (pathSet.units.find(next) == pathSet.units.end()) {
+        continue;
+      }
+
+      if (auto forkOp = dyn_cast<EagerForkLikeOpInterface>(cur)) {
+        sents.push_back(
+            forkOp.getInternalSentStateNamers()[forward.getResultNumber()]);
+      }
+
+      stack.push_back(next);
+    }
+  }
+  return sents;
+}
+} // namespace
+
+LogicalResult
+HandshakeAnnotatePropertiesPass::annotateIOGSingleToken(const IOG &iog) {
+  std::vector<std::unique_ptr<InternalStateNamer>> slots(0);
+  Operation *op = iog.entry.getOwner()->getParentOp();
+  auto nameAttr =
+      op->getAttrOfType<ArrayAttr>("argNames")[iog.entry.getArgNumber()];
+  std::string name = dyn_cast<StringAttr>(nameAttr).str();
+
+  slots.push_back(std::make_unique<EntrySlotNamer>(name));
+  std::vector<EagerForkSentNamer> forks(0);
+  for (auto &op : iog.units) {
+    for (auto &slot : getAllSlotsOfOperation(op)) {
+      slots.push_back(std::move(slot));
+    }
+    if (auto forkOp = dyn_cast<EagerForkLikeOpInterface>(op)) {
+      auto forkSlots = forkOp.getInternalSentStateNamers();
+      int count = 0;
+      for (auto [i, channel] : llvm::enumerate(forkOp->getResults())) {
+        if (iog.contains(channel)) {
+          forks.push_back(forkSlots[i]);
+          count += 1;
+        }
+      }
+      assert(count == 1);
+    }
+  }
+  auto p = IOGSingleToken(uid, FormalProperty::TAG::INVAR, std::move(slots),
+                          std::move(forks));
+  uid++;
+  propertyTable.push_back(p.toJSON());
+  return success();
+}
+
+LogicalResult
+HandshakeAnnotatePropertiesPass::annotateIOGConsecutiveTokens(const IOG &iog) {
+  std::vector<std::pair<Operation *, std::shared_ptr<InternalStateNamer>>>
+      slotOps;
+  for (auto &op : iog.units) {
+    auto slotCountNamer = getTokenCountNamerOfOperation(op);
+    if (slotCountNamer.has_value()) {
+      assert(*slotCountNamer);
+      slotOps.push_back({op, std::move(*slotCountNamer)});
+    }
+  }
+  for (auto slot1 = slotOps.begin(); slot1 != slotOps.end(); ++slot1) {
+    for (auto slot2 = slot1 + 1; slot2 != slotOps.end(); ++slot2) {
+      if (slot1 == slot2) {
+        // TODO: Handle loops, i.e. if the slot contains >=2 tokens, there
+        // should be a copied fork within a loop
+        continue;
+      }
+
+      IOGPathSet pathSet12(iog, slot1->first, slot2->first);
+
+      std::vector<EagerForkSentNamer> copiedSents =
+          findCopiedSents(iog, pathSet12);
+
+      IOGPathSet pathSet21(iog, slot2->first, slot1->first);
+      std::vector<EagerForkSentNamer> extra = findCopiedSents(iog, pathSet21);
+      copiedSents.insert(copiedSents.end(), extra.begin(), extra.end());
+
+      // Note:
+      // Even if the copiedSents is empty, this invariant is interesting! It
+      // means that both slots cannot be occupied at the same time, as there is
+      // only (at most) one token in the IOG
+
+      auto p = IOGConsecutiveTokens(uid, FormalProperty::TAG::INVAR,
+                                    slot1->second, slot2->second, copiedSents);
+      uid++;
+      propertyTable.push_back(p.toJSON());
+    }
+  }
+  return success();
+}
+
 LogicalResult
 HandshakeAnnotatePropertiesPass::annotateProperty(ModuleOp modOp,
                                                   FormalProperty::TYPE t) {
@@ -304,10 +420,17 @@ HandshakeAnnotatePropertiesPass::annotateProperty(ModuleOp modOp,
     return annotateCopiedSlotsOfAllForks(modOp);
   case FormalProperty::TYPE::ReconvergentPathFlow:
     return annotateReconvergentPathFlow(modOp);
+  case FormalProperty::TYPE::IOGSingleToken:
+  case FormalProperty::TYPE::IOGConsecutiveTokens:
+    assert(false &&
+           "TODO: IOG as pass so that this function has access to IOGs");
+    return failure();
   }
   return failure();
 }
-LogicalResult HandshakeAnnotatePropertiesPass::annotateQueriedProperties() {
+
+LogicalResult HandshakeAnnotatePropertiesPass::annotateQueriedProperties(
+    const std::vector<IOG> &iogs) {
   ModuleOp modOp = getOperation();
   LogicalResult res = success();
   if (annotateList != "") {
@@ -336,12 +459,35 @@ LogicalResult HandshakeAnnotatePropertiesPass::annotateQueriedProperties() {
       return failure();
     if (failed(annotateReconvergentPathFlow(modOp)))
       return failure();
+
+    for (const auto &iog : iogs) {
+      if (failed(annotateIOGSingleToken(iog)))
+        return failure();
+      if (failed(annotateIOGConsecutiveTokens(iog)))
+        return failure();
+    }
   }
   return success();
 }
 
 void HandshakeAnnotatePropertiesPass::runDynamaticPass() {
-  if (failed(annotateQueriedProperties())) {
+  ModuleOp modOp = getOperation();
+  auto iogs = findAllIOGs(modOp);
+  llvm::DenseSet<SinkOp> sinks;
+  for (auto &iog : iogs) {
+    for (Operation *unit : iog.units) {
+      if (auto sinkOp = dyn_cast<SinkOp>(unit)) {
+        sinks.insert(sinkOp);
+      }
+    }
+  }
+
+  for (SinkOp sink : sinks) {
+    auto unitAttr = UnitAttr::get(modOp.getContext());
+    sink->setAttr("IOG_TERMINATOR", unitAttr);
+  }
+
+  if (failed(annotateQueriedProperties(iogs))) {
     return signalPassFailure();
   }
 

experimental/lib/Support/CMakeLists.txt

@@ -10,6 +10,7 @@ add_dynamatic_library(DynamaticExperimentalSupport
   CFGAnnotation.cpp
   FormalProperty.cpp
   FlowExpression.cpp
+  IOG.cpp
 
   LINK_LIBS PUBLIC
   MLIRIR