[Formal][PropertyAnnotation]Buffer slot namers fix

experimental/lib/Support/FlowExpression.cpp

@@ -448,6 +448,7 @@ LogicalResult FlowEquationExtractor::extractBufferOp(BufferOp bufferOp) {
     // Then, `in` is set to `next`
     auto slot = FlowVariable(FlowInternalState(slotNamer));
     FlowVariable next = in.nextInternal();
+    slot.indexTokenTracker = in.indexTokenTracker;
     if (failed(extractSlotEquation(in, next, slot))) {
       return failure();
     }

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

@@ -31,6 +31,7 @@ def _generate_one_slot_break_none_dataless(name):
     DEFINE
     outs_valid := full | ins_valid;
     ins_ready := (!full) | outs_ready;
+    slot_0_full := full;
 """
 
 
@@ -52,6 +53,8 @@ def _generate_one_slot_break_none(name, data_type):
     outs := full ? reg : ins;
     outs_valid := full | ins_valid;
     ins_ready := (!full) | outs_ready;
+    slot_0_full := full;
+    data_0 := reg;
 """
 
 

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

@@ -24,7 +24,6 @@ def _generate_one_slot_break_dv_dataless(name):
   DEFINE
   ins_ready := !outs_valid_i | outs_ready;
   outs_valid := outs_valid_i;
-  slot_0_full := outs_valid_i;
 """
 
 
@@ -46,8 +45,8 @@ def _generate_one_slot_break_dv(name, data_type):
   DEFINE
   ins_ready := inner_one_slot_break_dv.ins_ready;
   outs_valid := inner_one_slot_break_dv.outs_valid;
+  outs_valid_i := inner_one_slot_break_dv.outs_valid_i;
   outs := data;
-  slot_0_full := 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,8 +24,6 @@ def _generate_one_slot_break_r_dataless(name):
   DEFINE
   ins_ready := !full;
   outs_valid := ins_valid | full;
-
-  slot_0_full := full;
 """
 
 
@@ -46,7 +44,7 @@ def _generate_one_slot_break_r(name, data_type):
   outs_valid := inner_one_slot_break_r.outs_valid;
   outs := inner_one_slot_break_r.full ? data : ins;
 
-  slot_0_full := inner_one_slot_break_r.slot_0_full;
+  full := 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,7 +36,7 @@ def _generate_control_merge_dataless(name, size, index_type):
   index_valid := inner_fork.outs_1_valid;
   index := inner_one_slot_break_r.outs;
 
-  slot_full := inner_one_slot_break_r.slot_0_full;
+  slot_full := inner_one_slot_break_r.full;
   data := inner_one_slot_break_r.data;
 
   outs_sent := inner_fork.outs_0_sent;
@@ -69,9 +69,5 @@ def _generate_control_merge(name, size, index_type, data_type):
   outs := data;
   index := inner_control_merge.index;
 
-  outs_sent := inner_control_merge.outs_sent;
-  index_sent := inner_control_merge.index_sent;
-  slot_full := inner_control_merge.slot_full;
-
 {_generate_control_merge_dataless(f"{name}__control_merge_dataless", size, index_type)}
 """

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

@@ -25,8 +25,8 @@ def _generate_load(name, data_type, addr_type):
   dataOut := inner_data_one_slot_break_r.outs;
   dataOut_valid := inner_data_one_slot_break_r.outs_valid;
 
-  addr_full := inner_addr_one_slot_break_r.slot_0_full;
-  data_full := inner_data_one_slot_break_r.slot_0_full;
+  addr_full := inner_addr_one_slot_break_r.full;
+  data_full := inner_data_one_slot_break_r.full;
 
 {generate_one_slot_break_r(f"{name}__addr_one_slot_break_r", {ATTR_BITWIDTH: addr_type.bitwidth})}
 {generate_one_slot_break_r(f"{name}__data_one_slot_break_r", {ATTR_BITWIDTH: data_type.bitwidth})}

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

@@ -4,6 +4,8 @@
 def generate_sink(name, params):
     data_type = SmvScalarType(params[ATTR_BITWIDTH])
 
+    if "pyTest" in params:
+        return _generate_iog_terminating_sink_dataless(name)
     if data_type.bitwidth == 0:
         return _generate_sink_dataless(name)
     else:
@@ -28,3 +30,15 @@ def _generate_sink(name, data_type):
   DEFINE
   ins_ready  :=  TRUE;
 """
+
+
+def _generate_iog_terminating_sink_dataless(name):
+    return f"""
+MODULE {name}(ins_valid)
+
+  VAR
+  slot_full : bool;
+  -- output
+  DEFINE
+  ins_ready  :=  !slot_full;
+"""

experimental/tools/unit-generators/smv/generators/support/delay_buffer.py

@@ -53,7 +53,7 @@ def _generate_delay_buffer(name, latency):
   -- output
   DEFINE ins_ready := inner_one_slot_break_dv.ins_ready;
   DEFINE outs_valid := inner_one_slot_break_dv.outs_valid;
-  DEFINE v{no_one_slot_break_dv_latency} := inner_one_slot_break_dv.slot_0_full;
+  DEFINE v{no_one_slot_break_dv_latency} := inner_one_slot_break_dv.outs_valid_i;
 
 {generate_one_slot_break_dv(f"{name}__one_slot_break_dv_dataless", {ATTR_BITWIDTH: 0})}
 """

include/dynamatic/Dialect/Handshake/HandshakeOpInternalStateNamer.h

@@ -194,9 +194,9 @@ struct ConstrainedEagerForkSentNamer : ConstrainedNamer {
 struct BufferSlotFullNamer : InternalStateNamer {
   BufferSlotFullNamer() = default;
   BufferSlotFullNamer(const std::string &opName, const std::string &slotName,
-                      size_t slotSize)
+                      const std::string &dataName, size_t slotSize)
       : InternalStateNamer(TYPE::BufferSlotFull), opName(opName),
-        slotName(slotName), slotSize(slotSize) {}
+        slotName(slotName), dataName(dataName), slotSize(slotSize) {}
   ~BufferSlotFullNamer() = default;
 
   static inline bool classof(const InternalStateNamer *fp) {
@@ -206,12 +206,13 @@ struct BufferSlotFullNamer : InternalStateNamer {
   ConstrainedBufferSlotFullNamer constrain(int32_t value);
 
   inline std::string getSMVName() const override {
-    return llvm::formatv("{0}.{1}_full", opName, slotName).str();
+    return llvm::formatv("{0}.{1}", opName, slotName).str();
   }
   inline llvm::json::Value toInnerJSON() const override {
     return llvm::json::Object({
         {OPERATION_LIT, opName},
         {SLOT_NAME_LIT, slotName},
+        {DATA_NAME_LIT, dataName},
         {SLOT_SIZE_LIT, slotSize},
     });
   }
@@ -221,9 +222,11 @@ struct BufferSlotFullNamer : InternalStateNamer {
 
   std::string opName;
   std::string slotName;
+  std::string dataName;
   size_t slotSize;
   static constexpr llvm::StringLiteral OPERATION_LIT = "operation";
   static constexpr llvm::StringLiteral SLOT_NAME_LIT = "slot_name";
+  static constexpr llvm::StringLiteral DATA_NAME_LIT = "data_name";
   static constexpr llvm::StringLiteral SLOT_SIZE_LIT = "slot_size";
 };
 
@@ -234,8 +237,11 @@ struct ConstrainedBufferSlotFullNamer : ConstrainedNamer {
   ~ConstrainedBufferSlotFullNamer() = default;
 
   inline std::string getSMVName() const override {
-    return llvm::formatv("{0} & ({1}.data = {2})", base.getSMVName(),
-                         base.opName, smvValue(base.slotSize, value))
+    // Assuming buffer1 contains a 32bit slot:
+    // buffer1.slot_full & (buffer1.slot_data = 0ud32_1)
+    return llvm::formatv("{0} & ({1}.{2} = {3})", base.getSMVName(),
+                         base.opName, base.dataName,
+                         smvValue(base.slotSize, value))
         .str();
   }
 

lib/Dialect/Handshake/HandshakeInterfaces.cpp

@@ -418,7 +418,8 @@ std::vector<BufferSlotFullNamer> ControlMergeOp::getInternalSlotStateNamers() {
          "Cannot get names of slot states for operation without name");
   handshake::ChannelType ct = getIndex().getType();
 
-  ret[0] = BufferSlotFullNamer(nameAttr.str(), "slot", ct.getDataBitWidth());
+  ret[0] = BufferSlotFullNamer(nameAttr.str(), "slot_full", "data",
+                               ct.getDataBitWidth());
   return ret;
 }
 
@@ -429,9 +430,11 @@ std::vector<BufferSlotFullNamer> LoadOp::getInternalSlotStateNamers() {
   assert(nameAttr &&
          "Cannot get names of slot states for operation without name");
 
-  ret[0] = BufferSlotFullNamer(nameAttr.str(), ADDR_SLOT_LIT.str(),
+  ret[0] = BufferSlotFullNamer(nameAttr.str(), ADDR_SLOT_LIT.str() + "_full",
+                               "NOT_ACCESSIBLE",
                                getAddress().getType().getDataBitWidth());
-  ret[1] = BufferSlotFullNamer(nameAttr.str(), DATA_SLOT_LIT.str(),
+  ret[1] = BufferSlotFullNamer(nameAttr.str(), DATA_SLOT_LIT.str() + "_full",
+                               "NOT_ACCESSIBLE",
                                getData().getType().getDataBitWidth());
   return ret;
 }
@@ -454,10 +457,39 @@ std::vector<BufferSlotFullNamer> BufferOp::getInternalSlotStateNamers() {
     assert(false && "Operand of BufferOp is not a channel");
   }
 
+  BufferType t = getBufferType();
+  switch (t) {
+  case BufferType::ONE_SLOT_BREAK_DV:
+    assert(ret.size() == 1);
+    ret[0] = BufferSlotFullNamer(nameAttr.str(), "outs_valid_i", "data", width);
+    break;
+  case BufferType::ONE_SLOT_BREAK_R:
+    assert(ret.size() == 1);
+    ret[0] = BufferSlotFullNamer(nameAttr.str(), "full", "data", width);
+    break;
+  case BufferType::FIFO_BREAK_NONE:
+    if (ret.size() == 1) {
+      ret[0] = BufferSlotFullNamer(nameAttr.str(), "full", "reg", width);
+    } else {
+      for (size_t i = 0; i < ret.size(); ++i) {
+        ret[i] = BufferSlotFullNamer(nameAttr.str(),
+                                     llvm::formatv("b{0}.full", i).str(),
+                                     llvm::formatv("b{0}.reg", i).str(), width);
+      }
+    }
+    break;
+  case BufferType::FIFO_BREAK_DV:
+  case BufferType::ONE_SLOT_BREAK_DVR:
+  case BufferType::SHIFT_REG_BREAK_DV:
+    llvm::report_fatal_error(
+        llvm::formatv("no name for buffer slot of type {0}", t));
+  }
+  /*
   for (size_t i = 0; i < getNumSlots(); ++i) {
     ret[i] =
         BufferSlotFullNamer(nameAttr.str(), "slot_" + std::to_string(i), width);
   }
+  */
   return ret;
 }
 

lib/Dialect/Handshake/HandshakeOpInternalStateNamer.cpp

@@ -114,6 +114,7 @@ BufferSlotFullNamer::fromInnerJSON(const llvm::json::Value &value,
   auto prop = std::make_unique<BufferSlotFullNamer>();
   if (!mapper || !mapper.map(OPERATION_LIT, prop->opName) ||
       !mapper.map(SLOT_NAME_LIT, prop->slotName) ||
+      !mapper.map(DATA_NAME_LIT, prop->dataName) ||
       !mapper.map(SLOT_SIZE_LIT, prop->slotSize))
     return nullptr;
   return prop;