From 03a266bdb9d4bd0ec012ad7e4fd44eef29acf3af Mon Sep 17 00:00:00 2001 From: Michael Nolan Date: Wed, 26 Feb 2020 09:08:00 -0500 Subject: [PATCH] Add partitioned right shift to part_shift_scalar --- .../part_shift/formal/proof_shift_scalar.py | 26 +++++++++++++++++++ src/ieee754/part_shift/part_shift_scalar.py | 10 ++++--- 2 files changed, 33 insertions(+), 3 deletions(-) diff --git a/src/ieee754/part_shift/formal/proof_shift_scalar.py b/src/ieee754/part_shift/formal/proof_shift_scalar.py index f76d0632..35dd993e 100644 --- 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 2a14fb5d..79fc3e69 100644 --- 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 -- 2.30.2