From a6a258fcbf4757aa031429636ef03afaf5b72d62 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Fri, 9 Jan 2026 14:45:58 +0100 Subject: [PATCH 1/2] spec: introduce SIGN template --- spec/book.typ | 1 + spec/sign.typ | 42 ++++++++++++++++++++++++++++++++++++++++++ spec/src/sign.toml | 42 ++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 85 insertions(+) create mode 100644 spec/sign.typ create mode 100644 spec/src/sign.toml diff --git a/spec/book.typ b/spec/book.typ index b194b7f70..2fd6d8767 100644 --- a/spec/book.typ +++ b/spec/book.typ @@ -10,6 +10,7 @@ ("memory.typ", [Memory argument], ), ("variables.typ", [Variables], ), ("is_bit.typ", [IS_BIT template], ), + ("sign.typ", [SIGN template], ), ("add.typ", [ADD/SUB template], ), ("decode.typ", [DECODE table], ), ("cpu.typ", [CPU chip], ), diff --git a/spec/sign.typ b/spec/sign.typ new file mode 100644 index 000000000..6f8993f53 --- /dev/null +++ b/spec/sign.typ @@ -0,0 +1,42 @@ +#import "/book.typ": book-page +#import "/src.typ": load_config, load_chip +#import "/chip.typ": render_chip_column_table, render_chip_assumptions, render_constraint_table + + +#let config = load_config() +#let chip = load_chip("src/sign.toml", config) +#show: book-page(chip.name) + +#let sign = raw(chip.name) + +#let highlighted_code(code) = { + box( + inset: (left: 4pt, right: 4pt), + outset: (top: 4pt, bottom: 4pt), + radius: 2pt, + fill: luma(230), + raw(code)) +} + +#sign is a constraint template that is used to extract a `Half`word's sign. + +== Interface +The #sign constraint template has the following interface: +#block(radius: 5pt, width: 100%, inset: 1.5em, fill: luma(230), raw("SIGN")) +It constrains that `sign` is set to `1` when both `X`'s most significant bit and `signed` are $1$, and $0$ otherwise. + +== Variables +The #sign template operates on three variables: +#render_chip_column_table(chip, config) + +== Assumptions +The #sign template operates on the following assumptions: +#render_chip_assumptions(chip, config) + +== 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. +This value is extracted in @sign:c:sign_if_signed. +If `X` is unsigned (i.e., $#`signed` = 0$), its sign is always $0$. +This is constrained by @sign:c:sign_if_unsigned. +#render_constraint_table(chip, config) diff --git a/spec/src/sign.toml b/spec/src/sign.toml new file mode 100644 index 000000000..81b5e8157 --- /dev/null +++ b/spec/src/sign.toml @@ -0,0 +1,42 @@ +name = "SIGN" + +[[variables.input]] +name = "X" +type = "Half" +desc = "Value for which to extract its sign." + +[[variables.input]] +name = "signed" +type = "Bit" +desc = "Whether `X` represents a signed value (1) or not (0)" + +[[variables.output]] +name = "sign" +type = "Bit" +desc = "Sign of `X`" + + +[[assumptions]] +desc = "`IS_HALF[X]`" + +[[assumptions]] +desc = "`IS_BIT`" + + +[[constraint_groups]] +name = "all" + +[[constraints.all]] +kind = "interaction" +tag = "MSB16" +input = ["X"] +output = "sign" +multiplicity = "signed" +ref = "sign:c:sign_if_signed" + +[[constraints.all]] +kind = "arith" +constraint = "$not#`signed` => #`sign` = 0$" +poly = ["*", ["not", "signed"], "sign"] +ref = "sign:c:sign_if_unsigned" + From cd5fb6f0cb36227f6950f6bfa22ae1ec4070ac22 Mon Sep 17 00:00:00 2001 From: Erik <159244975+erik-3milabs@users.noreply.github.com> Date: Tue, 3 Feb 2026 09:33:53 +0100 Subject: [PATCH 2/2] Update spec/src/sign.toml Co-authored-by: greptile-apps[bot] <165735046+greptile-apps[bot]@users.noreply.github.com> --- spec/src/sign.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spec/src/sign.toml b/spec/src/sign.toml index 81b5e8157..ca799e0cc 100644 --- a/spec/src/sign.toml +++ b/spec/src/sign.toml @@ -20,7 +20,7 @@ desc = "Sign of `X`" desc = "`IS_HALF[X]`" [[assumptions]] -desc = "`IS_BIT`" +desc = "`IS_BIT`" [[constraint_groups]]