[Formal][PropertyAnnotation] Entry Token Order invariant

experimental/include/experimental/Support/FormalProperty.h

@@ -33,6 +33,7 @@ class FormalProperty {
     EagerForkNotAllOutputSent,
     CopiedSlotsOfActiveForksAreFull,
     ReconvergentPathFlow,
+    EntryTokenOrder,
   };
 
   TAG getTag() const { return tag; }
@@ -271,6 +272,31 @@ class ReconvergentPathFlow : public FormalProperty {
   inline static const StringLiteral EQUATIONS_LIT = "equations";
 };
 
+class EntryTokenOrder : public FormalProperty {
+public:
+  const std::vector<EffectiveSlotNamer> &getSlots() const { return slots; }
+  int32_t getValue() const { return entryValue; }
+  llvm::json::Value extraInfoToJSON() const override;
+  static std::unique_ptr<EntryTokenOrder>
+  fromJSON(const llvm::json::Value &value, llvm::json::Path path);
+  EntryTokenOrder() = default;
+  EntryTokenOrder(unsigned long id, TAG tag,
+                  std::vector<EffectiveSlotNamer> slots, int32_t value)
+      : FormalProperty(id, tag, TYPE::EntryTokenOrder), slots(std::move(slots)),
+        entryValue(value) {}
+  ~EntryTokenOrder() = default;
+
+  static bool classof(const FormalProperty *fp) {
+    return fp->getType() == TYPE::EntryTokenOrder;
+  }
+
+private:
+  std::vector<EffectiveSlotNamer> slots;
+  int32_t entryValue;
+  inline static const StringLiteral SLOTS_LIT = "slots";
+  inline static const StringLiteral ENTRY_VALUE_LIT = "entry_value";
+};
+
 class FormalPropertyTable {
 public:
   FormalPropertyTable() = default;

experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp

@@ -84,6 +84,9 @@ struct HandshakeAnnotatePropertiesPass
   LogicalResult annotateCopiedSlots(Operation &op);
   LogicalResult annotateCopiedSlotsOfAllForks(ModuleOp modOp);
   LogicalResult annotateReconvergentPathFlow(ModuleOp modOp);
+  LogicalResult annotateEntryTokenOrderPaths(ControlMergeOp cmerge,
+                                             int32_t entryValue);
+  LogicalResult annotateEntryTokenOrder(ModuleOp modOp);
 };
 
 bool isChannelToBeChecked(OpResult res) {
@@ -290,6 +293,109 @@ HandshakeAnnotatePropertiesPass::annotateReconvergentPathFlow(ModuleOp modOp) {
   return success();
 }
 
+namespace {
+std::vector<std::pair<ControlMergeOp, int32_t>>
+findEntryCMerge(mlir::Value start) {
+  std::vector<std::pair<ControlMergeOp, int32_t>> ret;
+  std::vector<mlir::Value> stack;
+  stack.push_back(start);
+  while (!stack.empty()) {
+    mlir::Value cur = stack.back();
+    stack.pop_back();
+
+    OpOperand &operand = *cur.getUses().begin();
+    Operation *next = operand.getOwner();
+    if (auto cmerge = dyn_cast<ControlMergeOp>(next)) {
+      int32_t entry;
+      for (auto [i, input] : llvm::enumerate(cmerge.getDataOperands())) {
+        if (input == cur) {
+          entry = i;
+        }
+      }
+      ret.emplace_back(cmerge, entry);
+    }
+    if (isa<BufferOp, ForkOp>(next)) {
+      for (mlir::Value channel : next->getResults()) {
+        stack.push_back(channel);
+      }
+    }
+  }
+  return ret;
+}
+} // namespace
+
+LogicalResult HandshakeAnnotatePropertiesPass::annotateEntryTokenOrderPaths(
+    ControlMergeOp cmerge, int32_t entryValue) {
+  struct PartialPath {
+    std::vector<EffectiveSlotNamer> slots;
+    mlir::Value cur;
+  };
+  std::vector<PartialPath> stack;
+  EffectiveSlotNamer mergeSlot(std::make_unique<BufferSlotFullNamer>(
+      cmerge.getInternalSlotStateNamers()[0]));
+  PartialPath start = {
+      .slots = {},
+      .cur = cmerge.getIndex(),
+  };
+  start.slots.push_back(mergeSlot);
+  stack.push_back(start);
+  while (!stack.empty()) {
+    PartialPath path = stack.back();
+    stack.pop_back();
+
+    Operation *next = path.cur.getUses().begin()->getOwner();
+    if (auto mux = dyn_cast<MuxOp>(next)) {
+      // Path is terminated by MuxOp, so this is the end of the path
+      if (path.slots.size() < 2) {
+        // This path does not contain enough slots to actually mean anything
+        continue;
+      }
+      EntryTokenOrder p(uid++, FormalProperty::TAG::INVAR, path.slots,
+                        entryValue);
+      propertyTable.push_back(p.toJSON());
+      continue;
+    }
+    if (auto buffer = dyn_cast<BufferOp>(next)) {
+      for (auto &slot : buffer.getInternalSlotStateNamers()) {
+        path.slots.emplace_back(std::make_unique<BufferSlotFullNamer>(slot));
+      }
+      path.cur = buffer.getResult();
+      stack.push_back(std::move(path));
+      continue;
+    }
+    if (auto fork = dyn_cast<ForkOp>(next)) {
+      auto sents = fork.getInternalSentStateNamers();
+      for (auto [i, channel] : llvm::enumerate(next->getResults())) {
+        PartialPath nextPath = {
+            .slots = path.slots,
+            .cur = channel,
+        };
+        EffectiveSlotNamer &back = nextPath.slots.back();
+        back.copiedSents.push_back(sents[i]);
+        stack.push_back(nextPath);
+      }
+      continue;
+    }
+
+    assert(false && "unexpected op detected!");
+    return failure();
+  }
+  return success();
+}
+
+LogicalResult
+HandshakeAnnotatePropertiesPass::annotateEntryTokenOrder(ModuleOp modOp) {
+  for (auto funcOp : modOp.getOps<handshake::FuncOp>()) {
+    for (BlockArgument arg : funcOp.getRegion().getArguments()) {
+      for (auto [cmerge, entryValue] : findEntryCMerge(arg)) {
+        if (failed(annotateEntryTokenOrderPaths(cmerge, entryValue))) {
+          return failure();
+        }
+      }
+    }
+  }
+  return success();
+}
 LogicalResult
 HandshakeAnnotatePropertiesPass::annotateProperty(ModuleOp modOp,
                                                   FormalProperty::TYPE t) {
@@ -304,6 +410,8 @@ HandshakeAnnotatePropertiesPass::annotateProperty(ModuleOp modOp,
     return annotateCopiedSlotsOfAllForks(modOp);
   case FormalProperty::TYPE::ReconvergentPathFlow:
     return annotateReconvergentPathFlow(modOp);
+  case FormalProperty::TYPE::EntryTokenOrder:
+    return annotateEntryTokenOrder(modOp);
   }
   return failure();
 }
@@ -336,6 +444,8 @@ LogicalResult HandshakeAnnotatePropertiesPass::annotateQueriedProperties() {
       return failure();
     if (failed(annotateReconvergentPathFlow(modOp)))
       return failure();
+    if (failed(annotateEntryTokenOrder(modOp)))
+      return failure();
   }
   return success();
 }

