Exercise 4

Author: RobertBaruch

04_signs.md

@@ -0,0 +1,142 @@
+# Exercise 4: Signs
+
+## What you'll do, part 1:
+
+Write a module that takes a 64-bit signed number, and negates it in three ways:
+
+* Invert and add 1.
+* Directly negate it.
+* Starting from the least significant bit, copy up to and including the first 1, then invert the remaining bits.
+
+That last one seems a bit strange, but it works like this (using 8-bit numbers):
+
+Given as input `11101000`, copy up to and including the first 1 (`1000`), then invert the remaining bits: `00011000`. Compare this to inverting first (`00010111`) and adding one: `00011000`. Hey, at least the last technique doesn't require an adder.
+
+Formally verify that:
+
+* These three techniques always result in the same number.
+* The most significant bit of the number being set always means it is less than 0.
+
+When you complete this exercise, think about how long the formal verification engine took to run. Formal verification is not a brute-force process. If it were, then even at one check per nanosecond, it would take over 500 years to verify every 64-bit number. Rather, the formal verification engine is a solver, technically an [SMT solver](https://en.wikipedia.org/wiki/Satisfiability_modulo_theories), and every built-in theory such a solver has enables the solver to shortcut some brute-force approaches. The solver we have configured to use in the `[engines]` section of the sby file is the [Z3 solver](https://en.wikipedia.org/wiki/Z3_Theorem_Prover), which has overall good performance.
+
+### Signedness
+
+Up until now, when you've created a Signal, you've created unsigned signals. This means that arithmetic and comparisons on them are unsigned. So, the 4-bit unsigned number `1000` is always *greater* than the 4-bit unsigned number `0111`.
+
+However, in 2's complement, `1000` is -8 while `0111` is 7, which means that if these 4-bit signals were treated as *signed*, `1000` should be *less* than `0111`.
+
+```python
+x = Signal(signed(4))
+y = Signal(signed(4))
+m.d.comb += [
+    x.eq(0b1000),
+    y.eq(0b0111),
+    Assert(x < y),
+]
+```
+
+To treat an unsigned (or signed) signal as signed:
+
+```python
+x = Signal(4)
+y = Signal(4)
+m.d.comb += [
+    x.eq(0b1000),
+    y.eq(0b0111),
+    Assert(x.as_signed() < y.as_signed()),
+]
+```
+
+There is also a corresponding `as_unsigned()` function to convert a signed (or unsigned) signal to an unsigned signal.
+
+Negating a signal always results in a signed signal, regardless of whether the input signal is signed or unsigned:
+
+```python
+x = Signal(4)
+y = Signal(4)
+m.d.comb += [
+    x.eq(0b0011),
+    y.eq(0b1101),
+    Assert(y > x),
+    Assert(-x < x),
+]
+```
+
+Equality, on the other hand, does not take into account signedness. It is bit-for-bit equality:
+
+```python
+x = Signal(4)
+y = Signal(4)
+m.d.comb += [
+    x.eq(0b0011),
+    y.eq(0b1101),
+    Assert(y > x),
+    Assert(-x == y),
+]
+```
+
+All arithmetic operations that apply to signed signals are signed. For example, right shifts do take into account signedness, and the result is the same signedness as the input:
+
+```python
+x = Signal(4)
+y = Signal(signed(4))
+m.d.comb += [
+    x.eq(0b1000),
+    y.eq(0b1000),
+    Assert((x >> 1) == 0b0100),
+    Assert((y >> 1) == 0b1100),
+]
+```
+
+### Library: priority encoder
+
+A *priority encoder* is a circuit that takes an N-bit input and outputs the position of the first set bit, where "first" could mean most significant or least significant. nMigen has a coding library with a PriorityEncoder module built in, which outputs the position of the first least significant bit set.
+
+```python
+from nmigen.lib.coding import PriorityEncoder
+
+enc = PriorityEncoder(width=8)
+input = Signal(8)
+output = Signal(3)
+bit_set = Signal()
+
+m.d.comb += [
+    enc.i.eq(input),
+    output.eq(enc.o),
+    bit_set.eq(~enc.n),  # n really means that the input is zero
+]
+```
+
+For example, the input `0101000` will result in the output being 3 and bit_set being high.
+
+### Limitations on slices
+
+Slices such as `x[1:4]` require integers as indices, not signals. So you can't have:
+
+```python
+x = Signal(8)
+y = Signal(3)
+z = x[y]  # Results in an error
+```
+
+You can achieve the same effect using bit tricks. For example, `1 << y` gives you a 1 in the yth bit position. `(x >> y) & 1` gives you the yth bit of x.
+
+What does `(-1 << y) & x` give you?
+
+-----
+
+Interested in more bit-manipulation tricks? Check out Knuth's The Art of Computer Programming, Volume 4A, chapter 7.1.3 (Bitwise Tricks and Techniques). Hacker's Delight also contains copious bit manipulation fun.
+
+-----
+
+## What you'll do, part 2:
+
+Suppose you have a chip that can compare two 16-bit numbers, but only as unsigned numbers. It outputs whether the first is less than the second. Write such a module.
+
+Now write another module that uses the above module, and based only the most significant bits (i.e. the sign bits) of the original inputs, and the output of the unsigned comparator, outputs whether the first is less than the second, treated as *signed* numbers. The idea here is that you're limited to an unsigned comparator, and need a signed comparator.
+
+Formally verify that the output of your module is correct, by using `as_signed()`.
+
+## Stumped?
+
+The answers are in [`answers/e04_negate.py`](answers/e04_negate.py) and [`answers/e04_signed_compare.py`](answers/e04_signed_compare.py)

README.md

@@ -6,3 +6,4 @@ Work in progress!
 * [01 - Counting coin: basic concepts](01_input.md)
 * [02 - The day after: more if, and switch-case](02_switch.md)
 * [03 - Life finds a way: parts of signals](03_parts.md)
+* [04 - Signs: signed signals](04_signs.md)

answers/e04_negate.py

@@ -0,0 +1,63 @@
+# Disable pylint's "your name is too short" warning.
+# pylint: disable=C0103
+from typing import List, Tuple
+
+from nmigen import Signal, Module, Elaboratable
+from nmigen.build import Platform
+from nmigen.asserts import Assume, Assert, Cover
+from nmigen.lib.coding import PriorityEncoder
+
+from util import main
+
+
+class Negate(Elaboratable):
+    """Logic for the Negate module."""
+
+    def __init__(self):
+        self.input = Signal(64)
+        self.output1 = Signal(64)  # invert and add 1
+        self.output2 = Signal(64)  # direct negation
+        self.output3 = Signal(64)  # using priority encoder
+
+    def elaborate(self, _: Platform) -> Module:
+        """Implements the logic for the Negate module."""
+        m = Module()
+        m.submodules.enc = enc = PriorityEncoder(64)
+
+        m.d.comb += self.output1.eq(~self.input + 1)
+        m.d.comb += self.output2.eq(-self.input)
+        m.d.comb += enc.i.eq(self.input)
+
+        with m.If(enc.n):
+            m.d.comb += self.output3.eq(0)
+        with m.Else():
+            neg1 = Signal(64)
+            m.d.comb += neg1.eq(-1)
+            #          n
+            # 1111111111000000  # mask = -1 << n
+            # 0000000000111111  # lower_mask = ~(-1 << n)
+            # 0000000001000000  # 1 << n
+            mask = Signal(64)
+            m.d.comb += mask.eq(neg1 << enc.o)
+            lower_mask = ~mask
+            m.d.comb += self.output3.eq((~self.input & mask)
+                                        | (self.input & lower_mask)
+                                        | (1 << enc.o))
+
+        return m
+
+    @classmethod
+    def formal(cls) -> Tuple[Module, List[Signal]]:
+        """Formal verification for the Negate module."""
+        m = Module()
+        m.submodules.c = c = cls()
+
+        m.d.comb += Assert(c.output1 == c.output2)
+        m.d.comb += Assert(c.output2 == c.output3)
+        m.d.comb += Assert(c.output1[63] == (c.output1.as_signed() < 0))
+
+        return m, [c.input]
+
+
+if __name__ == "__main__":
+    main(Negate)

answers/e04_negate.sby

@@ -0,0 +1,33 @@
+[tasks]
+cover
+bmc
+
+[options]
+bmc: mode bmc
+cover: mode cover
+depth 1
+multiclock on
+
+[engines]
+cover: smtbmc z3
+bmc: smtbmc z3
+
+[script]
+read_verilog <<END
+module \$dff (CLK, D, Q);
+  parameter WIDTH = 0;
+  parameter CLK_POLARITY = 1'b1;
+  input CLK;
+  input [WIDTH-1:0] D;
+  output reg [WIDTH-1:0] Q;
+  \$ff #(.WIDTH(WIDTH)) _TECHMAP_REPLACE_ (.D(D),.Q(Q));
+endmodule
+END
+design -stash dff2ff
+read_ilang toplevel.il
+proc
+techmap -map %dff2ff top/w:clk %co
+prep -top top
+
+[files]
+toplevel.il

answers/e04_signed_compare.py

@@ -0,0 +1,78 @@
+# Disable pylint's "your name is too short" warning.
+# pylint: disable=C0103
+from typing import List, Tuple
+
+from nmigen import Signal, Module, Elaboratable
+from nmigen.build import Platform
+from nmigen.asserts import Assume, Assert, Cover
+from nmigen.lib.coding import PriorityEncoder
+
+from util import main
+
+
+class UnsignedComparator(Elaboratable):
+    """Logic for the UnsignedComparator module."""
+
+    def __init__(self):
+        self.a = Signal(16)
+        self.b = Signal(16)
+        self.lt = Signal()
+
+    def elaborate(self, _: Platform) -> Module:
+        """Implements the logic for the UnsignedComparator module."""
+        m = Module()
+
+        m.d.comb += self.lt.eq(self.a < self.b)
+
+        return m
+
+
+class SignedComparator(Elaboratable):
+    """Logic for the SignedComparator module."""
+
+    def __init__(self):
+        self.a = Signal(16)
+        self.b = Signal(16)
+        self.lt = Signal()
+
+    def elaborate(self, _: Platform) -> Module:
+        """Implements the logic for the SignedComparator module."""
+        m = Module()
+        m.submodules.ucmp = ucmp = UnsignedComparator()
+
+        ult = Signal()  # Unsigned less than
+
+        # Hook up the submodule
+        m.d.comb += [
+            ucmp.a.eq(self.a),
+            ucmp.b.eq(self.b),
+            ult.eq(ucmp.lt),
+        ]
+
+        is_a_neg = self.a[15]
+        is_b_neg = self.b[15]
+
+        with m.If(~is_a_neg & ~is_b_neg):
+            m.d.comb += self.lt.eq(ult)
+        with m.Elif(is_a_neg & ~is_b_neg):
+            m.d.comb += self.lt.eq(1)
+        with m.Elif(~is_a_neg & is_b_neg):
+            m.d.comb += self.lt.eq(0)
+        with m.Else():
+            m.d.comb += self.lt.eq(ult)
+
+        return m
+
+    @classmethod
+    def formal(cls) -> Tuple[Module, List[Signal]]:
+        """Formal verification for the SignedComparator module."""
+        m = Module()
+        m.submodules.c = c = cls()
+
+        m.d.comb += Assert(c.lt == (c.a.as_signed() < c.b.as_signed()))
+
+        return m, [c.a, c.b]
+
+
+if __name__ == "__main__":
+    main(SignedComparator)

answers/e04_signed_compare.sby

@@ -0,0 +1,33 @@
+[tasks]
+cover
+bmc
+
+[options]
+bmc: mode bmc
+cover: mode cover
+depth 1
+multiclock on
+
+[engines]
+cover: smtbmc z3
+bmc: smtbmc z3
+
+[script]
+read_verilog <<END
+module \$dff (CLK, D, Q);
+  parameter WIDTH = 0;
+  parameter CLK_POLARITY = 1'b1;
+  input CLK;
+  input [WIDTH-1:0] D;
+  output reg [WIDTH-1:0] Q;
+  \$ff #(.WIDTH(WIDTH)) _TECHMAP_REPLACE_ (.D(D),.Q(Q));
+endmodule
+END
+design -stash dff2ff
+read_ilang toplevel.il
+proc
+techmap -map %dff2ff top/w:clk %co
+prep -top top
+
+[files]
+toplevel.il