From 23dcd80a9e885ddb4e1c78141eedb8cf055dc13d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jean-Fran=C3=A7ois=20Nguyen?= Date: Mon, 18 Jul 2022 15:03:27 +0200 Subject: [PATCH] Add checks for Rotate/Shift instructions. --- power_fv/check/insn/all.py | 1 + power_fv/check/insn/rotate.py | 26 ++++++ power_fv/insn/const.py | 18 ++++ power_fv/insn/field.py | 3 + power_fv/insn/spec/rotate.py | 156 ++++++++++++++++++++++++++++++++++ 5 files changed, 204 insertions(+) create mode 100644 power_fv/check/insn/rotate.py create mode 100644 power_fv/insn/spec/rotate.py diff --git a/power_fv/check/insn/all.py b/power_fv/check/insn/all.py index 2bd2ddc..989eb13 100644 --- a/power_fv/check/insn/all.py +++ b/power_fv/check/insn/all.py @@ -4,5 +4,6 @@ from .loadstore import * from .cr import * from .compare import * from .logical import * +from .rotate import * from .msr import * from .spr import * diff --git a/power_fv/check/insn/rotate.py b/power_fv/check/insn/rotate.py new file mode 100644 index 0000000..2b0d7eb --- /dev/null +++ b/power_fv/check/insn/rotate.py @@ -0,0 +1,26 @@ +from power_fv.insn import const +from power_fv.insn.spec.rotate import RotateShiftSpec +from power_fv.check.insn import InsnCheck + + +__all__ = [ + "RLWINM", "RLWINM_", "RLWNM", "RLWNM_", "RLWIMI", "RLWIMI_", + "SLW" , "SLW_" , + "SRW" , "SRW_" , "SRAWI", "SRAWI_", "SRAW" , "SRAW_" , +] + + +class RLWINM (InsnCheck, spec_cls=RotateShiftSpec, insn_cls=const.RLWINM ): pass +class RLWINM_(InsnCheck, spec_cls=RotateShiftSpec, insn_cls=const.RLWINM_): pass +class RLWNM (InsnCheck, spec_cls=RotateShiftSpec, insn_cls=const.RLWNM ): pass +class RLWNM_ (InsnCheck, spec_cls=RotateShiftSpec, insn_cls=const.RLWNM_ ): pass +class RLWIMI (InsnCheck, spec_cls=RotateShiftSpec, insn_cls=const.RLWIMI ): pass +class RLWIMI_(InsnCheck, spec_cls=RotateShiftSpec, insn_cls=const.RLWIMI_): pass +class SLW (InsnCheck, spec_cls=RotateShiftSpec, insn_cls=const.SLW ): pass +class SLW_ (InsnCheck, spec_cls=RotateShiftSpec, insn_cls=const.SLW_ ): pass +class SRW (InsnCheck, spec_cls=RotateShiftSpec, insn_cls=const.SRW ): pass +class SRW_ (InsnCheck, spec_cls=RotateShiftSpec, insn_cls=const.SRW_ ): pass +class SRAWI (InsnCheck, spec_cls=RotateShiftSpec, insn_cls=const.SRAWI ): pass +class SRAWI_ (InsnCheck, spec_cls=RotateShiftSpec, insn_cls=const.SRAWI_ ): pass +class SRAW (InsnCheck, spec_cls=RotateShiftSpec, insn_cls=const.SRAW ): pass +class SRAW_ (InsnCheck, spec_cls=RotateShiftSpec, insn_cls=const.SRAW_ ): pass diff --git a/power_fv/insn/const.py b/power_fv/insn/const.py index a110892..eccd9f8 100644 --- a/power_fv/insn/const.py +++ b/power_fv/insn/const.py @@ -173,6 +173,24 @@ class POPCNTB (WordInsn): _fields = (f.PO(31), f.RS(), f.RA(), f.XO_X(12 class POPCNTW (WordInsn): _fields = (f.PO(31), f.RS(), f.RA(), f.XO_X(378)) class PRTYW (WordInsn): _fields = (f.PO(31), f.RS(), f.RA(), f.XO_X(154)) +# Rotate / Shift + +class RLWINM (WordInsn): _fields = (f.PO(21), f.RS(), f.RA(), f.SH(), f.MB(), f.ME(), f.Rc(0)) +class RLWINM_ (WordInsn): _fields = (f.PO(21), f.RS(), f.RA(), f.SH(), f.MB(), f.ME(), f.Rc(1)) +class RLWNM (WordInsn): _fields = (f.PO(23), f.RS(), f.RA(), f.RB(), f.MB(), f.ME(), f.Rc(0)) +class RLWNM_ (WordInsn): _fields = (f.PO(23), f.RS(), f.RA(), f.RB(), f.MB(), f.ME(), f.Rc(1)) +class RLWIMI (WordInsn): _fields = (f.PO(20), f.RS(), f.RA(), f.SH(), f.MB(), f.ME(), f.Rc(0)) +class RLWIMI_ (WordInsn): _fields = (f.PO(20), f.RS(), f.RA(), f.SH(), f.MB(), f.ME(), f.Rc(1)) + +class SLW (WordInsn): _fields = (f.PO(31), f.RS(), f.RA(), f.RB(), f.XO_X( 24), f.Rc(0)) +class SLW_ (WordInsn): _fields = (f.PO(31), f.RS(), f.RA(), f.RB(), f.XO_X( 24), f.Rc(1)) +class SRW (WordInsn): _fields = (f.PO(31), f.RS(), f.RA(), f.RB(), f.XO_X(536), f.Rc(0)) +class SRW_ (WordInsn): _fields = (f.PO(31), f.RS(), f.RA(), f.RB(), f.XO_X(536), f.Rc(1)) +class SRAWI (WordInsn): _fields = (f.PO(31), f.RS(), f.RA(), f.SH(), f.XO_X(824), f.Rc(0)) +class SRAWI_ (WordInsn): _fields = (f.PO(31), f.RS(), f.RA(), f.SH(), f.XO_X(824), f.Rc(1)) +class SRAW (WordInsn): _fields = (f.PO(31), f.RS(), f.RA(), f.RB(), f.XO_X(792), f.Rc(0)) +class SRAW_ (WordInsn): _fields = (f.PO(31), f.RS(), f.RA(), f.RB(), f.XO_X(792), f.Rc(1)) + # Move To/From System Register class MTMSR (WordInsn): _fields = (f.PO(31), f.RS(), f.L_X15(), f.XO_X(146)) diff --git a/power_fv/insn/field.py b/power_fv/insn/field.py index 56c3107..3887a04 100644 --- a/power_fv/insn/field.py +++ b/power_fv/insn/field.py @@ -25,12 +25,15 @@ class LI (InsnField): _shape = signed(24); _offset = 6; _name = "LI" class LK (InsnField): _shape = unsigned( 1); _offset = 31; _name = "LK" class OE (InsnField): _shape = unsigned( 1); _offset = 21; _name = "OE" class PO (InsnField): _shape = unsigned( 6); _offset = 0; _name = "PO" +class MB (InsnField): _shape = unsigned( 5); _offset = 21; _name = "MB" +class ME (InsnField): _shape = unsigned( 5); _offset = 26; _name = "ME" class RA (InsnField): _shape = unsigned( 5); _offset = 11; _name = "RA" class RB (InsnField): _shape = unsigned( 5); _offset = 16; _name = "RB" class Rc (InsnField): _shape = unsigned( 1); _offset = 31; _name = "Rc" class RS (InsnField): _shape = unsigned( 5); _offset = 6; _name = "RS" class RT (InsnField): _shape = unsigned( 5); _offset = 6; _name = "RT" class SI (InsnField): _shape = signed(16); _offset = 16; _name = "SI" +class SH (InsnField): _shape = unsigned( 5); _offset = 16; _name = "SH" class UI (InsnField): _shape = unsigned(16); _offset = 16; _name = "UI" class XO (InsnField): _shape = unsigned( 9); _offset = 22; _name = "XO" class XO_DX (InsnField): _shape = unsigned( 5); _offset = 26; _name = "XO" diff --git a/power_fv/insn/spec/rotate.py b/power_fv/insn/spec/rotate.py new file mode 100644 index 0000000..5d7fbe8 --- /dev/null +++ b/power_fv/insn/spec/rotate.py @@ -0,0 +1,156 @@ +from amaranth import * + +from power_fv import pfv +from power_fv.insn.const import * + +from . import InsnSpec +from .utils import iea + + +__all__ = ["RotateShiftSpec"] + + +class RotateShiftSpec(InsnSpec, Elaboratable): + def __init__(self, insn): + self.pfv = pfv.Interface() + self.insn = insn + + def elaborate(self, platform): + m = Module() + + m.d.comb += [ + self.pfv.stb .eq(1), + self.pfv.insn.eq(Cat(Const(0, 32), self.insn.as_value())), + self.pfv.intr.eq(0), + self.pfv.nia .eq(iea(self.pfv.cia + 4, self.pfv.msr.r_data.sf)), + self.pfv.msr.r_mask.sf.eq(1), + ] + + src = Signal(unsigned(64)) + shamt = Signal(unsigned( 6)) + rotl = Signal(unsigned(64)) + mask = Signal(unsigned(64)) + result = Signal(unsigned(64)) + + # Source operand : (RS)(32:63)||(RS)(32:63) + + m.d.comb += [ + self.pfv.rs.index.eq(self.insn.RS), + self.pfv.rs.r_stb.eq(1), + src.eq(self.pfv.rs.r_data), + ] + + # Shift amount : SH or (RB)(59:63) + + if isinstance(self.insn, (RLWINM, RLWINM_, RLWIMI, RLWIMI_, SRAWI, SRAWI_)): + m.d.comb += shamt.eq(self.insn.SH) + elif isinstance(self.insn, (RLWNM, RLWNM_, SLW, SLW_, SRW, SRW_, SRAW, SRAW_)): + m.d.comb += [ + self.pfv.rb.index.eq(self.insn.RB), + self.pfv.rb.r_stb.eq(1), + shamt.eq(self.pfv.rb.r_data[:6]), + ] + else: + assert False + + # Mask + + def _mask(mstart, mstop): + mask = ((1 << 64-mstart) - 1) & ~((1 << 63-mstop ) - 1) + mask_inv = ~((1 << 63-mstop ) - 1) | ((1 << 64-mstart) - 1) + return Mux(mstart <= mstop, mask, mask_inv) + + if isinstance(self.insn, (RLWINM, RLWINM_, RLWNM, RLWNM_, RLWIMI, RLWIMI_)): + m.d.comb += mask.eq(_mask(self.insn.MB+32, self.insn.ME+32)) + elif isinstance(self.insn, (SLW, SLW_)): + m.d.comb += mask.eq(Mux(shamt[5], 0, _mask(32, 63-shamt))) + elif isinstance(self.insn, (SRW, SRW_, SRAW, SRAW_)): + m.d.comb += mask.eq(Mux(shamt[5], 0, _mask(shamt+32, 63))) + elif isinstance(self.insn, (SRAWI, SRAWI_)): + m.d.comb += mask.eq(_mask(shamt+32, 63)) + else: + assert False + + # Rotation + + def _rotl32(src, n): + v = Repl(src[:32], 2) + return ((v << n) | (v >> 64-n)) & Repl(1, 64) + + if isinstance(self.insn, ( + RLWINM, RLWINM_, RLWNM, RLWNM_, RLWIMI, RLWIMI_, + SLW, SLW_, + )): + m.d.comb += rotl.eq(_rotl32(src, shamt)) + elif isinstance(self.insn, (SRW, SRW_, SRAWI, SRAWI_, SRAW, SRAW_)): + m.d.comb += rotl.eq(_rotl32(src, 64-shamt)) + else: + assert False + + # Write result to RA + + m.d.comb += [ + self.pfv.ra.index .eq(self.insn.RA), + self.pfv.ra.w_stb .eq(1), + self.pfv.ra.w_data.eq(result), + ] + + if isinstance(self.insn, (RLWINM, RLWINM_, RLWNM, RLWNM_, SLW, SLW_, SRW, SRW_)): + m.d.comb += result.eq(rotl & mask) + elif isinstance(self.insn, (RLWIMI, RLWIMI_)): + m.d.comb += self.pfv.ra.r_stb.eq(1) + m.d.comb += result.eq(rotl & mask | self.pfv.ra.r_data & ~mask) + elif isinstance(self.insn, (SRAWI, SRAWI_, SRAW, SRAW_)): + m.d.comb += result.eq(rotl & mask | Repl(src[31], 64) & ~mask) + else: + assert False + + # Write CR0 + + if isinstance(self.insn, ( + RLWINM_, RLWNM_, RLWIMI_, SLW_, SRW_, SRAWI_, SRAW_, + )): + cr0_w_mask = Record([("so", 1), ("eq_", 1), ("gt", 1), ("lt", 1)]) + cr0_w_data = Record([("so", 1), ("eq_", 1), ("gt", 1), ("lt", 1)]) + + m.d.comb += [ + self.pfv.xer.r_mask.so.eq(1), + + cr0_w_mask .eq(0b1111), + cr0_w_data.so .eq(self.pfv.xer.r_data.so), + cr0_w_data.eq_.eq(~Mux(self.pfv.msr.r_data.sf, result[:64].any(), result[:32].any())), + cr0_w_data.gt .eq(~(cr0_w_data.lt | cr0_w_data.eq_)), + cr0_w_data.lt .eq(Mux(self.pfv.msr.r_data.sf, result[63], result[31])), + + self.pfv.cr.w_mask.cr0.eq(cr0_w_mask), + self.pfv.cr.w_data.cr0.eq(cr0_w_data), + ] + + # Write XER + + if isinstance(self.insn, (SRAWI, SRAWI_, SRAW, SRAW_)): + carry = Signal() + + m.d.comb += [ + carry.eq(src[31] & (rotl & ~mask)[:32].any()), + + self.pfv.xer.w_mask.ca .eq(1), + self.pfv.xer.w_data.ca .eq(carry), + self.pfv.xer.w_mask.ca32.eq(1), + self.pfv.xer.w_data.ca32.eq(carry), + ] + + # Interrupt causes + + intr = Record([ + ("rotl32_mask", 1), + ]) + + if isinstance(self.insn, (RLWINM, RLWINM_, RLWNM, RLWNM_, RLWIMI, RLWIMI_)): + m.d.comb += intr.rotl32_mask.eq((self.insn.MB >= 32) | (self.insn.ME >= 32)) + else: + m.d.comb += intr.rotl32_mask.eq(0) + + m.d.comb += self.pfv.intr.eq(intr.any()) + + return m