expected = Signal(width)
with m.Switch(points.as_sig()):
- # with m.Case(0b00):
- # comb += Assert(
- # out[0:24] == (data[0:24] << (shifter & 0x1f)) & 0xffffff)
+ 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:16] ==
- # (data[8:16] << (shifter)) & 0xffff)
+ 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)
+ 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)
module = ShifterDriver()
self.assertFormal(module, mode="bmc", depth=4)
def test_ilang(self):
- width = 32
- mwidth = 4
+ width = 24
+ mwidth = 3
gates = Signal(mwidth-1)
points = PartitionPoints()
step = int(width/mwidth)
shifter_masks = []
for i in range(len(intervals)):
max_bits = math.ceil(math.log2(width-intervals[i][0]))
+ sm_mask = Signal(shiftbits, name="sm_mask%d" % i)
if pwid-i != 0:
sm = ShifterMask(pwid-i, shiftbits,
max_bits, min_bits)
- setattr(m.submodules, "sm%d" % i, sm)
comb += sm.gates.eq(gates[i:pwid])
- mask = Signal(shiftbits, name="sm_mask%d" % i)
- comb += mask.eq(sm.mask)
- shifter_masks.append(mask)
+ 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
- shifter_masks.append((1<<min_bits)-1)
- print(m.submodules)
+ # this seems to fix it
+ comb += sm_mask.eq((1<<min_bits)-1)
+ if i != 0:
+ shifter_mask = Signal(shiftbits, name="shifter_mask%d" % i)
+ comb += shifter_mask.eq(Mux(gates[i-1],
+ sm_mask,
+ shifter_masks[i-1]))
+ shifter_masks.append(shifter_mask)
+ else:
+ shifter_masks.append(sm_mask)
for i, interval in enumerate(intervals):
s,e = interval