diff --git a/experimental/include/experimental/Support/FormalProperty.h b/experimental/include/experimental/Support/FormalProperty.h index 11d5b181df..7e1b07b1e3 100644 --- a/experimental/include/experimental/Support/FormalProperty.h +++ b/experimental/include/experimental/Support/FormalProperty.h @@ -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; } @@ -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: @@ -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: @@ -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 getForkOps() { return forkOps; } + std::vector getOutputIdxs() { return outputIdxs; } + + llvm::json::Value extraInfoToJSON() const override; + + static std::unique_ptr + fromJSON(const llvm::json::Value &value, llvm::json::Path path); + + PathSingleSentForkOutput() = default; + PathSingleSentForkOutput(unsigned long id, TAG tag, + const std::vector &forkOps, + const std::vector &outputIdxs); + ~PathSingleSentForkOutput() = default; + + static bool classof(const FormalProperty *fp) { + return fp->getType() == TYPE::PathSingleSentForkOutput; + } + +private: + std::vector forkOps; + std::vector outputIdxs; + inline static const StringLiteral FORK_OPS_LIT = "fork_ops"; + inline static const StringLiteral OUTPUT_IDXS_LIT = "output_idxs"; +}; + class FormalPropertyTable { public: FormalPropertyTable() = default; diff --git a/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp b/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp index 92e6b6b94e..7790d0b72d 100644 --- a/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp +++ b/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp @@ -73,6 +73,13 @@ struct HandshakeAnnotatePropertiesPass Operation &curOp); LogicalResult annotateCopiedSlots(Operation &op); LogicalResult annotateCopiedSlotsOfAllForks(ModuleOp modOp); + + LogicalResult annotatePathSingleForkSentRec( + const std::unordered_set &visitedSet, + const std::vector &prevForks, + const std::vector &prevIdxs, Operation &curOp, + bool annotateIdxs); + LogicalResult annotatePathSingleForkSent(ModuleOp modOp); bool isChannelToBeChecked(OpResult res); }; } // namespace @@ -223,6 +230,78 @@ HandshakeAnnotatePropertiesPass::annotateCopiedSlotsOfAllForks(ModuleOp modOp) { return success(); } +LogicalResult HandshakeAnnotatePropertiesPass::annotatePathSingleForkSentRec( + const std::unordered_set &visitedSet, + const std::vector &prevForks, + const std::vector &prevIdxs, Operation &curOp, + bool annotateIdxs) { + for (auto [i, res] : llvm::enumerate(curOp.getResults())) { + std::vector 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 newVisited = visitedSet; + newVisited.insert(id); + + // Found a slot, which marks the end of this path + if (auto bufOp = dyn_cast(op)) { + continue; + } + + if (auto forkOp = dyn_cast(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()) { + for (Operation &op : funcOp.getOps()) { + if (auto forkOp = dyn_cast(op)) { + std::vector names{}; + std::vector outputs{}; + std::unordered_set 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(); @@ -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)); diff --git a/experimental/lib/Support/FormalProperty.cpp b/experimental/lib/Support/FormalProperty.cpp index 94cca64a9d..93e4906051 100644 --- a/experimental/lib/Support/FormalProperty.cpp +++ b/experimental/lib/Support/FormalProperty.cpp @@ -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; } @@ -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"; } } @@ -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)); } } @@ -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(); } @@ -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(); @@ -304,6 +310,32 @@ CopiedSlotsOfActiveForkAreFull::fromJSON(const llvm::json::Value &value, return prop; } +PathSingleSentForkOutput::PathSingleSentForkOutput( + unsigned long id, TAG tag, const std::vector &forkOps, + const std::vector &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::fromJSON(const llvm::json::Value &value, + llvm::json::Path path) { + auto prop = std::make_unique(); + + 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()); diff --git a/experimental/tools/unit-generators/smv/generators/handshake/load.py b/experimental/tools/unit-generators/smv/generators/handshake/load.py index 3314328ce1..c486de307f 100644 --- a/experimental/tools/unit-generators/smv/generators/handshake/load.py +++ b/experimental/tools/unit-generators/smv/generators/handshake/load.py @@ -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})} diff --git a/tools/export-rtl/export-rtl.cpp b/tools/export-rtl/export-rtl.cpp index f047f8f5c8..6ecc7c0f56 100644 --- a/tools/export-rtl/export-rtl.cpp +++ b/tools/export-rtl/export-rtl.cpp @@ -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(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 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";