From 0f731db18ad9de78493b1db755478dfae9b1ff2f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jean-Fran=C3=A7ois=20Nguyen?= Date: Wed, 13 Jul 2022 20:58:56 +0200 Subject: [PATCH] Add checks for Load/Store instructions. --- power_fv/check/insn/all.py | 13 +- power_fv/check/insn/loadstore.py | 49 ++++++ power_fv/insn/const.py | 39 +++++ power_fv/insn/field.py | 1 + power_fv/insn/spec/loadstore.py | 272 +++++++++++++++++++++++++++++++ power_fv/insn/spec/utils.py | 10 +- 6 files changed, 376 insertions(+), 8 deletions(-) create mode 100644 power_fv/check/insn/loadstore.py create mode 100644 power_fv/insn/spec/loadstore.py diff --git a/power_fv/check/insn/all.py b/power_fv/check/insn/all.py index e380813..3ae4b5d 100644 --- a/power_fv/check/insn/all.py +++ b/power_fv/check/insn/all.py @@ -1,6 +1,7 @@ -from .addsub import * -from .branch import * -from .cr import * -from .compare import * -from .msr import * -from .spr import * +from .addsub import * +from .branch import * +from .loadstore import * +from .cr import * +from .compare import * +from .msr import * +from .spr import * diff --git a/power_fv/check/insn/loadstore.py b/power_fv/check/insn/loadstore.py new file mode 100644 index 0000000..7d98d3e --- /dev/null +++ b/power_fv/check/insn/loadstore.py @@ -0,0 +1,49 @@ +from power_fv.insn import const +from power_fv.insn.spec.loadstore import LoadStoreSpec +from power_fv.check.insn import InsnCheck + + +__all__ = [ + "LBZ", "LBZX", "LBZU", "LBZUX", + "LHZ", "LHZX", "LHZU", "LHZUX", "LHA", "LHAX", "LHAU", "LHAUX", + "LWZ", "LWZU", "LWZX", "LWZUX", + "STB", "STBX", "STBU", "STBUX", + "STH", "STHU", "STHX", "STHUX", + "STW", "STWX", "STWX", "STWUX", + "LWBRX", "STHBRX", "STWBRX", +] + + +class LBZ (InsnCheck, spec_cls=LoadStoreSpec, insn_cls=const.LBZ ): pass +class LBZX (InsnCheck, spec_cls=LoadStoreSpec, insn_cls=const.LBZX ): pass +class LBZU (InsnCheck, spec_cls=LoadStoreSpec, insn_cls=const.LBZU ): pass +class LBZUX (InsnCheck, spec_cls=LoadStoreSpec, insn_cls=const.LBZUX): pass +class LHZ (InsnCheck, spec_cls=LoadStoreSpec, insn_cls=const.LHZ ): pass +class LHZX (InsnCheck, spec_cls=LoadStoreSpec, insn_cls=const.LHZX ): pass +class LHZU (InsnCheck, spec_cls=LoadStoreSpec, insn_cls=const.LHZU ): pass +class LHZUX (InsnCheck, spec_cls=LoadStoreSpec, insn_cls=const.LHZUX): pass +class LHA (InsnCheck, spec_cls=LoadStoreSpec, insn_cls=const.LHA ): pass +class LHAX (InsnCheck, spec_cls=LoadStoreSpec, insn_cls=const.LHAX ): pass +class LHAU (InsnCheck, spec_cls=LoadStoreSpec, insn_cls=const.LHAU ): pass +class LHAUX (InsnCheck, spec_cls=LoadStoreSpec, insn_cls=const.LHAUX): pass +class LWZ (InsnCheck, spec_cls=LoadStoreSpec, insn_cls=const.LWZ ): pass +class LWZX (InsnCheck, spec_cls=LoadStoreSpec, insn_cls=const.LWZX ): pass +class LWZU (InsnCheck, spec_cls=LoadStoreSpec, insn_cls=const.LWZU ): pass +class LWZUX (InsnCheck, spec_cls=LoadStoreSpec, insn_cls=const.LWZUX): pass + +class STB (InsnCheck, spec_cls=LoadStoreSpec, insn_cls=const.STB ): pass +class STBX (InsnCheck, spec_cls=LoadStoreSpec, insn_cls=const.STBX ): pass +class STBU (InsnCheck, spec_cls=LoadStoreSpec, insn_cls=const.STBU ): pass +class STBUX (InsnCheck, spec_cls=LoadStoreSpec, insn_cls=const.STBUX): pass +class STH (InsnCheck, spec_cls=LoadStoreSpec, insn_cls=const.STH ): pass +class STHX (InsnCheck, spec_cls=LoadStoreSpec, insn_cls=const.STHX ): pass +class STHU (InsnCheck, spec_cls=LoadStoreSpec, insn_cls=const.STHU ): pass +class STHUX (InsnCheck, spec_cls=LoadStoreSpec, insn_cls=const.STHUX): pass +class STW (InsnCheck, spec_cls=LoadStoreSpec, insn_cls=const.STW ): pass +class STWX (InsnCheck, spec_cls=LoadStoreSpec, insn_cls=const.STWX ): pass +class STWU (InsnCheck, spec_cls=LoadStoreSpec, insn_cls=const.STWU ): pass +class STWUX (InsnCheck, spec_cls=LoadStoreSpec, insn_cls=const.STWUX): pass + +class LWBRX (InsnCheck, spec_cls=LoadStoreSpec, insn_cls=const.LWBRX ): pass +class STHBRX(InsnCheck, spec_cls=LoadStoreSpec, insn_cls=const.STHBRX): pass +class STWBRX(InsnCheck, spec_cls=LoadStoreSpec, insn_cls=const.STWBRX): pass diff --git a/power_fv/insn/const.py b/power_fv/insn/const.py index 5c6cd88..64d7edb 100644 --- a/power_fv/insn/const.py +++ b/power_fv/insn/const.py @@ -33,6 +33,45 @@ class CREQV (WordInsn): _fields = (f.PO(19), f.BT(), f.BA(), f.BB(), f.XO_XL(2 class CRORC (WordInsn): _fields = (f.PO(19), f.BT(), f.BA(), f.BB(), f.XO_XL(417)) class MCRF (WordInsn): _fields = (f.PO(19), f.BF(), f.BFA(), f.XO_XL( 0)) +# Load + +class LBZ (WordInsn): _fields = (f.PO(34), f.RT(), f.RA(), f.D()) +class LBZX (WordInsn): _fields = (f.PO(31), f.RT(), f.RA(), f.RB(), f.XO_X( 87)) +class LBZU (WordInsn): _fields = (f.PO(35), f.RT(), f.RA(), f.D()) +class LBZUX (WordInsn): _fields = (f.PO(31), f.RT(), f.RA(), f.RB(), f.XO_X(119)) +class LHZ (WordInsn): _fields = (f.PO(40), f.RT(), f.RA(), f.D()) +class LHZX (WordInsn): _fields = (f.PO(31), f.RT(), f.RA(), f.RB(), f.XO_X(279)) +class LHZU (WordInsn): _fields = (f.PO(41), f.RT(), f.RA(), f.D()) +class LHZUX (WordInsn): _fields = (f.PO(31), f.RT(), f.RA(), f.RB(), f.XO_X(311)) +class LHA (WordInsn): _fields = (f.PO(42), f.RT(), f.RA(), f.D()) +class LHAX (WordInsn): _fields = (f.PO(31), f.RT(), f.RA(), f.RB(), f.XO_X(343)) +class LHAU (WordInsn): _fields = (f.PO(43), f.RT(), f.RA(), f.D()) +class LHAUX (WordInsn): _fields = (f.PO(31), f.RT(), f.RA(), f.RB(), f.XO_X(375)) +class LWZ (WordInsn): _fields = (f.PO(32), f.RT(), f.RA(), f.D()) +class LWZX (WordInsn): _fields = (f.PO(31), f.RT(), f.RA(), f.RB(), f.XO_X( 23)) +class LWZU (WordInsn): _fields = (f.PO(33), f.RT(), f.RA(), f.D()) +class LWZUX (WordInsn): _fields = (f.PO(31), f.RT(), f.RA(), f.RB(), f.XO_X( 55)) + +class LWBRX (WordInsn): _fields = (f.PO(31), f.RT(), f.RA(), f.RB(), f.XO_X(534)) + +# Store + +class STB (WordInsn): _fields = (f.PO(38), f.RS(), f.RA(), f.D()) +class STBX (WordInsn): _fields = (f.PO(31), f.RS(), f.RA(), f.RB(), f.XO_X(215)) +class STBU (WordInsn): _fields = (f.PO(39), f.RS(), f.RA(), f.D()) +class STBUX (WordInsn): _fields = (f.PO(31), f.RS(), f.RA(), f.RB(), f.XO_X(247)) +class STH (WordInsn): _fields = (f.PO(44), f.RS(), f.RA(), f.D()) +class STHX (WordInsn): _fields = (f.PO(31), f.RS(), f.RA(), f.RB(), f.XO_X(407)) +class STHU (WordInsn): _fields = (f.PO(45), f.RS(), f.RA(), f.D()) +class STHUX (WordInsn): _fields = (f.PO(31), f.RS(), f.RA(), f.RB(), f.XO_X(439)) +class STW (WordInsn): _fields = (f.PO(36), f.RS(), f.RA(), f.D()) +class STWX (WordInsn): _fields = (f.PO(31), f.RS(), f.RA(), f.RB(), f.XO_X(151)) +class STWU (WordInsn): _fields = (f.PO(37), f.RS(), f.RA(), f.D()) +class STWUX (WordInsn): _fields = (f.PO(31), f.RS(), f.RA(), f.RB(), f.XO_X(183)) + +class STHBRX (WordInsn): _fields = (f.PO(31), f.RS(), f.RA(), f.RB(), f.XO_X(918)) +class STWBRX (WordInsn): _fields = (f.PO(31), f.RS(), f.RA(), f.RB(), f.XO_X(662)) + # Add / Subtract From class ADDI (WordInsn): _fields = (f.PO(14), f.RT(), f.RA(), f.SI()) diff --git a/power_fv/insn/field.py b/power_fv/insn/field.py index 674c356..56c3107 100644 --- a/power_fv/insn/field.py +++ b/power_fv/insn/field.py @@ -14,6 +14,7 @@ class BI (InsnField): _shape = unsigned( 5); _offset = 11; _name = "BI" class BO (InsnField): _shape = unsigned( 5); _offset = 6; _name = "BO" class BT (InsnField): _shape = unsigned( 5); _offset = 6; _name = "BT" class CY (InsnField): _shape = unsigned( 2); _offset = 21; _name = "CY" +class D (InsnField): _shape = signed(16); _offset = 16; _name = "D" class d0 (InsnField): _shape = signed(10); _offset = 16; _name = "d0" class d1 (InsnField): _shape = signed( 5); _offset = 11; _name = "d1" class d2 (InsnField): _shape = signed( 1); _offset = 31; _name = "d2" diff --git a/power_fv/insn/spec/loadstore.py b/power_fv/insn/spec/loadstore.py new file mode 100644 index 0000000..54e9d90 --- /dev/null +++ b/power_fv/insn/spec/loadstore.py @@ -0,0 +1,272 @@ +from amaranth import * +from amaranth.utils import log2_int + +from power_fv import pfv +from power_fv.insn.const import * + +from . import InsnSpec +from .utils import iea, byte_reversed + + +__all__ = ["LoadStoreSpec"] + + +class LoadStoreSpec(InsnSpec, Elaboratable): + def __init__(self, insn, *, dword_aligned=False): + self.pfv = pfv.Interface() + self.insn = insn + self.dword_aligned = dword_aligned + + 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.nia .eq(iea(self.pfv.cia + 4, self.pfv.msr.r_data.sf)), + self.pfv.msr.r_mask.sf.eq(1), + ] + + # EA (effective address) = ea_base + ea_offset + + ea = Signal(64) + ea_base = Signal(64) + ea_offset = Signal(64) + + # ea_base : (RA|0) or (RA) + + m.d.comb += self.pfv.ra.index.eq(self.insn.RA) + + if isinstance(self.insn, ( + LBZ, LBZX, LHZ, LHZX, LHA, LHAX, LWZ, LWZX, + STB, STBX, STH, STHX, STW, STWX, + LWBRX, STHBRX, STWBRX + )): + m.d.comb += [ + self.pfv.ra.r_stb.eq(self.insn.RA != 0), + ea_base.eq(Mux(self.insn.RA != 0, self.pfv.ra.r_data, 0)), + ] + elif isinstance(self.insn, ( + LBZU, LBZUX, LHZU, LHZUX, LHAU, LHAUX, LWZU, LWZUX, + STBU, STBUX, STHU, STHUX, STWU, STWUX + )): + m.d.comb += [ + self.pfv.ra.r_stb.eq(1), + ea_base.eq(self.pfv.ra.r_data), + ] + else: + assert False + + # ea_offset : EXTS(D) or (RB) + + if isinstance(self.insn, ( + LBZ, LBZU, LHZ, LHZU, LHA, LHAU, LWZ, LWZU, + STB, STBU, STH, STHU, STW, STWU, + )): + m.d.comb += ea_offset.eq(self.insn.D.as_signed()) + elif isinstance(self.insn, ( + LBZX, LBZUX, LHZX, LHZUX, LHAX, LHAUX, LWZX, LWZUX, + STBX, STBUX, STHX, STHUX, STWX, STWUX, + LWBRX, STHBRX, STWBRX, + )): + m.d.comb += [ + self.pfv.rb.index.eq(self.insn.RB), + self.pfv.rb.r_stb.eq(1), + ea_offset.eq(self.pfv.rb.r_data) + ] + else: + assert False + + m.d.comb += ea.eq(iea(ea_base + ea_offset, self.pfv.msr.r_data.sf)) + + # If `dword_aligned` is set, `pfv.mem.addr` points to the dword containing EA. + # If `dword_aligned` is unset, `pfv.mem.addr` is equal to EA. + + byte_offset = Signal(3) + half_offset = Signal(2) + word_offset = Signal(1) + + m.d.comb += self.pfv.mem.addr[3:].eq(ea[3:]) + + if self.dword_aligned: + m.d.comb += [ + self.pfv.mem.addr[:3].eq(0), + byte_offset.eq(ea[:3]), + ] + else: + m.d.comb += [ + self.pfv.mem.addr[:3].eq(ea[:3]), + byte_offset.eq(0), + ] + + m.d.comb += [ + half_offset.eq(byte_offset[1:]), + word_offset.eq(byte_offset[2:]), + ] + + msr_le = self.pfv.msr.r_data.le + m.d.comb += self.pfv.msr.r_mask.le.eq(1) + + # Load: read from memory, then write the result to RT. + + if isinstance(self.insn, ( + LBZ, LBZX, LBZU, LBZUX, + LHZ, LHZX, LHZU, LHZUX, + LHA, LHAX, LHAU, LHAUX, + LWZ, LWZX, LWZU, LWZUX, + LWBRX, + )): + load_byte = Signal( 8) + load_half = Signal(16) + load_word = Signal(32) + load_result = Signal(64) + + m.d.comb += [ + load_byte.eq(self.pfv.mem.r_data.word_select(byte_offset, width= 8)), + load_half.eq(self.pfv.mem.r_data.word_select(half_offset, width=16)), + load_word.eq(self.pfv.mem.r_data.word_select(word_offset, width=32)), + ] + + if isinstance(self.insn, (LBZ, LBZX, LBZU, LBZUX)): + m.d.comb += [ + self.pfv.mem.r_mask.word_select(byte_offset, width=1).eq(0x1), + load_result.eq(load_byte.as_unsigned()), + ] + elif isinstance(self.insn, (LHZ, LHZX, LHZU, LHZUX)): + m.d.comb += [ + self.pfv.mem.r_mask.word_select(half_offset, width=2).eq(0x3), + load_result.eq(byte_reversed(load_half, ~msr_le).as_unsigned()), + ] + elif isinstance(self.insn, (LHA, LHAX, LHAU, LHAUX)): + m.d.comb += [ + self.pfv.mem.r_mask.word_select(half_offset, width=2).eq(0x3), + load_result.eq(byte_reversed(load_half, ~msr_le).as_signed()) + ] + elif isinstance(self.insn, (LWZ, LWZX, LWZU, LWZUX)): + m.d.comb += [ + self.pfv.mem.r_mask.word_select(word_offset, width=4).eq(0xf), + load_result.eq(byte_reversed(load_word, ~msr_le).as_unsigned()), + ] + elif isinstance(self.insn, LWBRX): + m.d.comb += [ + self.pfv.mem.r_mask.word_select(word_offset, width=4).eq(0xf), + load_result.eq(byte_reversed(load_word, msr_le).as_unsigned()), + ] + else: + assert False + + m.d.comb += [ + self.pfv.rt.index .eq(self.insn.RT), + self.pfv.rt.w_stb .eq(1), + self.pfv.rt.w_data.eq(load_result), + ] + + # Store: read from RS, then write the result to memory. + + elif isinstance(self.insn, ( + STB, STBX, STBU, STBUX, + STH, STHX, STHU, STHUX, + STW, STWX, STWU, STWUX, + STHBRX, STWBRX, + )): + store_byte = Signal(64) + store_half = Signal(64) + store_word = Signal(64) + + m.d.comb += [ + self.pfv.rs.index.eq(self.insn.RS), + self.pfv.rs.r_stb.eq(1), + + store_byte.eq(Repl(self.pfv.rs.r_data[: 8], count=8)), + store_half.eq(Repl(self.pfv.rs.r_data[:16], count=4)), + store_word.eq(Repl(self.pfv.rs.r_data[:32], count=2)), + ] + + if isinstance(self.insn, (STB, STBX, STBU, STBUX)): + m.d.comb += [ + self.pfv.mem.w_mask.word_select(byte_offset, width=1).eq(0x1), + self.pfv.mem.w_data.eq(store_byte), + ] + elif isinstance(self.insn, (STH, STHX, STHU, STHUX)): + m.d.comb += [ + self.pfv.mem.w_mask.word_select(half_offset, width=2).eq(0x3), + self.pfv.mem.w_data.eq(byte_reversed(store_half, ~msr_le)), + ] + elif isinstance(self.insn, (STW, STWX, STWU, STWUX)): + m.d.comb += [ + self.pfv.mem.w_mask.word_select(word_offset, width=4).eq(0xf), + self.pfv.mem.w_data.eq(byte_reversed(store_word, ~msr_le)), + ] + elif isinstance(self.insn, STHBRX): + m.d.comb += [ + self.pfv.mem.w_mask.word_select(half_offset, width=2).eq(0x3), + self.pfv.mem.w_data.eq(byte_reversed(store_half, msr_le)), + ] + elif isinstance(self.insn, STWBRX): + m.d.comb += [ + self.pfv.mem.w_mask.word_select(word_offset, width=4).eq(0xf), + self.pfv.mem.w_data.eq(byte_reversed(store_word, msr_le)), + ] + else: + assert False + + else: + assert False + + # Load/store with update: write EA to RA. + + if isinstance(self.insn, ( + LBZU, LBZUX, LHZU, LHZUX, LHAU, LHAUX, LWZU, LWZUX, + STBU, STBUX, STHU, STHUX, STWU, STWUX, + )): + m.d.comb += [ + self.pfv.ra.w_stb .eq(1), + self.pfv.ra.w_data.eq(ea), + ] + + # Interrupt causes + + intr = Record([ + ("misaligned", 1), + ("update_zero", 1), + ("update_rt", 1), + ]) + + if isinstance(self.insn, ( + LBZ, LBZX, LBZU, LBZUX, + STB, STBX, STBU, STBUX, + )): + m.d.comb += intr.misaligned.eq(0) + elif isinstance(self.insn, ( + LHZ, LHZX, LHZU, LHZUX, LHA, LHAX, LHAU, LHAUX, + STH, STHX, STHU, STHUX, + STHBRX, + )): + m.d.comb += intr.misaligned.eq(byte_offset[0]) + elif isinstance(self.insn, ( + LWZ, LWZX, LWZU, LWZUX, + STW, STWX, STWU, STWUX, + LWBRX, STWBRX, + )): + m.d.comb += intr.misaligned.eq(byte_offset[:1].any()) + else: + assert False + + if isinstance(self.insn, ( + LBZU, LBZUX, LHZU, LHZUX, LHAU, LHAUX, LWZU, LWZUX, + STBU, STBUX, STHU, STHUX, STWU, STWUX, + )): + m.d.comb += intr.update_zero.eq(self.insn.RA == 0) + else: + m.d.comb += intr.update_zero.eq(0) + + if isinstance(self.insn, ( + LBZU, LBZUX, LHZU, LHZUX, LHAU, LHAUX, LWZU, LWZUX, + )): + m.d.comb += intr.update_rt.eq(self.insn.RA == self.insn.RT) + else: + m.d.comb += intr.update_rt.eq(0) + + m.d.comb += self.pfv.intr.eq(intr.any()) + + return m diff --git a/power_fv/insn/spec/utils.py b/power_fv/insn/spec/utils.py index 158f487..dc12651 100644 --- a/power_fv/insn/spec/utils.py +++ b/power_fv/insn/spec/utils.py @@ -1,8 +1,7 @@ from amaranth import * -from amaranth.utils import bits_for -__all__ = ["iea"] +__all__ = ["iea", "byte_reversed"] def iea(addr, msr_sf): @@ -11,3 +10,10 @@ def iea(addr, msr_sf): assert len(msr_sf) == 1 mask = Cat(Repl(1, 32), Repl(msr_sf, 32)) return addr & mask + + +def byte_reversed(src, en=0): + src, en = Value.cast(src), Value.cast(en) + assert len(src) in {8, 16, 32, 64} + res = Cat(src.word_select(i, width=8) for i in reversed(range(len(src) // 8))) + return Mux(en, res, src)