+ expected = Signal(64)
+ rot = Signal(64)
+ m.d.comb += rot.eq(rotl32(dut.i.rs[:32], dut.i.rb[:5]))
+ m.d.comb += mask.start.eq(dut.fields.FormM.MB[:] + 32)
+ m.d.comb += mask.end.eq(dut.fields.FormM.ME[:] + 32)
+
+ # for rlwinm and rlwnm, ra is guaranteed to be 0, so that part of
+ # the expression turns into a no-op
+ m.d.comb += expected.eq((rot & mask.out) | (dut.i.ra & ~mask.out))
+ m.d.comb += Assert(dut.o.o.data == expected)
+ m.d.comb += Assert(dut.o.xer_ca.data == 0)
+
+ def _check_rlc64(self, m, dut):
+ m.d.comb += Assume(~dut.i.ctx.op.is_32bit)
+ # rldic and rldimi
+
+ # `rb` is always a 6-bit immediate
+ m.d.comb += Assume(dut.i.rb[6:] == 0)
+
+ m.submodules.mask = mask = Mask()
+ expected = Signal(64)
+ rot = Signal(64)
+ m.d.comb += rot.eq(rotl64(dut.i.rs, dut.i.rb[:6]))
+ mb = dut.fields.FormMD.mb[:]
+ m.d.comb += mask.start.eq(Cat(mb[1:6], mb[0]))
+ m.d.comb += mask.end.eq(63 - dut.i.rb[:6])
+
+ # for rldic, ra is guaranteed to be 0, so that part of
+ # the expression turns into a no-op
+ m.d.comb += expected.eq((rot & mask.out) | (dut.i.ra & ~mask.out))
+ m.d.comb += Assert(dut.o.o.data == expected)