Skip to content

spec: Fix CPU sign bit constraints for word_instr #435

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

Merged
RobinJadoul merged 2 commits into from
Mar 25, 2026
Merged

spec: Fix CPU sign bit constraints for word_instr #435

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
a4b63da
spec: Fix CPU sign bit constraints for `word_instr`
RobinJadoul Mar 17, 2026
fc824ca
naming and assumptions
RobinJadoul Mar 24, 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
2 changes: 2 additions & 0 deletions spec/sign.typ
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,8 @@ The #sign template operates on three variables:
The #sign template operates on the following assumptions:
#render_chip_assumptions(chip, config)

If `sign` is set to $1$, `X` will be range-checked to be a halfword, and hence proving may fail if this is not ensured.

= Constraints
It takes only two constraints to compute the `sign` of `X`, given whether `X` represents a `signed` value or not.
When $#`signed` = 1$, the sign of `X` is equal to its most significant bit.
Expand Down
57 changes: 24 additions & 33 deletions spec/src/cpu.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -234,9 +234,9 @@ desc = "The value of register `rs2`"
pad = 0

[[variables.auxiliary]]
name = "rv1_sign_bit"
name = "rv1_ext_bit"
type = "Bit"
desc = "The sign bit of `rv1` if seen as a 32-bit word"
desc = "The sign bit of `rv1` if seen as a 32-bit word, used for sign extension with `word_instr`"
pad = 0

[[variables.auxiliary]]
Expand All @@ -246,9 +246,9 @@ desc = "The extended version of `rv1`, depending on `word_instr`"
pad = 0

[[variables.auxiliary]]
name = "arg2_sign_bit"
name = "rv2_ext_bit"
type = "Bit"
desc = "The sign bit of `arg2` if seen as a 32-bit word"
desc = "The sign bit of `rv2` if seen as a 32-bit word, used for sign extension with `word_instr`"
pad = 0

[[variables.auxiliary]]
Expand All @@ -258,9 +258,9 @@ desc = "A multiplexed version of `rv2` and `imm`, to be used as second argument
pad = 0

[[variables.auxiliary]]
name = "res_sign_bit"
name = "res_ext_bit"
type = "Bit"
desc = "The sign bit of `res`, if seen as a 32-bit word"
desc = "The sign bit of `res`, if seen as a 32-bit word, used for sign extension with `word_instr`"
pad = 0

[[variables.auxiliary]]
Expand Down Expand Up @@ -722,16 +722,10 @@ name = "ext"
prefix = "E"

[[constraints.ext]]
kind = "arith"
constraint = "$(#`rv1_sign_bit` or #`arg2_sign_bit` or #`res_sign_bit`) => #`word_instr`$"
poly = ["*", ["+", "rv1_sign_bit", "arg2_sign_bit", "res_sign_bit"], ["not", "word_instr"]]

[[constraints.ext]]
kind = "interaction"
tag = "MSB16"
input = [["idx", "rv1", 1]]
output = "rv1_sign_bit"
multiplicity = "word_instr"
kind = "template"
tag = "SIGN"
input = [["idx", "rv1", 1], "word_instr"]
output = "rv1_ext_bit"

