diff --git a/experimental/include/experimental/Support/FormalProperty.h b/experimental/include/experimental/Support/FormalProperty.h
index 1bb12a62e..2ab202eb1 100644
--- a/experimental/include/experimental/Support/FormalProperty.h
+++ b/experimental/include/experimental/Support/FormalProperty.h
@@ -33,6 +33,8 @@ class FormalProperty {
     EagerForkNotAllOutputSent,
     CopiedSlotsOfActiveForksAreFull,
     ReconvergentPathFlow,
+    EntryTokenOrder,
+    SingleEntryToken,
   };
 
   TAG getTag() const { return tag; }
@@ -271,6 +273,58 @@ 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 SingleEntryToken : public FormalProperty {
+public:
+  const std::vector<EffectiveSlotNamer> &getEcPath() const { return ec; }
+  const std::vector<EffectiveSlotNamer> &getCmPath() const { return cm; }
+
+  llvm::json::Value extraInfoToJSON() const override;
+  static std::unique_ptr<SingleEntryToken>
+  fromJSON(const llvm::json::Value &value, llvm::json::Path path);
+  SingleEntryToken() = default;
+  SingleEntryToken(unsigned long id, TAG tag,
+                   std::vector<EffectiveSlotNamer> ec,
+                   std::vector<EffectiveSlotNamer> cm)
+      : FormalProperty(id, tag, TYPE::SingleEntryToken), ec(std::move(ec)),
+        cm(std::move(cm)) {}
+  ~SingleEntryToken() = default;
+
+  static bool classof(const FormalProperty *fp) {
+    return fp->getType() == TYPE::SingleEntryToken;
+  }
+
+private:
+  std::vector<EffectiveSlotNamer> ec;
+  std::vector<EffectiveSlotNamer> cm;
+  inline static const StringLiteral PATH_EC_LIT = "entry_cmerge_path";
+  inline static const StringLiteral PATH_CM_LIT = "cmerge_mux_path";
+};
+
 class FormalPropertyTable {
 public:
   FormalPropertyTable() = default;
diff --git a/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp b/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp
index d504db9d9..955e73d00 100644
--- a/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp
+++ b/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp
@@ -84,6 +84,10 @@ 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);
+  LogicalResult annotateSingleEntryToken(ModuleOp modOp);
 };
 
 bool isChannelToBeChecked(OpResult res) {
@@ -290,6 +294,174 @@ HandshakeAnnotatePropertiesPass::annotateReconvergentPathFlow(ModuleOp modOp) {
   return success();
 }
 
+namespace {
+struct EntryCMergePath {
+  std::vector<EffectiveSlotNamer> slots;
+  ControlMergeOp cmerge;
+  int32_t entryValue;
+};
+std::vector<EntryCMergePath> findEntryCMergePaths(BlockArgument startChannel) {
+  struct PartialPath {
+    std::vector<EffectiveSlotNamer> slots;
+    mlir::Value cur;
+  };
+  std::vector<EntryCMergePath> ret;
+  std::vector<PartialPath> stack;
+  PartialPath start = {
+      .slots = {},
+      .cur = startChannel,
+  };
+  // TODO: Make this an entry slot (which is in a different PR)
+  Operation *op = startChannel.getOwner()->getParentOp();
+  auto nameAttr =
+      op->getAttrOfType<ArrayAttr>("argNames")[startChannel.getArgNumber()];
+  std::string name = dyn_cast<StringAttr>(nameAttr).str();
+  llvm::errs() << name << "\n";
+  start.slots.emplace_back(
+      std::make_unique<BufferSlotFullNamer>(name, "valid", "", 0));
+  stack.push_back(start);
+  while (!stack.empty()) {
+    PartialPath path = std::move(stack.back());
+    stack.pop_back();
+
+    Operation *next = path.cur.getUses().begin()->getOwner();
+    if (auto cmerge = dyn_cast<ControlMergeOp>(next)) {
+      int32_t entry;
+      for (auto [i, input] : llvm::enumerate(cmerge.getDataOperands())) {
+        if (input == path.cur) {
+          entry = i;
+        }
+      }
+      EntryCMergePath retPath = {
+          .slots = path.slots,
+          .cmerge = cmerge,
+          .entryValue = entry,
+      };
+      ret.push_back(retPath);
+    }
+    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,
+        };
+        assert(!nextPath.slots.empty());
+        EffectiveSlotNamer &back = nextPath.slots.back();
+        back.copiedSents.push_back(sents[i]);
+        stack.push_back(nextPath);
+      }
+      continue;
+    }
+  }
+  return ret;
+}
+
+std::vector<std::vector<EffectiveSlotNamer>>
+findCMergeMuxPaths(ControlMergeOp cmerge) {
+  struct PartialPath {
+    std::vector<EffectiveSlotNamer> slots;
+    mlir::Value cur;
+  };
+  std::vector<std::vector<EffectiveSlotNamer>> ret{};
+  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
+      ret.push_back(std::move(path.slots));
+      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;
+    }
+
+    llvm::report_fatal_error("unexpected op detected");
+  }
+  return ret;
+}
+} // namespace
+
+LogicalResult HandshakeAnnotatePropertiesPass::annotateEntryTokenOrderPaths(
+    ControlMergeOp cmerge, int32_t entryValue) {
+  for (const auto &path : findCMergeMuxPaths(cmerge)) {
+    if (path.size() < 2) {
+      // The regex of this invariant trivially holds for any path of length 1
+      continue;
+    }
+    EntryTokenOrder p(uid++, FormalProperty::TAG::INVAR, path, entryValue);
+    propertyTable.push_back(p.toJSON());
+  }
+  return success();
+}
+
+LogicalResult
+HandshakeAnnotatePropertiesPass::annotateEntryTokenOrder(ModuleOp modOp) {
+  for (auto funcOp : modOp.getOps<handshake::FuncOp>()) {
+    for (BlockArgument arg : funcOp.getRegion().getArguments()) {
+      for (const auto &path : findEntryCMergePaths(arg)) {
+        if (failed(
+                annotateEntryTokenOrderPaths(path.cmerge, path.entryValue))) {
+          return failure();
+        }
+      }
+    }
+  }
+  return success();
+}
+
+LogicalResult
+HandshakeAnnotatePropertiesPass::annotateSingleEntryToken(ModuleOp modOp) {
+  for (auto funcOp : modOp.getOps<handshake::FuncOp>()) {
+    for (BlockArgument arg : funcOp.getRegion().getArguments()) {
+      for (const auto &ec : findEntryCMergePaths(arg)) {
+        for (const auto &cm : findCMergeMuxPaths(ec.cmerge)) {
+          SingleEntryToken p(uid++, FormalProperty::TAG::INVAR, ec.slots, cm);
+          propertyTable.push_back(p.toJSON());
+        }
+      }
+    }
+  }
+  return success();
+}
+
 LogicalResult
 HandshakeAnnotatePropertiesPass::annotateProperty(ModuleOp modOp,
                                                   FormalProperty::TYPE t) {
@@ -304,6 +476,10 @@ HandshakeAnnotatePropertiesPass::annotateProperty(ModuleOp modOp,
     return annotateCopiedSlotsOfAllForks(modOp);
   case FormalProperty::TYPE::ReconvergentPathFlow:
     return annotateReconvergentPathFlow(modOp);
+  case FormalProperty::TYPE::EntryTokenOrder:
+    return annotateEntryTokenOrder(modOp);
+  case FormalProperty::TYPE::SingleEntryToken:
+    return annotateSingleEntryToken(modOp);
   }
   return failure();
 }
