Skip to content

[Formal][Property Annotation] Annotate path--single-sent-fork-output #713

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
Basmet0 wants to merge 10 commits into
base: main
Choose a base branch
from
Draft

[Formal][Property Annotation] Annotate path--single-sent-fork-output #713

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
5661257
invariant 3 boilerplate
Jan 15, 2026
e20fcce
invariant 3 annotation and generation
Jan 16, 2026
5d8a65d
comment explaining the invariant
Jan 19, 2026
8d0c16a
removed debug prints
Jan 21, 2026
7e44421
added consistent naming of load operator slots in the smv unit generator
Jan 21, 2026
d59e069
better naming of functions
Jan 21, 2026
bc8b531
formatting
Jan 21, 2026
1944deb
expand acronyms
Feb 5, 2026
023be43
combined everything into a single function
Feb 5, 2026
baeb978
formatting
Feb 5, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
43 changes: 39 additions & 4 deletions experimental/include/experimental/Support/FormalProperty.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,8 +27,9 @@ class FormalProperty {
enum class TYPE {
AOB /* Absence Of Backpressure */,
VEQ /* Valid EQuivalence */,
EFNAO /* Eager Fork Not All Output sent */,
CSOAFAF, /* Copied Slots Of Active Forks Are Full */
EagerForkNotAllOutputSent, /* Eager Fork Not All Output sent */
CopiedSlotsOfActiveForksAreFull, /* Copied Slots Of Active Forks Are Full */
PathSingleSentForkOutput, /* Path Single Sent Fork Output */
};

TAG getTag() const { return tag; }
Expand Down Expand Up @@ -178,7 +179,7 @@ class EagerForkNotAllOutputSent : public FormalProperty {
~EagerForkNotAllOutputSent() = default;

static bool classof(const FormalProperty *fp) {
return fp->getType() == TYPE::EFNAO;
return fp->getType() == TYPE::EagerForkNotAllOutputSent;
}

private:
Expand Down Expand Up @@ -214,7 +215,7 @@ class CopiedSlotsOfActiveForkAreFull : public FormalProperty {
~CopiedSlotsOfActiveForkAreFull() = default;

static bool classof(const FormalProperty *fp) {
return fp->getType() == TYPE::CSOAFAF;
return fp->getType() == TYPE::CopiedSlotsOfActiveForksAreFull;
}

private:
Expand All @@ -228,6 +229,40 @@ class CopiedSlotsOfActiveForkAreFull : public FormalProperty {
inline static const StringLiteral BUFFER_SLOT_LIT = "buffer_slot";
};

// For any path that does not contain any slots, only at most a single fork
// output along that path can be in the `sent` state. In other words, if there
// is a path containing two fork outputs in the `sent` state, there has to be a
// slot containing a token between them, as the earlier `sent` output duplicated
// a token onto this path, and the later `sent` output blocks the token from
// leaving the path. See invariant 3 of
// https://ieeexplore.ieee.org/document/10323796 for more details
class PathSingleSentForkOutput : public FormalProperty {
public:
std::vector<std::string> getForkOps() { return forkOps; }
std::vector<unsigned> getOutputIdxs() { return outputIdxs; }

llvm::json::Value extraInfoToJSON() const override;

static std::unique_ptr<PathSingleSentForkOutput>
fromJSON(const llvm::json::Value &value, llvm::json::Path path);

PathSingleSentForkOutput() = default;
PathSingleSentForkOutput(unsigned long id, TAG tag,
const std::vector<std::string> &forkOps,
const std::vector<unsigned> &outputIdxs);
~PathSingleSentForkOutput() = default;

static bool classof(const FormalProperty *fp) {
return fp->getType() == TYPE::PathSingleSentForkOutput;
}

private:
std::vector<std::string> forkOps;
std::vector<unsigned> outputIdxs;
inline static const StringLiteral FORK_OPS_LIT = "fork_ops";
inline static const StringLiteral OUTPUT_IDXS_LIT = "output_idxs";
};

class FormalPropertyTable {
public:
FormalPropertyTable() = default;
Expand Down
81 changes: 81 additions & 0 deletions experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -73,6 +73,13 @@ struct HandshakeAnnotatePropertiesPass
Operation &curOp);
LogicalResult annotateCopiedSlots(Operation &op);
LogicalResult annotateCopiedSlotsOfAllForks(ModuleOp modOp);

LogicalResult annotatePathSingleForkSentRec(
const std::unordered_set<std::string> &visitedSet,
const std::vector<std::string> &prevForks,
const std::vector<unsigned> &prevIdxs, Operation &curOp,
bool annotateIdxs);
LogicalResult annotatePathSingleForkSent(ModuleOp modOp);
bool isChannelToBeChecked(OpResult res);
};
} // namespace
Expand Down Expand Up @@ -223,6 +230,78 @@ HandshakeAnnotatePropertiesPass::annotateCopiedSlotsOfAllForks(ModuleOp modOp) {
return success();
}

LogicalResult HandshakeAnnotatePropertiesPass::annotatePathSingleForkSentRec(
const std::unordered_set<std::string> &visitedSet,
const std::vector<std::string> &prevForks,
const std::vector<unsigned> &prevIdxs, Operation &curOp,
bool annotateIdxs) {
for (auto [i, res] : llvm::enumerate(curOp.getResults())) {
std::vector<unsigned> nextIdxs = prevIdxs;
if (annotateIdxs) {
nextIdxs.push_back(i);
if (prevForks.size() != nextIdxs.size()) {
llvm::errs() << "Different Indexs size and forks size\n";
return failure();
}
// No need to annotate properties of length 1 or lower
if (prevForks.size() > 1) {
PathSingleSentForkOutput p(uid, FormalProperty::TAG::INVAR, prevForks,
nextIdxs);
propertyTable.push_back(p.toJSON());
uid++;
}
}
for (auto *op : res.getUsers()) {
// If this operation has been visited, there is nothing to do
std::string id = getUniqueName(op).str();
if (auto iter = visitedSet.find(id); iter != visitedSet.end()) {
continue;
}
std::unordered_set<std::string> newVisited = visitedSet;
newVisited.insert(id);

// Found a slot, which marks the end of this path
if (auto bufOp = dyn_cast<handshake::BufferLikeOpInterface>(op)) {
continue;
}

if (auto forkOp = dyn_cast<handshake::EagerForkLikeOpInterface>(op)) {
auto nextForks = prevForks;
nextForks.push_back(id);
if (failed(annotatePathSingleForkSentRec(newVisited, nextForks,
nextIdxs, *op, true))) {
return failure();
}
} else {
if (failed(annotatePathSingleForkSentRec(newVisited, prevForks,
nextIdxs, *op, false))) {
return failure();
}
}
}
}
return success();
}

LogicalResult
HandshakeAnnotatePropertiesPass::annotatePathSingleForkSent(ModuleOp modOp) {
for (handshake::FuncOp funcOp : modOp.getOps<handshake::FuncOp>()) {
for (Operation &op : funcOp.getOps()) {
if (auto forkOp = dyn_cast<handshake::EagerForkLikeOpInterface>(op)) {
std::vector<std::string> names{};
std::vector<unsigned> outputs{};
Comment on lines +291 to +292
Copy link
Copy Markdown
Member

@Jiahui17 Jiahui17 Jan 29, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Store the ops instead of names (extract the names just right before dumping them to json

Makes more sense to have an internal data structure for holding the path we need, something like:

// Stored in detail namespace since they are internal data structures for implementing algorithms
namespace detail {
/// Add the documentation here
struct BufferLessPathNode {
  Operation op;
  Value val;
};
};

std::unordered_set<std::string> visited{};
names.push_back(getUniqueName(&op).str());
if (failed(annotatePathSingleForkSentRec(visited, names, outputs, op,
true))) {
return failure();
}
}
}
}
return success();
}

void HandshakeAnnotatePropertiesPass::runDynamaticPass() {
ModuleOp modOp = getOperation();

Expand All @@ -235,6 +314,8 @@ void HandshakeAnnotatePropertiesPass::runDynamaticPass() {
return signalPassFailure();
if (failed(annotateCopiedSlotsOfAllForks(modOp)))
return signalPassFailure();
if (failed(annotatePathSingleForkSent(modOp)))
return signalPassFailure();
}

llvm::json::Value jsonVal(std::move(propertyTable));
Expand Down
48 changes: 40 additions & 8 deletions experimental/lib/Support/FormalProperty.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -28,9 +28,11 @@ FormalProperty::typeFromStr(const std::string &s) {
if (s == "VEQ")
return FormalProperty::TYPE::VEQ;
if (s == "EFNAO")
return FormalProperty::TYPE::EFNAO;
return FormalProperty::TYPE::EagerForkNotAllOutputSent;
if (s == "CSOAFAF")
return FormalProperty::TYPE::CSOAFAF;
return FormalProperty::TYPE::CopiedSlotsOfActiveForksAreFull;
if (s == "PSSFO")
return FormalProperty::TYPE::PathSingleSentForkOutput;

return std::nullopt;
}
Expand All @@ -41,10 +43,12 @@ std::string FormalProperty::typeToStr(TYPE t) {
return "AOB";
case TYPE::VEQ:
return "VEQ";
case TYPE::EFNAO:
case TYPE::EagerForkNotAllOutputSent:
return "EFNAO";
case TYPE::CSOAFAF:
case TYPE::CopiedSlotsOfActiveForksAreFull:
return "CSOAFAF";
case TYPE::PathSingleSentForkOutput:
return "PSSFO";
}
}

Expand Down Expand Up @@ -97,11 +101,13 @@ FormalProperty::fromJSON(const llvm::json::Value &value,
return AbsenceOfBackpressure::fromJSON(value, path.field(INFO_LIT));
case TYPE::VEQ:
return ValidEquivalence::fromJSON(value, path.field(INFO_LIT));
case TYPE::EFNAO:
case TYPE::EagerForkNotAllOutputSent:
return EagerForkNotAllOutputSent::fromJSON(value, path.field(INFO_LIT));
case TYPE::CSOAFAF:
case TYPE::CopiedSlotsOfActiveForksAreFull:
return CopiedSlotsOfActiveForkAreFull::fromJSON(value,
path.field(INFO_LIT));
case TYPE::PathSingleSentForkOutput:
return PathSingleSentForkOutput::fromJSON(value, path.field(INFO_LIT));
}
}

Expand Down Expand Up @@ -243,7 +249,7 @@ ValidEquivalence::fromJSON(const llvm::json::Value &value,

EagerForkNotAllOutputSent::EagerForkNotAllOutputSent(
unsigned long id, TAG tag, handshake::EagerForkLikeOpInterface &forkOp)
: FormalProperty(id, tag, TYPE::EFNAO) {
: FormalProperty(id, tag, TYPE::EagerForkNotAllOutputSent) {
ownerOp = getUniqueName(forkOp).str();
numEagerForkOutputs = forkOp.getNumEagerOutputs();
}
Expand Down Expand Up @@ -273,7 +279,7 @@ EagerForkNotAllOutputSent::fromJSON(const llvm::json::Value &value,
CopiedSlotsOfActiveForkAreFull::CopiedSlotsOfActiveForkAreFull(
unsigned long id, TAG tag, handshake::BufferLikeOpInterface &bufferOpI,
handshake::EagerForkLikeOpInterface &forkOpI)
: FormalProperty(id, tag, TYPE::CSOAFAF) {
: FormalProperty(id, tag, TYPE::CopiedSlotsOfActiveForksAreFull) {
forkOp = getUniqueName(forkOpI).str();
numEagerForkOutputs = forkOpI.getNumEagerOutputs();
bufferOp = getUniqueName(bufferOpI).str();
Expand Down Expand Up @@ -304,6 +310,32 @@ CopiedSlotsOfActiveForkAreFull::fromJSON(const llvm::json::Value &value,
return prop;
}

PathSingleSentForkOutput::PathSingleSentForkOutput(
unsigned long id, TAG tag, const std::vector<std::string> &forkOps,
const std::vector<unsigned> &outputIdxs)
: FormalProperty(id, tag, TYPE::PathSingleSentForkOutput), forkOps{forkOps},
outputIdxs{outputIdxs} {}

llvm::json::Value PathSingleSentForkOutput::extraInfoToJSON() const {
return llvm::json::Object(
{{FORK_OPS_LIT, forkOps}, {OUTPUT_IDXS_LIT, outputIdxs}});
}

std::unique_ptr<PathSingleSentForkOutput>
PathSingleSentForkOutput::fromJSON(const llvm::json::Value &value,
llvm::json::Path path) {
auto prop = std::make_unique<PathSingleSentForkOutput>();

auto info = prop->parseBaseAndExtractInfo(value, path);
llvm::json::ObjectMapper mapper(info, path);

if (!mapper || !mapper.map(FORK_OPS_LIT, prop->forkOps) ||
!mapper.map(OUTPUT_IDXS_LIT, prop->outputIdxs))
return nullptr;

return prop;
}

LogicalResult FormalPropertyTable::addPropertiesFromJSON(StringRef filepath) {
// Open the properties' database
std::ifstream inputFile(filepath.str());
Expand Down
2 changes: 2 additions & 0 deletions experimental/tools/unit-generators/smv/generators/handshake/load.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,8 @@ def _generate_load(name, data_type, addr_type):
dataFromMem_ready := inner_data_one_slot_break_r.ins_ready;
dataOut := inner_data_one_slot_break_r.outs;
dataOut_valid := inner_data_one_slot_break_r.outs_valid;
full_0 := inner_addr_one_slot_break_r.full_0;
full_1 := inner_data_one_slot_break_r.full_0;

{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})}
Expand Down
19 changes: 19 additions & 0 deletions tools/export-rtl/export-rtl.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1285,6 +1285,25 @@ LogicalResult SMVWriter::createProperties(WriteModData &data) const {
llvm::formatv("({0}) -> {1}", llvm::join(forkOutNames, " | "),
bufferFull)
.str();
// e.g. (fork6.sent_0 | fork6.sent_1) -> load1.full_1
// when the second slot of load1 is a copied slot of fork6
data.properties[p->getId()] = {propertyString, propertyTag};
} else if (auto *p =
llvm::dyn_cast<PathSingleSentForkOutput>(property.get())) {
// e.g. count(fork0.sent_0, fork1.sent_1, fork2.sent_0) <= 2
auto names = p->getForkOps();
auto idxs = p->getOutputIdxs();
if (names.size() != idxs.size()) {
llvm::errs() << "Expected equal number of forks and fork outputs in "
"PathSingleSentForkOutput invariant\n";
return failure();
}
std::vector<std::string> forkOutNames{names.size()};
for (size_t i = 0; i < names.size(); ++i) {
forkOutNames[i] = llvm::formatv("{0}.sent_{1}", names[i], idxs[i]);
}
std::string propertyString =
llvm::formatv("count({0}) <= 1", llvm::join(forkOutNames, ", "));
data.properties[p->getId()] = {propertyString, propertyTag};
} else {
llvm::errs() << "Formal property Type not known\n";
Expand Down