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..ca799e0cc --- /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" +