[Formal][PropertyAnnotation] Annotating IOG-based invariants#855
Merged
Conversation
Jiahui17
reviewed
Apr 16, 2026
added 17 commits
April 16, 2026 15:26
… active fork in between
…t the first slot) edge case: As the MC is not part of the IOG, tokens "hidden" within MC are not accounted for
Mark slots as IOG-terminating, and annotate SMV with a single slot in that case Annotate entry slots Extract all slots and eager fork states from IOG Export invariant to SMV
pass "self" to module of the environment endOp is a terminating node
Jiahui17
reviewed
May 5, 2026
Member
Jiahui17
left a comment
Jiahui17
left a comment
There was a problem hiding this comment.
Some cosmetic comments (looking into IOG.cpp and HandshakeAnnotateProperties.cpp now..
Member
There was a problem hiding this comment.
maybe it is cleaner to add a new operation for this instead of adding more attributes...
Comment on lines
+36
to
+37
| SmallVector<std::string> inputVariables; | ||
| inputVariables.push_back("self"); |
Member
There was a problem hiding this comment.
// NOTE: self is ... (see page XX in the nuXmv user manual)
SmallVector<std::string> inputVariables = {"self"};
Jiahui17
reviewed
May 5, 2026
Member
Jiahui17
left a comment
Jiahui17
left a comment
There was a problem hiding this comment.
Just realized that we already discussed the IOG part
Member
|
Member
Pls re-request review when you are done
|
Member
|
New OP |
Instead of terminating IOGs with sinks, they are now terminated with dead buffers This way, the extra attribute that propagates through handshake -> hw -> python is no longer necessary
Collaborator
Author
|
I created the new dead buffer operation instead of using an attribute of the sink operation. I am now doing the merge so that the CI runs |
Member
|
Could you rebase the branch to main? |
Jiahui17
reviewed
May 11, 2026
| // consumed by sinks | ||
| bool syncOutput = false; | ||
|
|
||
| // Determines if the output is modelled as a dead buffer (i.e. accepts one |
Member
There was a problem hiding this comment.
the output or all outputs? Technically we can choose whether to have a single output or multiple outputs
| namespace { | ||
| // This function finds appropriate fork sent states for the consecutive tokens | ||
| // invariant: Given the IOG and a set of paths from a start buffer to an end | ||
| // buffer, it determines all forks for which: |
Member
There was a problem hiding this comment.
it determines the sent states of all forks?
| if (!iog.contains(forward)) { | ||
| continue; | ||
| } | ||
| Operation *next = forward.getUses().begin()->getOwner(); |
Member
There was a problem hiding this comment.
maybe we can shorten this by one forward.getUsers().back() (not super sure now..)?
| #include "mlir/IR/BuiltinOps.h" | ||
|
|
||
| namespace dynamatic { | ||
| IOGPathSet::IOGPathSet(const IOG &iog, Operation *startA, Operation *endA) |
Member
There was a problem hiding this comment.
remember to address the remark that I had earier (should this be a class method of IOG itself?)!
Jiahui17
reviewed
May 12, 2026
| // TODO: Handle LoadOp for MC slot | ||
| auto slots = loadOp.getInternalSlotStateNamers(); | ||
| auto *mcOp = loadOp.getAddressResult().getUses().begin()->getOwner(); | ||
| assert(mcOp); |
Member
There was a problem hiding this comment.
if (!mcOp) {
op->emitError(...);
llvm::report_fatal_error();
}| // 1. The start buffer is the copied slot of the fork | ||
| // 2. The fork is part of a path from start to end along the IOG | ||
| std::vector<EagerForkSentNamer> findCopiedSents(const IOG &iog, | ||
| const IOGPathSet &pathSet) { |
Member
There was a problem hiding this comment.
- The construction of IOGPathSet is actually essential to understanding how this algorithm works
- The struct IOGPathSet hides the info that pathSet.start == the start buffer
Jiahui17
approved these changes
May 13, 2026
Member
|
Good job, thanks! |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.