[Formal][Property Annotation] Annotate fork--copied-slot invariant

experimental/include/experimental/Analysis/Passes.td

@@ -26,7 +26,7 @@ def HandshakeAnnotateProperties : DynamaticPass< "handshake-annotate-properties"
   let constructor = "dynamatic::experimental::formalprop::createAnnotateProperties()";
   let options = [ Option<"jsonPath", "json-path", "std::string", "",
     "Path to JSON-formatted file where the properties' information is stored.">,
-    Option<"annotateInvariants", "annotate-invariants", "bool", "true",
+    Option<"annotateInvariants", "annotate-invariants", "bool", "false",
     "Annotate invariants to assist k-inductive proofs">];
 }
 

experimental/include/experimental/Support/FormalProperty.h

@@ -28,6 +28,7 @@ class FormalProperty {
     AOB /* Absence Of Backpressure */,
     VEQ /* Valid EQuivalence */,
     EFNAO /* Eager Fork Not All Output sent */,
+    CSOAFAF, /* Copied Slots Of Active Forks Are Full */
   };
 
   TAG getTag() const { return tag; }
@@ -187,6 +188,46 @@ class EagerForkNotAllOutputSent : public FormalProperty {
   inline static const StringLiteral NUM_EAGER_OUTPUTS_LIT = "num_eager_outputs";
 };
 
+// When an eager fork is `sent` state for at least one of its outputs, it is
+// considered `active`. When transitioning to the `active` state, the `ready`
+// signal is false, and the incoming token is blocked. Because of this, all
+// slots immediately before the fork (i.e. copied slots) must be full. More
+// formally, a copied slot of a fork is defined as a slot that has a path
+// towards the fork without any other slots on it. See invariant 2 of
+// https://ieeexplore.ieee.org/document/10323796 for more details
+class CopiedSlotsOfActiveForkAreFull : public FormalProperty {
+public:
+  std::string getForkOp() { return forkOp; }
+  unsigned getNumEagerForkOutputs() { return numEagerForkOutputs; }
+  std::string getBufferOp() { return bufferOp; }
+  unsigned getBufferSlot() { return bufferSlot; }
+
+  llvm::json::Value extraInfoToJSON() const override;
+
+  static std::unique_ptr<CopiedSlotsOfActiveForkAreFull>
+  fromJSON(const llvm::json::Value &value, llvm::json::Path path);
+
+  CopiedSlotsOfActiveForkAreFull() = default;
+  CopiedSlotsOfActiveForkAreFull(unsigned long id, TAG tag,
+                                 handshake::BufferLikeOpInterface &bufferOp,
+                                 handshake::EagerForkLikeOpInterface &forkOp);
+  ~CopiedSlotsOfActiveForkAreFull() = default;
+
+  static bool classof(const FormalProperty *fp) {
+    return fp->getType() == TYPE::CSOAFAF;
+  }
+
+private:
+  std::string forkOp;
+  unsigned numEagerForkOutputs;
+  std::string bufferOp;
+  unsigned bufferSlot;
+  inline static const StringLiteral FORK_OP_LIT = "fork_op";
+  inline static const StringLiteral NUM_EAGER_OUTPUTS_LIT = "num_eager_outputs";
+  inline static const StringLiteral BUFFER_OP_LIT = "buffer_op";
+  inline static const StringLiteral BUFFER_SLOT_LIT = "buffer_slot";
+};
+
 class FormalPropertyTable {
 public:
   FormalPropertyTable() = default;

experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp

@@ -35,6 +35,7 @@
 #include "llvm/Support/JSON.h"
 #include <fstream>
 #include <ostream>
+#include <unordered_set>
 
 using namespace llvm;
 using namespace mlir;
@@ -66,6 +67,12 @@ struct HandshakeAnnotatePropertiesPass
   LogicalResult annotateValidEquivalenceBetweenOps(Operation &op1,
                                                    Operation &op2);
   LogicalResult annotateEagerForkNotAllOutputSent(ModuleOp modOp);
+  LogicalResult
+  annotateCopiedSlotsRec(std::unordered_set<std::string> &visitedSet,
+                         handshake::EagerForkLikeOpInterface &originFork,
+                         Operation &curOp);
+  LogicalResult annotateCopiedSlots(Operation &op);
+  LogicalResult annotateCopiedSlotsOfAllForks(ModuleOp modOp);
   bool isChannelToBeChecked(OpResult res);
 };
 } // namespace