@@ -336,6 +512,10 @@ LogicalResult HandshakeAnnotatePropertiesPass::annotateQueriedProperties() {
       return failure();
     if (failed(annotateReconvergentPathFlow(modOp)))
       return failure();
+    if (failed(annotateEntryTokenOrder(modOp)))
+      return failure();
+    if (failed(annotateSingleEntryToken(modOp)))
+      return failure();
   }
   return success();
 }
diff --git a/experimental/lib/Support/FormalProperty.cpp b/experimental/lib/Support/FormalProperty.cpp
index 99d33f3c5..d487b1169 100644
--- a/experimental/lib/Support/FormalProperty.cpp
+++ b/experimental/lib/Support/FormalProperty.cpp
@@ -33,6 +33,10 @@ FormalProperty::typeFromStr(const std::string &s) {
     return FormalProperty::TYPE::CopiedSlotsOfActiveForksAreFull;
   if (s == "ReconvergentPathFlow")
     return FormalProperty::TYPE::ReconvergentPathFlow;
+  if (s == "EntryTokenOrder")
+    return FormalProperty::TYPE::EntryTokenOrder;
+  if (s == "SingleEntryToken")
+    return FormalProperty::TYPE::SingleEntryToken;
 
   return std::nullopt;
 }
@@ -49,6 +53,10 @@ std::string FormalProperty::typeToStr(TYPE t) {
     return "CopiedSlotsOfActiveForksAreFull";
   case TYPE::ReconvergentPathFlow:
     return "ReconvergentPathFlow";
+  case TYPE::EntryTokenOrder:
+    return "EntryTokenOrder";
+  case TYPE::SingleEntryToken:
+    return "SingleEntryToken";
   }
 }
 
