spec: rv2 as DWordBL in CPU due to STORE#297
Closed
RobinJadoul wants to merge 2 commits into
Closed
Conversation
RobinJadoul
added
bug
RobinJadoul
force-pushed
the
spec/arr-expr
branch
from
f8bdacf to
a25ff49
Compare
RobinJadoul
force-pushed
the
spec/cpu-store-rv2-bytes
branch
2 times, most recently
from
8c27a0f to
f980217
Compare
RobinJadoul
force-pushed
the
spec/arr-expr
branch
from
a25ff49 to
3242100
Compare
This is a (temporary, for now) change to the CPU to have `rv2` available as `DWordBL` so that the `MEMW` interaction on the `STORE` path can work correctly. It already builds on top of the array expressions to clean up the signatures for all MEMW calls from the CPU along the way.
RobinJadoul
force-pushed
the
spec/arr-expr
branch
from
3242100 to
7e92332
Compare
RobinJadoul
force-pushed
the
spec/cpu-store-rv2-bytes
branch
from
96ab5fa to
293dcb8
Compare
erik-3milabs
reviewed
Feb 9, 2026
Collaborator
erik-3milabs
left a comment
erik-3milabs
left a comment
There was a problem hiding this comment.
there are some changes in here that are not expected given the title of the PR...
Comment on lines
+656
to
+657
| input = [1, ["*", 2, "rs1"], ["arr", ["idx", ["cast", "rv1", "DWordWL"], 0], ["idx", "rv1", 2], 0, 0, 0, 0, 0, 0], ["+", "timestamp", ["cast", 0, "DWordWL"]], 1, 0, 0] | ||
| output = ["arr", ["idx", ["cast", "rv1", "DWordWL"], 0], ["idx", "rv1", 2], 0, 0, 0, 0, 0, 0] |
Collaborator
There was a problem hiding this comment.
While I agree that pushing rv1 into the array this way is correct, I'd be inclined to apply cast to the second appearance of "rv1" in either array as well, just to make it easier to read.
Comment on lines
+759
to
+765
| constraint = "$#`arg2[:4]` = (1 - #`STORE` - #`LOAD`) dot #`rv2[:4]` + (1 - #`BEQ` - #`BLT`) dot #`imm[0]`$" | ||
| poly = ["-", ["idx", ["cast", "arg2", "DWordWL"], 0], ["*", ["-", 1, "STORE", "LOAD"], ["idx", ["cast", "rv2", "DWordWL"], 0]], ["*", ["-", 1, "BEQ", "BLT"], ["idx", "imm", 0]]] | ||
|
|
||
| [[constraints.ext]] | ||
| kind = "arith" | ||
| constraint = "$#`arg2[4:]` = (1 - #`STORE` - #`LOAD`) dot ((1 - #`word_instr`) dot #`rv2[2]` + #`signed` dot #`arg2_sign_bit` dot (2^(32) - 1)) + (1 - #`BEQ` - #`BLT`) dot #`imm[1]`$" | ||
| poly = ["-", ["idx", ["cast", "arg2", "DWordWL"], 1], ["*", ["-", 1, "STORE", "LOAD"], ["not", "word_instr"], ["idx", "rv2", 2]], ["*", ["-", 1, "STORE", "LOAD"], "signed", "arg2_sign_bit", ["-", ["^", 2, 32], 1]], ["*", ["-", 1, "BEQ", "BLT"], ["idx", "imm", 1]]] | ||
| constraint = "$#`arg2[4:]` = (1 - #`STORE` - #`LOAD`) dot ((1 - #`word_instr`) dot #`rv2[4:]` + #`signed` dot #`arg2_sign_bit` dot (2^(32) - 1)) + (1 - #`BEQ` - #`BLT`) dot #`imm[1]`$" | ||
| poly = ["-", ["idx", ["cast", "arg2", "DWordWL"], 1], ["*", ["-", 1, "STORE", "LOAD"], ["not", "word_instr"], ["idx", ["cast", "rv2", "DWordWL"], 1]], ["*", ["-", 1, "STORE", "LOAD"], "signed", "arg2_sign_bit", ["-", ["^", 2, 32], 1]], ["*", ["-", 1, "BEQ", "BLT"], ["idx", "imm", 1]]] |
Collaborator
There was a problem hiding this comment.
I believe we decided to move away from slicing. Shall we use this opportunity to remove the slices in these two constraints?
Collaborator
Author
There was a problem hiding this comment.
I mostly mind them in the "formal" polys, less so in the descriptive constraint
Collaborator
|
I take it this can be closed, as it is superseded by #308, right? |
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.
This is a (temporary, for now) change to the CPU to have
rv2available asDWordBLso that theMEMWinteraction on theSTOREpath can work correctly.It already builds on top of the array expressions to clean up the signatures for all MEMW calls from the CPU along the way.