@@ -153,6 +160,69 @@ HandshakeAnnotatePropertiesPass::annotateEagerForkNotAllOutputSent(
   return success();
 }
 
+LogicalResult HandshakeAnnotatePropertiesPass::annotateCopiedSlotsRec(
+    std::unordered_set<std::string> &visitedSet,
+    handshake::EagerForkLikeOpInterface &originFork, Operation &curOp) {
+
+  // If this operation has been visited, there is nothing to do
+  std::string id = getUniqueName(&curOp).str();
+  if (auto iter = visitedSet.find(id); iter != visitedSet.end()) {
+    return success();
+  }
+  visitedSet.insert(id);
+
+  // If this operation contains a slot, the copied slot has been found and can
+  // be annotated
+  if (auto bufferOp = dyn_cast<handshake::BufferLikeOpInterface>(curOp)) {
+    CopiedSlotsOfActiveForkAreFull p(uid, FormalProperty::TAG::INVAR, bufferOp,
+                                     originFork);
+    propertyTable.push_back(p.toJSON());
+    uid++;
+    return success();
+  }
+
+  if (auto mergeOp = dyn_cast<handshake::MergeLikeOpInterface>(curOp)) {
+    // TODO: Which of the previous paths should be followed?
+    return success();
+  }
+
+  // Only JoinLikeOps or single-operand ops are remaining, but ideally a
+  // dyn_cast would happen for either case
+  for (auto value : curOp.getOperands()) {
+    Operation *prevOpPtr = value.getDefiningOp();
+    if (prevOpPtr == nullptr)
+      // if there is no defining op, the value must be a constant, and does not
+      // need to be annotated
+      continue;
+    Operation &prevOp = *prevOpPtr;
+    if (failed(annotateCopiedSlotsRec(visitedSet, originFork, prevOp))) {
+      return failure();
+    }
+  }
+
+  return success();
+}
+
+LogicalResult
+HandshakeAnnotatePropertiesPass::annotateCopiedSlots(Operation &op) {
+  std::unordered_set<std::string> visitedSet = {};
+  if (auto forkOp = dyn_cast<handshake::EagerForkLikeOpInterface>(op)) {
+    return annotateCopiedSlotsRec(visitedSet, forkOp, op);
+  }
+  return success();
+}
+
+LogicalResult
+HandshakeAnnotatePropertiesPass::annotateCopiedSlotsOfAllForks(ModuleOp modOp) {
+  for (handshake::FuncOp funcOp : modOp.getOps<handshake::FuncOp>()) {
+    for (Operation &op : funcOp.getOps()) {
+      if (failed(annotateCopiedSlots(op)))
+        return failure();
+    }
+  }
+  return success();
+}
+
 void HandshakeAnnotatePropertiesPass::runDynamaticPass() {
   ModuleOp modOp = getOperation();
 
@@ -163,6 +233,8 @@ void HandshakeAnnotatePropertiesPass::runDynamaticPass() {
   if (annotateInvariants) {
     if (failed(annotateEagerForkNotAllOutputSent(modOp)))
       return signalPassFailure();
+    if (failed(annotateCopiedSlotsOfAllForks(modOp)))
+      return signalPassFailure();
   }
 
   llvm::json::Value jsonVal(std::move(propertyTable));

experimental/lib/Support/FormalProperty.cpp

@@ -29,6 +29,8 @@ FormalProperty::typeFromStr(const std::string &s) {
     return FormalProperty::TYPE::VEQ;
   if (s == "EFNAO")
     return FormalProperty::TYPE::EFNAO;
+  if (s == "CSOAFAF")
+    return FormalProperty::TYPE::CSOAFAF;
 
   return std::nullopt;
 }
@@ -41,6 +43,8 @@ std::string FormalProperty::typeToStr(TYPE t) {
     return "VEQ";
   case TYPE::EFNAO:
     return "EFNAO";
+  case TYPE::CSOAFAF:
+    return "CSOAFAF";
   }
 }
 
@@ -95,6 +99,9 @@ FormalProperty::fromJSON(const llvm::json::Value &value,
     return ValidEquivalence::fromJSON(value, path.field(INFO_LIT));
   case TYPE::EFNAO:
     return EagerForkNotAllOutputSent::fromJSON(value, path.field(INFO_LIT));
+  case TYPE::CSOAFAF:
+    return CopiedSlotsOfActiveForkAreFull::fromJSON(value,
+                                                    path.field(INFO_LIT));
   }
 }
 
