Add partitioned right shift to part_shift_scalar

diff --git a/src/ieee754/part_shift/formal/proof_shift_scalar.py b/src/ieee754/part_shift/formal/proof_shift_scalar.py
index f76d063241319d01a3a241c809de7fec57e95005..35dd993ead2657300e085772bbbf245a7ae71e57 100644 (file)
--- a/src/ieee754/part_shift/formal/proof_shift_scalar.py
+++ b/src/ieee754/part_shift/formal/proof_shift_scalar.py
@@ -90,6 +90,32 @@ class ShifterDriver(Elaboratable):
                                 (data[8:16] << (shifter & 0x7)) & 0xff)
                     comb += Assert(out[16:24] ==
                                 (data[16:24] << (shifter & 0x7)) & 0xff)
+        with m.Else():
+            with m.Switch(points.as_sig()):
+                with m.Case(0b00):
+                    comb += Assert(
+                        out[0:24] == (data[0:24] >> (shifter & 0x1f)) &
+                        0xffffff)
+
+                with m.Case(0b01):
+                    comb += Assert(out[0:8] ==
+                                (data[0:8] >> (shifter & 0x7)) & 0xFF)
+                    comb += Assert(out[8:24] ==
+                                (data[8:24] >> (shifter & 0xf)) & 0xffff)
+
+                with m.Case(0b10):
+                    comb += Assert(out[16:24] ==
+                                (data[16:24] >> (shifter & 0x7)) & 0xff)
+                    comb += Assert(out[0:16] ==
+                                (data[0:16] >> (shifter & 0xf)) & 0xffff)
+
+                with m.Case(0b11):
+                    comb += Assert(out[0:8] ==
+                                (data[0:8] >> (shifter & 0x7)) & 0xFF)
+                    comb += Assert(out[8:16] ==
+                                (data[8:16] >> (shifter & 0x7)) & 0xff)
+                    comb += Assert(out[16:24] ==
+                                (data[16:24] >> (shifter & 0x7)) & 0xff)
         return m
 
 class PartitionedScalarShiftTestCase(FHDLTestCase):

diff --git a/src/ieee754/part_shift/part_shift_scalar.py b/src/ieee754/part_shift/part_shift_scalar.py
index 2a14fb5da608fef3fce2e39760fb935ede0f9f19..79fc3e69cfe3193b775bc38feb6b821c9de75748 100644 (file)
--- a/src/ieee754/part_shift/part_shift_scalar.py
+++ b/src/ieee754/part_shift/part_shift_scalar.py
@@ -52,6 +52,10 @@ class PartitionedScalarShift(Elaboratable):
         m.submodules.out_br = out_br = GatedBitReverse(self.data.width)
         comb += out_br.reverse_en.eq(self.bitrev)
         comb += self.output.eq(out_br.output)
+
+        m.submodules.gate_br = gate_br = GatedBitReverse(pwid)
+        comb += gate_br.data.eq(gates)
+        comb += gate_br.reverse_en.eq(self.bitrev)
         start = 0
         for i in range(len(keys)):
             end = keys[i]
@@ -68,7 +72,7 @@ class PartitionedScalarShift(Elaboratable):
             if pwid-i != 0:
                 sm = ShifterMask(pwid-i, shiftbits,
                                  max_bits, min_bits)
-                comb += sm.gates.eq(gates[i:pwid])
+                comb += sm.gates.eq(gate_br.output[i:pwid])
                 comb += sm_mask.eq(sm.mask)
                 setattr(m.submodules, "sm%d" % i, sm)
             else: # having a 0 width signal seems to give the proof issues
@@ -77,7 +81,7 @@ class PartitionedScalarShift(Elaboratable):
             if i != 0:
                 shifter_mask = Signal(shiftbits, name="shifter_mask%d" % i,
                                       reset_less=True)
-                comb += shifter_mask.eq(Mux(gates[i-1],
+                comb += shifter_mask.eq(Mux(gate_br.output[i-1],
                                          sm_mask,
                                          shifter_masks[i-1]))
                 shifter_masks.append(shifter_mask)
@@ -99,7 +103,7 @@ class PartitionedScalarShift(Elaboratable):
             if i == 0:
                 intermed = shiftparts[i]
             else:
-                intermed = shiftparts[i] | Mux(gates[i-1], 0, prev)
+                intermed = shiftparts[i] | Mux(gate_br.output[i-1], 0, prev)
             comb += outputs[i].eq(intermed[start:end])
             prev = intermed