spec: SIGN

spec/book.typ

@@ -10,6 +10,7 @@
     ("memory.typ", [Memory argument], <memory>),
     ("variables.typ", [Variables], <vars>),
     ("is_bit.typ", [IS_BIT template], <isbit>),
+    ("sign.typ", [SIGN template], <sign>),
     ("add.typ", [ADD/SUB template], <add>),
     ("decode.typ", [DECODE table], <decode>),
     ("cpu.typ", [CPU chip], <cpu>),

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<sign; X, signed>"))
+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)

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<signed>`"
+
+
+[[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"
+