@@ -261,6 +268,42 @@ EagerForkNotAllOutputSent::fromJSON(const llvm::json::Value &value,
   return prop;
 }
 
+// Invariant 2 -- see https://ieeexplore.ieee.org/document/10323796
+
+CopiedSlotsOfActiveForkAreFull::CopiedSlotsOfActiveForkAreFull(
+    unsigned long id, TAG tag, handshake::BufferLikeOpInterface &bufferOpI,
+    handshake::EagerForkLikeOpInterface &forkOpI)
+    : FormalProperty(id, tag, TYPE::CSOAFAF) {
+  forkOp = getUniqueName(forkOpI).str();
+  numEagerForkOutputs = forkOpI.getNumEagerOutputs();
+  bufferOp = getUniqueName(bufferOpI).str();
+  bufferSlot = bufferOpI.getNumSlots() - 1;
+}
+
+llvm::json::Value CopiedSlotsOfActiveForkAreFull::extraInfoToJSON() const {
+  return llvm::json::Object({{FORK_OP_LIT, forkOp},
+                             {NUM_EAGER_OUTPUTS_LIT, numEagerForkOutputs},
+                             {BUFFER_OP_LIT, bufferOp},
+                             {BUFFER_SLOT_LIT, bufferSlot}});
+}
+
+std::unique_ptr<CopiedSlotsOfActiveForkAreFull>
+CopiedSlotsOfActiveForkAreFull::fromJSON(const llvm::json::Value &value,
+                                         llvm::json::Path path) {
+  auto prop = std::make_unique<CopiedSlotsOfActiveForkAreFull>();
+
+  auto info = prop->parseBaseAndExtractInfo(value, path);
+  llvm::json::ObjectMapper mapper(info, path);
+
+  if (!mapper || !mapper.map(FORK_OP_LIT, prop->forkOp) ||
+      !mapper.map(NUM_EAGER_OUTPUTS_LIT, prop->numEagerForkOutputs) ||
+      !mapper.map(BUFFER_OP_LIT, prop->bufferOp) ||
+      !mapper.map(BUFFER_SLOT_LIT, prop->bufferSlot))
+    return nullptr;
+
+  return prop;
+}
+
 LogicalResult FormalPropertyTable::addPropertiesFromJSON(StringRef filepath) {
   // Open the properties' database
   std::ifstream inputFile(filepath.str());

experimental/tools/rigidification/rigidification.sh

@@ -34,7 +34,7 @@ rm -rf "$FORMAL_DIR" && mkdir -p "$FORMAL_DIR"
 
 # Annotate properties
 "$DYNAMATIC_OPT_BIN" "$F_HANDSHAKE_EXPORT" \
-  --handshake-annotate-properties=json-path=$F_FORMAL_PROP \
+  --handshake-annotate-properties="json-path=$F_FORMAL_PROP annotate-invariants" \
   > /dev/null
 
 # handshake level -> hw level

experimental/tools/unit-generators/smv/generators/handshake/buffers/one_slot_break_dv.py

@@ -46,6 +46,7 @@ def _generate_one_slot_break_dv(name, data_type):
   ins_ready := inner_one_slot_break_dv.ins_ready;
   outs_valid := inner_one_slot_break_dv.outs_valid;
   outs := data;
+  full_0 := inner_one_slot_break_dv.outs_valid_i;
 
 {_generate_one_slot_break_dv_dataless(f"{name}__one_slot_break_dv_dataless")}
 """

experimental/tools/unit-generators/smv/generators/handshake/buffers/one_slot_break_r.py

@@ -24,6 +24,7 @@ def _generate_one_slot_break_r_dataless(name):
   DEFINE
   ins_ready := !full;
   outs_valid := ins_valid | full;
+  full_0 := full;
 """
 
 
@@ -43,6 +44,7 @@ def _generate_one_slot_break_r(name, data_type):
   ins_ready := inner_one_slot_break_r.ins_ready;
   outs_valid := inner_one_slot_break_r.outs_valid;
   outs := inner_one_slot_break_r.full ? data : ins;
+  full_0 := inner_one_slot_break_r.full;
 
 {_generate_one_slot_break_r_dataless(f"{name}__one_slot_break_r_dataless")}
 """

experimental/tools/unit-generators/smv/generators/handshake/control_merge.py

@@ -36,6 +36,7 @@ def _generate_control_merge_dataless(name, size, index_type):
   outs_valid := inner_fork.outs_0_valid;
   index_valid := inner_fork.outs_1_valid;
   index := inner_one_slot_break_r.outs;
+  full_0 := inner_one_slot_break_r.full_0;
 
 {generate_merge(f"{name}__merge_dataless", {ATTR_SIZE: size, ATTR_BITWIDTH: 0})}
 {generate_one_slot_break_r(f"{name}__one_slot_break_r", {ATTR_BITWIDTH: index_type.bitwidth})}
@@ -62,6 +63,7 @@ def _generate_control_merge(name, size, index_type, data_type):
   index_valid := inner_control_merge.index_valid;
   outs := data;
   index := inner_control_merge.index;
+  full_0 := inner_control_merge.full_0;
 
 {_generate_control_merge_dataless(f"{name}__control_merge_dataless", size, index_type)}
 """

tools/export-rtl/export-rtl.cpp

@@ -1268,6 +1268,23 @@ LogicalResult SMVWriter::createProperties(WriteModData &data) const {
       // e.g. count(fork0.sent_0, fork0.sent_1) < 2
       // for operation "fork0" with 2 eager outputs
       data.properties[p->getId()] = {propertyString, propertyTag};
+    } else if (auto *p = llvm::dyn_cast<CopiedSlotsOfActiveForkAreFull>(
+                   property.get())) {
+      unsigned numOut = p->getNumEagerForkOutputs();
+      std::string forkName = p->getForkOp();
+      std::string bufferName = p->getBufferOp();
+      int bufferSlot = p->getBufferSlot();
+      std::vector<std::string> forkOutNames{numOut};
+      for (unsigned i = 0; i < numOut; ++i) {
+        forkOutNames[i] = llvm::formatv("{0}.sent_{1}", forkName, i).str();
+      }
+      std::string bufferFull =
+          llvm::formatv("{0}.full_{1}", bufferName, bufferSlot).str();
+      std::string propertyString =
+          llvm::formatv("({0}) -> {1}", llvm::join(forkOutNames, " | "),
+                        bufferFull)
+              .str();
+      data.properties[p->getId()] = {propertyString, propertyTag};
     } else {
       llvm::errs() << "Formal property Type not known\n";
       return failure();