experimental/lib/Support/FormalProperty.cpp

@@ -33,6 +33,8 @@ FormalProperty::typeFromStr(const std::string &s) {
     return FormalProperty::TYPE::CopiedSlotsOfActiveForksAreFull;
   if (s == "ReconvergentPathFlow")
     return FormalProperty::TYPE::ReconvergentPathFlow;
+  if (s == "EntryTokenOrder")
+    return FormalProperty::TYPE::EntryTokenOrder;
 
   return std::nullopt;
 }
@@ -49,6 +51,8 @@ std::string FormalProperty::typeToStr(TYPE t) {
     return "CopiedSlotsOfActiveForksAreFull";
   case TYPE::ReconvergentPathFlow:
     return "ReconvergentPathFlow";
+  case TYPE::EntryTokenOrder:
+    return "EntryTokenOrder";
   }
 }
 
@@ -108,6 +112,8 @@ FormalProperty::fromJSON(const llvm::json::Value &value,
                                                     path.field(INFO_LIT));
   case TYPE::ReconvergentPathFlow:
     return ReconvergentPathFlow::fromJSON(value, path.field(INFO_LIT));
+  case TYPE::EntryTokenOrder:
+    return EntryTokenOrder::fromJSON(value, path.field(INFO_LIT));
   }
 }
 