@@ -108,6 +116,10 @@ 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));
+  case TYPE::SingleEntryToken:
+    return SingleEntryToken::fromJSON(value, path.field(INFO_LIT));
   }
 }
 
@@ -362,6 +374,43 @@ 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;
+}
+
+llvm::json::Value SingleEntryToken::extraInfoToJSON() const {
+  return llvm::json::Object({{PATH_CM_LIT, cm}, {PATH_EC_LIT, ec}});
+}
+
+std::unique_ptr<SingleEntryToken>
+SingleEntryToken::fromJSON(const llvm::json::Value &value,
+                           llvm::json::Path path) {
+  auto prop = std::make_unique<SingleEntryToken>();
+
+  llvm::json::Value info = prop->parseBaseAndExtractInfo(value, path);
+  llvm::json::ObjectMapper mapper(info, path);
+
+  if (!mapper || !mapper.map(PATH_CM_LIT, prop->cm) ||
+      !mapper.map(PATH_EC_LIT, prop->ec))
+    return nullptr;
+  return prop;
+}
+
 LogicalResult FormalPropertyTable::addPropertiesFromJSON(StringRef filepath) {
   // Open the properties' database
   std::ifstream inputFile(filepath.str());
diff --git a/include/dynamatic/Dialect/Handshake/HandshakeOpInternalStateNamer.h b/include/dynamatic/Dialect/Handshake/HandshakeOpInternalStateNamer.h
index dd6046df1..0d295540c 100644
--- a/include/dynamatic/Dialect/Handshake/HandshakeOpInternalStateNamer.h
+++ b/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,6 +49,9 @@ 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) {}
@@ -53,7 +59,7 @@ struct InternalStateNamer {
 
   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
diff --git a/lib/Dialect/Handshake/HandshakeOpInternalStateNamer.cpp b/lib/Dialect/Handshake/HandshakeOpInternalStateNamer.cpp
index bd0e34c4f..4f72b9cfa 100644
--- a/lib/Dialect/Handshake/HandshakeOpInternalStateNamer.cpp
+++ b/lib/Dialect/Handshake/HandshakeOpInternalStateNamer.cpp
@@ -1,4 +1,5 @@
 #include "dynamatic/Dialect/Handshake/HandshakeOpInternalStateNamer.h"
+#include "llvm/ADT/StringExtras.h"
 #include "llvm/Support/Casting.h"
 
 namespace dynamatic {
@@ -15,6 +16,8 @@ InternalStateNamer::typeFromStr(const std::string &s) {
     return TYPE::Constrained;
   if (s == MEMORY_CONTROLLER_SLOT)
     return TYPE::MemoryControllerSlot;
+  if (s == EFFECTIVE_SLOT)
+    return TYPE::EffectiveSlot;
   return std::nullopt;
 }
 
@@ -30,6 +33,8 @@ std::string InternalStateNamer::typeToStr(TYPE t) {
     return CONSTRAINED.str();
   case TYPE::MemoryControllerSlot:
     return MEMORY_CONTROLLER_SLOT.str();
+  case TYPE::EffectiveSlot:
+    return EFFECTIVE_SLOT.str();
   }
 }
 
@@ -75,6 +80,7 @@ bool fromJSON(const llvm::json::Value &value,
   BufferSlotFullNamer bs;
   PipelineSlotNamer ps;
   MemoryControllerSlotNamer mc;
+  EffectiveSlotNamer es;
   switch (type) {
   case InternalStateNamer::TYPE::EagerForkSent:
     ef = EagerForkSentNamer();
@@ -103,13 +109,29 @@ bool fromJSON(const llvm::json::Value &value,
       return false;
     namer = std::make_unique<MemoryControllerSlotNamer>(std::move(mc));
     break;
+  case InternalStateNamer::TYPE::EffectiveSlot:
+    if (!mapper.map(InternalStateNamer::INNER_LIT, es))
+      return false;
+    namer = std::make_unique<EffectiveSlotNamer>(std::move(es));
+    break;
   }
   namer->type = type;
   return true;
 }
 
+bool fromJSON(const llvm::json::Value &value,
+              std::shared_ptr<InternalStateNamer> &namer,
+              llvm::json::Path path) {
+  std::unique_ptr<InternalStateNamer> unique;
+
+  if (!fromJSON(value, unique, path))
+    return false;
+  namer = std::move(unique);
+  return true;
+}
+
 std::unique_ptr<ConstrainedNamer>
-InternalStateNamer::tryConstrain(int32_t value) {
+InternalStateNamer::tryConstrain(int32_t value) const {
   if (auto *namer = dyn_cast<EagerForkSentNamer>(this)) {
     return std::make_unique<ConstrainedEagerForkSentNamer>(
         namer->constrain(value));
@@ -118,6 +140,9 @@ InternalStateNamer::tryConstrain(int32_t value) {
     return std::make_unique<ConstrainedBufferSlotFullNamer>(
         namer->constrain(value));
   }
+  if (auto *namer = dyn_cast<EffectiveSlotNamer>(this)) {
+    return namer->constrain(value);
+  }
 
   return nullptr;
 }
@@ -131,7 +156,8 @@ bool fromJSON(const llvm::json::Value &value, EagerForkSentNamer &namer,
          mapper.map(EagerForkSentNamer::CHANNEL_SIZE_LIT, namer.channelSize);
 }
 
-ConstrainedEagerForkSentNamer EagerForkSentNamer::constrain(int32_t value) {
+ConstrainedEagerForkSentNamer
+EagerForkSentNamer::constrain(int32_t value) const {
   ConstrainedEagerForkSentNamer p(*this, value);
   return p;
 }
@@ -146,7 +172,8 @@ bool fromJSON(const llvm::json::Value &value, BufferSlotFullNamer &namer,
          mapper.map(BufferSlotFullNamer::SLOT_SIZE_LIT, namer.slotSize);
 }
 
-ConstrainedBufferSlotFullNamer BufferSlotFullNamer::constrain(int32_t value) {
+ConstrainedBufferSlotFullNamer
+BufferSlotFullNamer::constrain(int32_t value) const {
   ConstrainedBufferSlotFullNamer p(*this, value);
   return p;
 }
@@ -188,5 +215,34 @@ bool fromJSON(const llvm::json::Value &value, MemoryControllerSlotNamer &namer,
   return true;
 }
 
+std::string EffectiveSlotNamer::getSMVName() const {
+  if (copiedSents.empty()) {
+    return slot->getSMVName();
+  }
+
+  std::vector<std::string> sentNames;
+  sentNames.reserve(copiedSents.size());
+  for (auto &sent : copiedSents) {
+    sentNames.push_back(llvm::formatv("!{0}", sent.getSMVName()));
+  }
+  return llvm::formatv("({0} & {1})", slot->getSMVName(),
+                       llvm::join(sentNames, " & "));
+}
+llvm::json::Value EffectiveSlotNamer::toInnerJSON() const {
+  return llvm::json::Object(
+      {{SLOT_LIT, slot}, {COPIED_SENTS_LIT, copiedSents}});
+}
+
+bool fromJSON(const llvm::json::Value &value, EffectiveSlotNamer &namer,
+              llvm::json::Path path) {
+  llvm::json::ObjectMapper mapper(value, path);
+  return mapper && mapper.map(EffectiveSlotNamer::SLOT_LIT, namer.slot) &&
+         mapper.map(EffectiveSlotNamer::COPIED_SENTS_LIT, namer.copiedSents);
+}
+
+std::unique_ptr<ConstrainedNamer>
+EffectiveSlotNamer::constrain(int32_t value) const {
+  return std::make_unique<ConstrainedEffectiveSlotNamer>(*this, value);
+}
 } // namespace handshake
 } // namespace dynamatic
diff --git a/tools/export-rtl/export-rtl.cpp b/tools/export-rtl/export-rtl.cpp
index 5173a0e1e..79008c70e 100644
--- a/tools/export-rtl/export-rtl.cpp
+++ b/tools/export-rtl/export-rtl.cpp
@@ -1302,6 +1302,45 @@ LogicalResult SMVWriter::createProperties(WriteModData &data) const {
       }
       std::string propertyString = llvm::join(eqs, " & ");
       data.properties[p->getId()] = {propertyString, propertyTag};
+    } else if (auto *p = llvm::dyn_cast<EntryTokenOrder>(property.get())) {
+      std::vector<std::string> ends{};
+      const auto &slots = p->getSlots();
+      assert(slots.size() >= 2);
+
+      for (auto start = slots.begin(); start != slots.end(); ++start) {
+        std::string entryToken = start->constrain(p->getValue())->getSMVName();
+        std::vector<std::string> laterSlots{};
+        for (auto later = start + 1; later != slots.end(); ++later) {
+          // Any later slot must not be full
+          laterSlots.emplace_back(llvm::formatv("!({0})", later->getSMVName()));
+        }
+        // if laterSlots is empty, there is nothing to annotate with this
+        // starting slot
+        if (laterSlots.empty()) {
+          continue;
+        }
+
+        ends.push_back(llvm::formatv("(({0}) -> ({1}))", entryToken,
+                                     llvm::join(laterSlots, " & ")));
+      }
+      // This holds because every EntryTokenOrder slot path contains at least
+      // two slots
+      assert(!ends.empty());
+      std::string propertyString = llvm::join(ends, " & ");
+      data.properties[p->getId()] = {propertyString, propertyTag};
+    } else if (auto *p = llvm::dyn_cast<SingleEntryToken>(property.get())) {
+      std::vector<std::string> cmStrs;
+      for (const auto &x : p->getCmPath()) {
+        cmStrs.push_back(x.getSMVName());
+      }
+      std::vector<std::string> ecStrs;
+      for (const auto &x : p->getEcPath()) {
+        ecStrs.push_back(x.getSMVName());
+      }
+      std::string propertyString =
+          llvm::formatv("count({0}) > 0 -> count({1}) = 0",
+                        llvm::join(cmStrs, ", "), llvm::join(ecStrs, ", "));
+      data.properties[p->getId()] = {propertyString, propertyTag};
     } else {
       llvm::errs() << "Formal property Type not known\n";
       return failure();