[[constraints.ext]]
kind = "arith"
Expand All @@ -740,15 +734,14 @@ poly = ["-", ["idx", ["cast", "arg1", "DWordWL"], 0], ["idx", ["cast", "rv1", "D

[[constraints.ext]]
kind = "arith"
constraint = "$#`arg1[4:]` = #`rv1[2]` dot (1 - #`word_instr`) + (2^(32) - 1) dot #`rv1_sign_bit` dot #`signed`$"
poly = ["-", ["idx", ["cast", "arg1", "DWordWL"], 1], ["*", ["not", "word_instr"], ["idx", "rv1", 2]], ["*", "signed", "rv1_sign_bit", ["-", ["^", 2, 32], 1]]]
constraint = "$#`arg1[4:]` = #`rv1[2]` dot (1 - #`word_instr`) + (2^(32) - 1) dot #`rv1_ext_bit` dot #`signed`$"
poly = ["-", ["idx", ["cast", "arg1", "DWordWL"], 1], ["*", ["not", "word_instr"], ["idx", "rv1", 2]], ["*", "signed", "rv1_ext_bit", ["-", ["^", 2, 32], 1]]]

[[constraints.ext]]
kind = "interaction"
tag = "MSB16"
input = [["idx", "rv2", 1]]
output = "arg2_sign_bit"
multiplicity = "word_instr"
Copy link
Copy Markdown
Collaborator

@erik-3milabs erik-3milabs Mar 18, 2026

Choose a reason for hiding this comment

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

I believe this should have arg2 rather than rv2 as input.

The two things suggesting this to me:

  1. the name mismatch between the input (rv2) and the output (arg2_sign_bit)
  2. The SIGN template assumes IS_HALF[rv2[1]]. While CE61 + CR33 does this for some cases, it does not cover all.

Copy link
Copy Markdown
Collaborator

@erik-3milabs erik-3milabs Mar 19, 2026

Choose a reason for hiding this comment

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

Having another look at the constraints, I believe that the above is not actually correct. Perhaps renaming arg2_sign_bit to rv2_sign_bit would be a better solution.

Copy link
Copy Markdown
Collaborator Author

@RobinJadoul RobinJadoul Mar 24, 2026

Choose a reason for hiding this comment

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

Hmm, I think that may even be more generally a problem, that rv2 isn't always properly range checked (and maybe rv1 too)
Though the range check would have to be on arg{1,2} for most uses, it could be dangerous

Copy link
Copy Markdown
Collaborator Author

@RobinJadoul RobinJadoul Mar 24, 2026

Choose a reason for hiding this comment

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

Double checked that the range checks are fine; since rv1 and rv2 are just bridging between range-checked memory and range-checked arg1 and arg2

kind = "template"
tag = "SIGN"
input = [["idx", "rv2", 1], "word_instr"]
output = "rv2_ext_bit"

[[constraints.ext]]
kind = "arith"
Expand All @@ -757,15 +750,14 @@ poly = ["-", ["idx", ["cast", "arg2", "DWordWL"], 0], ["*", ["not", "LOAD"], ["i

[[constraints.ext]]
kind = "arith"
constraint = "$#`arg2[4:]` = (1 - #`LOAD`) dot ((1 - #`word_instr`) dot #`rv2[2]` + #`signed` dot #`arg2_sign_bit` dot (2^(32) - 1)) + (1 - #`BEQ` - #`BLT` - #`STORE`) dot #`imm[1]`$"
poly = ["-", ["idx", ["cast", "arg2", "DWordWL"], 1], ["*", ["not", "LOAD"], ["not", "word_instr"], ["idx", "rv2", 2]], ["*", ["not", "LOAD"], "signed", "arg2_sign_bit", ["-", ["^", 2, 32], 1]], ["*", ["-", 1, "BEQ", "BLT", "STORE"], ["idx", "imm", 1]]]
constraint = "$#`arg2[4:]` = (1 - #`LOAD`) dot ((1 - #`word_instr`) dot #`rv2[2]` + #`signed` dot #`rv2_ext_bit` dot (2^(32) - 1)) + (1 - #`BEQ` - #`BLT` - #`STORE`) dot #`imm[1]`$"
poly = ["-", ["idx", ["cast", "arg2", "DWordWL"], 1], ["*", ["not", "LOAD"], ["not", "word_instr"], ["idx", "rv2", 2]], ["*", ["not", "LOAD"], "signed", "rv2_ext_bit", ["-", ["^", 2, 32], 1]], ["*", ["-", 1, "BEQ", "BLT", "STORE"], ["idx", "imm", 1]]]

[[constraints.ext]]
kind = "interaction"
tag = "MSB8"
input = [["idx", "res", 3]]
output = "res_sign_bit"
multiplicity = "word_instr"
kind = "template"
tag = "SIGN"
input = [["idx", ["cast", "res", "DWordHL"], 1], "word_instr"]
output = "res_ext_bit"

[[constraints.ext]]
kind = "arith"
Expand All @@ -774,10 +766,9 @@ poly = ["*", ["not", "LOAD"], ["-", ["idx", "rvd", 0], ["idx", ["cast", "res", "

[[constraints.ext]]
kind = "arith"
constraint = "$#`!LOAD` => #`rvd[1]` = (1 - #`word_instr`) dot #`res[4:]` + #`res_sign_bit` dot (2^(32) - 1)$"
constraint = "$#`!LOAD` => #`rvd[1]` = (1 - #`word_instr`) dot #`res[4:]` + #`res_ext_bit` dot (2^(32) - 1)$"
desc = "_Sign_ extend the output if it wasn't a `LOAD`. Only `LOAD` has both `write_register = 1` and `rvd ≠ res`. `LOAD` and `word_instr` are disjoint"
poly = ["*", ["not", "LOAD"], ["-", ["idx", "rvd", 1], ["*", ["not", "word_instr"], ["idx", ["cast", "res", "DWordWL"], 1]], ["*", "res_sign_bit", ["-", ["^", 2, 32], 1]]]]

poly = ["*", ["not", "LOAD"], ["-", ["idx", "rvd", 1], ["*", ["not", "word_instr"], ["idx", ["cast", "res", "DWordWL"], 1]], ["*", "res_ext_bit", ["-", ["^", 2, 32], 1]]]]


[[constraint_groups]]
Expand Down
3 changes: 0 additions & 3 deletions spec/src/sign.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,9 +16,6 @@ type = "Bit"
desc = "Sign of `X`"


[[assumptions]]
desc = "`IS_HALF[X]`"

[[assumptions]]
desc = "`IS_BIT<signed>`"

Expand Down
Loading