* https://bugs.libre-soc.org/show_bug.cgi?id=340
"""
+import unittest
import enum
-from shutil import which
from nmigen import (Module, Signal, Elaboratable, Mux, Cat, Repl,
- signed, Array, Const, Value, unsigned)
-from nmigen.asserts import Assert, AnyConst, Assume, Cover
+ signed, Const, unsigned)
+from nmigen.asserts import Assert, AnyConst, Assume
from nmutil.formaltest import FHDLTestCase
from nmutil.sim_util import do_sim
from nmigen.sim import Delay
from soc.fu.shift_rot.main_stage import ShiftRotMainStage
-from soc.fu.shift_rot.rotator import right_mask, left_mask
from soc.fu.shift_rot.pipe_data import ShiftRotPipeSpec
-from soc.fu.shift_rot.sr_input_record import CompSROpSubset
from openpower.decoder.power_enums import MicrOp
-from openpower.consts import field
-
-import unittest
-from nmutil.extend import exts
@enum.unique
return m
- # all following code in elaborate is kept for ease of reference, to be
- # deleted once this proof is completed.
-
- # convenience variables
- rs = dut.i.rs # register to shift
- b = dut.i.rb # register containing amount to shift by
- ra = dut.i.a # source register if masking is to be done
- carry_in = dut.i.xer_ca[0]
- carry_in32 = dut.i.xer_ca[1]
- carry_out = dut.o.xer_ca
- o = dut.o.o.data
- print("fields", rec.fields)
- itype = rec.insn_type
-
- # instruction fields
- m_fields = dut.fields.FormM
- md_fields = dut.fields.FormMD
-
- # setup random inputs
- comb += rs.eq(AnyConst(64))
- comb += ra.eq(AnyConst(64))
- comb += b.eq(AnyConst(64))
- comb += carry_in.eq(AnyConst(1))
- comb += carry_in32.eq(AnyConst(1))
-
- # copy operation
- comb += dut.i.ctx.op.eq(rec)
-
- # check that the operation (op) is passed through (and muxid)
- comb += Assert(dut.o.ctx.op == dut.i.ctx.op)
- comb += Assert(dut.o.ctx.muxid == dut.i.ctx.muxid)
-
- # signed and signed/32 versions of input rs
- a_signed = Signal(signed(64))
- a_signed_32 = Signal(signed(32))
- comb += a_signed.eq(rs)
- comb += a_signed_32.eq(rs[0:32])
-
- # masks: start-left
- mb = Signal(7, reset_less=True)
- ml = Signal(64, reset_less=True)
-
- # clear left?
- with m.If((itype == MicrOp.OP_RLC) | (itype == MicrOp.OP_RLCL)):
- with m.If(rec.is_32bit):
- comb += mb.eq(m_fields.MB[:])
- with m.Else():
- comb += mb.eq(md_fields.mb[:])
- with m.Else():
- with m.If(rec.is_32bit):
- comb += mb.eq(b[0:6])
- with m.Else():
- comb += mb.eq(b+32)
- comb += ml.eq(left_mask(m, mb))
-
- # masks: end-right
- me = Signal(7, reset_less=True)
- mr = Signal(64, reset_less=True)
-
- # clear right?
- with m.If((itype == MicrOp.OP_RLC) | (itype == MicrOp.OP_RLCR)):
- with m.If(rec.is_32bit):
- comb += me.eq(m_fields.ME[:])
- with m.Else():
- comb += me.eq(md_fields.me[:])
- with m.Else():
- with m.If(rec.is_32bit):
- comb += me.eq(b[0:6])
- with m.Else():
- comb += me.eq(63-b)
- comb += mr.eq(right_mask(m, me))
-
- # must check Data.ok
- o_ok = Signal()
- comb += o_ok.eq(1)
-
- # main assertion of arithmetic operations
- with m.Switch(itype):
-
- # left-shift: 64/32-bit
- with m.Case(MicrOp.OP_SHL):
- comb += Assume(ra == 0)
- with m.If(rec.is_32bit):
- comb += Assert(o[0:32] == ((rs << b[0:6]) & 0xffffffff))
- comb += Assert(o[32:64] == 0)
- with m.Else():
- comb += Assert(o == ((rs << b[0:7]) & ((1 << 64)-1)))
-
- # right-shift: 64/32-bit / signed
- with m.Case(MicrOp.OP_SHR):
- comb += Assume(ra == 0)
- with m.If(~rec.is_signed):
- with m.If(rec.is_32bit):
- comb += Assert(o[0:32] == (rs[0:32] >> b[0:6]))
- comb += Assert(o[32:64] == 0)
- with m.Else():
- comb += Assert(o == (rs >> b[0:7]))
- with m.Else():
- with m.If(rec.is_32bit):
- comb += Assert(o[0:32] == (a_signed_32 >> b[0:6]))
- comb += Assert(o[32:64] == Repl(rs[31], 32))
- with m.Else():
- comb += Assert(o == (a_signed >> b[0:7]))
-
- # extswsli: 32/64-bit moded
- with m.Case(MicrOp.OP_EXTSWSLI):
- comb += Assume(ra == 0)
- with m.If(rec.is_32bit):
- comb += Assert(o[0:32] == ((rs << b[0:6]) & 0xffffffff))
- comb += Assert(o[32:64] == 0)
- with m.Else():
- # sign-extend to 64 bit
- a_s = Signal(64, reset_less=True)
- comb += a_s.eq(exts(rs, 32, 64))
- comb += Assert(o == ((a_s << b[0:7]) & ((1 << 64)-1)))
-
- # rlwinm, rlwnm, rlwimi
- # *CAN* these even be 64-bit capable? I don't think they are.
- with m.Case(MicrOp.OP_RLC):
- comb += Assume(ra == 0)
- comb += Assume(rec.is_32bit)
-
- # Duplicate some signals so that they're much easier to find
- # in gtkwave.
- # Pro-tip: when debugging, factor out expressions into
- # explicitly named
- # signals, and search using a unique grep-tag (RLC in my case).
- # After
- # debugging, resubstitute values to comply with surrounding
- # code norms.
-
- mrl = Signal(64, reset_less=True, name='MASK_FOR_RLC')
- with m.If(mb > me):
- comb += mrl.eq(ml | mr)
- with m.Else():
- comb += mrl.eq(ml & mr)
-
- ainp = Signal(64, reset_less=True, name='A_INP_FOR_RLC')
- comb += ainp.eq(field(rs, 32, 63))
-
- sh = Signal(6, reset_less=True, name='SH_FOR_RLC')
- comb += sh.eq(b[0:6])
-
- exp_shl = Signal(64, reset_less=True,
- name='A_SHIFTED_LEFT_BY_SH_FOR_RLC')
- comb += exp_shl.eq((ainp << sh) & 0xFFFFFFFF)
-
- exp_shr = Signal(64, reset_less=True,
- name='A_SHIFTED_RIGHT_FOR_RLC')
- comb += exp_shr.eq((ainp >> (32 - sh)) & 0xFFFFFFFF)
-
- exp_rot = Signal(64, reset_less=True,
- name='A_ROTATED_LEFT_FOR_RLC')
- comb += exp_rot.eq(exp_shl | exp_shr)
-
- exp_ol = Signal(32, reset_less=True,
- name='EXPECTED_OL_FOR_RLC')
- comb += exp_ol.eq(field((exp_rot & mrl) | (ainp & ~mrl),
- 32, 63))
-
- act_ol = Signal(32, reset_less=True, name='ACTUAL_OL_FOR_RLC')
- comb += act_ol.eq(field(o, 32, 63))
-
- # If I uncomment the following lines, I can confirm that all
- # 32-bit rotations work. If I uncomment only one of the
- # following lines, I can confirm that all 32-bit rotations
- # work. When I remove/recomment BOTH lines, however, the
- # assertion fails. Why??
-
-# comb += Assume(mr == 0xFFFFFFFF)
-# comb += Assume(ml == 0xFFFFFFFF)
- # with m.If(rec.is_32bit):
- # comb += Assert(act_ol == exp_ol)
- # comb += Assert(field(o, 0, 31) == 0)
-
- # TODO
- with m.Case(MicrOp.OP_RLCR):
- pass
- with m.Case(MicrOp.OP_RLCL):
- pass
- with m.Case(MicrOp.OP_TERNLOG):
- lut = dut.fields.FormTLI.TLI[:]
- for i in range(64):
- idx = Cat(dut.i.rb[i], dut.i.ra[i], dut.i.rc[i])
- for j in range(8):
- with m.If(j == idx):
- comb += Assert(dut.o.o.data[i] == lut[j])
- with m.Case(MicrOp.OP_GREV):
- ra_bits = Array(dut.i.ra[i] for i in range(64))
- with m.If(dut.i.ctx.op.is_32bit):
- # assert zero-extended
- comb += Assert(dut.o.o.data[32:] == 0)
- for i in range(32):
- idx = dut.i.rb[0:5] ^ i
- comb += Assert(dut.o.o.data[i]
- == ra_bits[idx])
- with m.Else():
- for i in range(64):
- idx = dut.i.rb[0:6] ^ i
- comb += Assert(dut.o.o.data[i]
- == ra_bits[idx])
-
- with m.Default():
- comb += o_ok.eq(0)
-
- # check that data ok was only enabled when op actioned
- comb += Assert(dut.o.o.ok == o_ok)
-
- return m
-
def _check_shl(self, m, dut):
m.d.comb += Assume(dut.i.ra == 0)
expected = Signal(64)
projects / soc.git / commitdiff