@@ -362,6 +368,25 @@ ReconvergentPathFlow::fromJSON(const llvm::json::Value &value,
   return prop;
 }
 
+llvm::json::Value EntryTokenOrder::extraInfoToJSON() const {
+  return llvm::json::Object(
+      {{SLOTS_LIT, slots}, {ENTRY_VALUE_LIT, entryValue}});
+}
+
+std::unique_ptr<EntryTokenOrder>
+EntryTokenOrder::fromJSON(const llvm::json::Value &value,
+                          llvm::json::Path path) {
+  auto prop = std::make_unique<EntryTokenOrder>();
+
+  llvm::json::Value info = prop->parseBaseAndExtractInfo(value, path);
+  llvm::json::ObjectMapper mapper(info, path);
+
+  if (!mapper || !mapper.map(SLOTS_LIT, prop->slots) ||
+      !mapper.map(ENTRY_VALUE_LIT, prop->entryValue))
+    return nullptr;
+  return prop;
+}
+
 LogicalResult FormalPropertyTable::addPropertiesFromJSON(StringRef filepath) {
   // Open the properties' database
   std::ifstream inputFile(filepath.str());

include/dynamatic/Dialect/Handshake/HandshakeOpInternalStateNamer.h

@@ -16,6 +16,8 @@ struct ConstrainedNamer;
 struct ConstrainedEagerForkSentNamer;
 struct ConstrainedBufferSlotFullNamer;
 struct MemoryControllerSlotNamer;
+struct EffectiveSlotNamer;
+struct ConstrainedEffectiveSlotNamer;
 
 // A general structure for an operation is assumed:
 // in1, in2, ... -> Join/Merge/Mux
@@ -32,6 +34,7 @@ struct InternalStateNamer {
     PipelineSlot,
     Constrained,
     MemoryControllerSlot,
+    EffectiveSlot,
   };
   static std::optional<TYPE> typeFromStr(const std::string &s);
   static std::string typeToStr(TYPE t);
@@ -46,14 +49,17 @@ struct InternalStateNamer {
   friend bool fromJSON(const llvm::json::Value &value,
                        std::unique_ptr<InternalStateNamer> &namer,
                        llvm::json::Path path);
+  friend bool fromJSON(const llvm::json::Value &value,
+                       std::shared_ptr<InternalStateNamer> &namer,
+                       llvm::json::Path path);
 
   InternalStateNamer() = default;
   InternalStateNamer(TYPE type) : type(type) {}
   virtual ~InternalStateNamer() = default;
 
   static inline bool classof(const InternalStateNamer *fp) { return true; }
 
-  std::unique_ptr<ConstrainedNamer> tryConstrain(int32_t value);
+  std::unique_ptr<ConstrainedNamer> tryConstrain(int32_t value) const;
 
   TYPE type;
   static constexpr llvm::StringLiteral TYPE_LIT = "type";
@@ -63,6 +69,7 @@ struct InternalStateNamer {
   static constexpr llvm::StringLiteral CONSTRAINED = "Constrained";
   static constexpr llvm::StringLiteral MEMORY_CONTROLLER_SLOT =
       "MemoryControllerSlot";
+  static constexpr llvm::StringLiteral EFFECTIVE_SLOT = "EffectiveSlot";
   static constexpr llvm::StringLiteral INNER_LIT = "inner";
 };
 
@@ -138,7 +145,7 @@ struct EagerForkSentNamer : InternalStateNamer {
   std::string channelName;
   size_t channelSize;
 
-  ConstrainedEagerForkSentNamer constrain(int32_t value);
+  ConstrainedEagerForkSentNamer constrain(int32_t value) const;
 
   static constexpr llvm::StringLiteral OPERATION_LIT = "operation";
   static constexpr llvm::StringLiteral CHANNEL_NAME_LIT = "channel_name";
@@ -195,7 +202,7 @@ struct BufferSlotFullNamer : InternalStateNamer {
     return fp->type == TYPE::BufferSlotFull;
   }
 
-  ConstrainedBufferSlotFullNamer constrain(int32_t value);
+  ConstrainedBufferSlotFullNamer constrain(int32_t value) const;
 
   inline std::string getSMVName() const override {
     return llvm::formatv("{0}.{1}", opName, slotName).str();
@@ -328,6 +335,50 @@ struct MemoryControllerSlotNamer : InternalStateNamer {
   static constexpr llvm::StringLiteral LOADLESS_LIT = "loadless";
 };
 
+// EffectiveSlotNamer generates the SMV that is TRUE if and only if the
+// targetted slot 1. contains data and 2. is not duplicated by an eager fork.
+struct EffectiveSlotNamer : InternalStateNamer {
+  EffectiveSlotNamer() = default;
+  EffectiveSlotNamer(std::unique_ptr<InternalStateNamer> slot)
+      : InternalStateNamer(TYPE::EffectiveSlot), slot(std::move(slot)),
+        copiedSents(std::vector<EagerForkSentNamer>()) {}
+  ~EffectiveSlotNamer() = default;
+  static inline bool classof(const InternalStateNamer *fp) {
+    return fp->type == TYPE::EffectiveSlot;
+  }
+
+  inline void addCopiedSent(EagerForkSentNamer sent) {
+    copiedSents.push_back(std::move(sent));
+  }
+
+  std::unique_ptr<ConstrainedNamer> constrain(int32_t value) const;
+
+  std::string getSMVName() const override;
+  llvm::json::Value toInnerJSON() const override;
+  friend bool fromJSON(const llvm::json::Value &value,
+                       EffectiveSlotNamer &namer, llvm::json::Path path);
+
+  std::shared_ptr<InternalStateNamer> slot;
+  std::vector<EagerForkSentNamer> copiedSents;
+  static constexpr llvm::StringLiteral SLOT_LIT = "slot";
+  static constexpr llvm::StringLiteral COPIED_SENTS_LIT = "copied_sents";
+};
+
+struct ConstrainedEffectiveSlotNamer : ConstrainedNamer {
+  ConstrainedEffectiveSlotNamer() = default;
+  ConstrainedEffectiveSlotNamer(EffectiveSlotNamer namer, int32_t value)
+      : ConstrainedNamer(TYPE::EffectiveSlot, value) {
+    namer.slot = namer.slot->tryConstrain(value);
+    inner = namer;
+  }
+  ~ConstrainedEffectiveSlotNamer() = default;
+  inline std::unique_ptr<InternalStateNamer> getUnconstrained() const override {
+    return std::make_unique<EffectiveSlotNamer>(inner);
+  }
+  inline std::string getSMVName() const override { return inner.getSMVName(); }
+  EffectiveSlotNamer inner;
+};
+
 // Specialize llvm::json toJSON template for each namer so that they can be
 // converted to json automatically by llvm where necessary
 inline llvm::json::Value toJSON(const EagerForkSentNamer &namer) {
@@ -345,6 +396,9 @@ inline llvm::json::Value toJSON(const MemoryControllerSlotNamer &namer) {
 inline llvm::json::Value toJSON(const ConstrainedNamer &namer) {
   return namer.toInnerJSON();
 }
+inline llvm::json::Value toJSON(const EffectiveSlotNamer &namer) {
+  return namer.toInnerJSON();
+}
 
 } // namespace handshake
 } // namespace dynamatic