From 7b7aa6cc9bc495b8ddee08b3cad08d1f63078034 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jean-Fran=C3=A7ois=20Nguyen?= Date: Mon, 18 Jul 2022 15:14:33 +0200 Subject: [PATCH] Add checks for CR Move / Set Boolean instructions. --- power_fv/check/insn/cr.py | 37 ++++++--- power_fv/insn/const.py | 14 +++- power_fv/insn/field.py | 2 + power_fv/insn/spec/cr.py | 156 ++++++++++++++++++++++++++++++++++---- 4 files changed, 183 insertions(+), 26 deletions(-) diff --git a/power_fv/check/insn/cr.py b/power_fv/check/insn/cr.py index 2c90f3b..2a26e0d 100644 --- a/power_fv/check/insn/cr.py +++ b/power_fv/check/insn/cr.py @@ -1,20 +1,35 @@ from power_fv.insn import const -from power_fv.insn.spec.cr import CRSpec +from power_fv.insn.spec.cr import CRLogicalSpec, CRMoveSpec from power_fv.check.insn import InsnCheck __all__ = [ "CRAND", "CROR", "CRNAND", "CRXOR", "CRNOR", "CRANDC", "CREQV", "CRORC", - "MCRF" , + "MCRF", "MCRXRX", "MTCRF", "MFOCRF", "MFCR", + "SETB", #"SETBC", "SETBCR", "SETNBC", "SETNBCR", ] -class CRAND (InsnCheck, spec_cls=CRSpec, insn_cls=const.CRAND ): pass -class CROR (InsnCheck, spec_cls=CRSpec, insn_cls=const.CROR ): pass -class CRNAND (InsnCheck, spec_cls=CRSpec, insn_cls=const.CRNAND): pass -class CRXOR (InsnCheck, spec_cls=CRSpec, insn_cls=const.CRXOR ): pass -class CRNOR (InsnCheck, spec_cls=CRSpec, insn_cls=const.CRNOR ): pass -class CRANDC (InsnCheck, spec_cls=CRSpec, insn_cls=const.CRANDC): pass -class CREQV (InsnCheck, spec_cls=CRSpec, insn_cls=const.CREQV ): pass -class CRORC (InsnCheck, spec_cls=CRSpec, insn_cls=const.CRORC ): pass -class MCRF (InsnCheck, spec_cls=CRSpec, insn_cls=const.MCRF ): pass +class CRAND (InsnCheck, spec_cls=CRLogicalSpec, insn_cls=const.CRAND ): pass +class CROR (InsnCheck, spec_cls=CRLogicalSpec, insn_cls=const.CROR ): pass +class CRNAND (InsnCheck, spec_cls=CRLogicalSpec, insn_cls=const.CRNAND): pass +class CRXOR (InsnCheck, spec_cls=CRLogicalSpec, insn_cls=const.CRXOR ): pass +class CRNOR (InsnCheck, spec_cls=CRLogicalSpec, insn_cls=const.CRNOR ): pass +class CRANDC (InsnCheck, spec_cls=CRLogicalSpec, insn_cls=const.CRANDC): pass +class CREQV (InsnCheck, spec_cls=CRLogicalSpec, insn_cls=const.CREQV ): pass +class CRORC (InsnCheck, spec_cls=CRLogicalSpec, insn_cls=const.CRORC ): pass + +class MCRF (InsnCheck, spec_cls=CRMoveSpec, insn_cls=const.MCRF ): pass +class MCRXRX (InsnCheck, spec_cls=CRMoveSpec, insn_cls=const.MCRXRX): pass +class MTOCRF (InsnCheck, spec_cls=CRMoveSpec, insn_cls=const.MTOCRF): pass +class MTCRF (InsnCheck, spec_cls=CRMoveSpec, insn_cls=const.MTCRF ): pass +class MFOCRF (InsnCheck, spec_cls=CRMoveSpec, insn_cls=const.MFOCRF): pass +class MFCR (InsnCheck, spec_cls=CRMoveSpec, insn_cls=const.MFCR ): pass + +class SETB (InsnCheck, spec_cls=CRMoveSpec, insn_cls=const.SETB ): pass + +# TODO: add a --exclude= argument to the 'check' command +# class SETBC (InsnCheck, spec_cls=CRMoveSpec, insn_cls=const.SETBC ): pass +# class SETBCR (InsnCheck, spec_cls=CRMoveSpec, insn_cls=const.SETBCR ): pass +# class SETNBC (InsnCheck, spec_cls=CRMoveSpec, insn_cls=const.SETNBC ): pass +# class SETNBCR(InsnCheck, spec_cls=CRMoveSpec, insn_cls=const.SETNBCR): pass diff --git a/power_fv/insn/const.py b/power_fv/insn/const.py index 9db681c..4cf40c6 100644 --- a/power_fv/insn/const.py +++ b/power_fv/insn/const.py @@ -36,7 +36,19 @@ class CRNOR (WordInsn): _fields = (f.PO(19), f.BT(), f.BA(), f.BB(), f.XO_XL( class CRANDC (WordInsn): _fields = (f.PO(19), f.BT(), f.BA(), f.BB(), f.XO_XL(129)) class CREQV (WordInsn): _fields = (f.PO(19), f.BT(), f.BA(), f.BB(), f.XO_XL(289)) 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)) + +class MCRF (WordInsn): _fields = (f.PO(19), f.BF(), f.BFA(), f.XO_XL ( 0)) +class MCRXRX (WordInsn): _fields = (f.PO(31), f.BF(), f.XO_X (576)) +class MTOCRF (WordInsn): _fields = (f.PO(31), f.RS(), f.XFX_11(1), f.FXM(), f.XO_XFX(144)) +class MTCRF (WordInsn): _fields = (f.PO(31), f.RS(), f.XFX_11(0), f.FXM(), f.XO_XFX(144)) +class MFOCRF (WordInsn): _fields = (f.PO(31), f.RT(), f.XFX_11(1), f.FXM(), f.XO_XFX( 19)) +class MFCR (WordInsn): _fields = (f.PO(31), f.RT(), f.XFX_11(0), f.XO_XFX( 19)) + +class SETB (WordInsn): _fields = (f.PO(31), f.RT(), f.BFA(), f.XO_X(128)) +class SETBC (WordInsn): _fields = (f.PO(31), f.RT(), f.BI(), f.XO_X(384)) +class SETBCR (WordInsn): _fields = (f.PO(31), f.RT(), f.BI(), f.XO_X(416)) +class SETNBC (WordInsn): _fields = (f.PO(31), f.RT(), f.BI(), f.XO_X(448)) +class SETNBCR (WordInsn): _fields = (f.PO(31), f.RT(), f.BI(), f.XO_X(480)) # Load diff --git a/power_fv/insn/field.py b/power_fv/insn/field.py index 376e57f..0ac2ae8 100644 --- a/power_fv/insn/field.py +++ b/power_fv/insn/field.py @@ -18,6 +18,7 @@ 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" +class FXM (InsnField): _shape = unsigned( 8); _offset = 12; _name = "FXM" class LEV (InsnField): _shape = unsigned( 7); _offset = 20; _name = "LEV" class L_D10 (InsnField): _shape = unsigned( 1); _offset = 10; _name = "L" class L_X10 (InsnField): _shape = unsigned( 1); _offset = 10; _name = "L" @@ -39,6 +40,7 @@ class SI (InsnField): _shape = signed(16); _offset = 16; _name = "SI" class SH (InsnField): _shape = unsigned( 5); _offset = 16; _name = "SH" class TO (InsnField): _shape = unsigned( 5); _offset = 6; _name = "TO" class UI (InsnField): _shape = unsigned(16); _offset = 16; _name = "UI" +class XFX_11(InsnField): _shape = unsigned( 1); _offset = 11; _name = "_11" class XO (InsnField): _shape = unsigned( 9); _offset = 22; _name = "XO" class XO_DX (InsnField): _shape = unsigned( 5); _offset = 26; _name = "XO" class XO_X (InsnField): _shape = unsigned(10); _offset = 21; _name = "XO" diff --git a/power_fv/insn/spec/cr.py b/power_fv/insn/spec/cr.py index a91607e..738a1df 100644 --- a/power_fv/insn/spec/cr.py +++ b/power_fv/insn/spec/cr.py @@ -1,16 +1,19 @@ from amaranth import * +from amaranth.asserts import Assume +from amaranth.lib.coding import Encoder from power_fv import pfv from power_fv.insn.const import * +from power_fv.build.sby import SymbiYosysPlatform from . import InsnSpec from .utils import iea -__all__ = ["CRSpec"] +__all__ = ["CRLogicalSpec", "CRMoveSpec"] -class CRSpec(InsnSpec, Elaboratable): +class CRLogicalSpec(InsnSpec, Elaboratable): def __init__(self, insn): self.pfv = pfv.Interface() self.insn = insn @@ -35,11 +38,11 @@ class CRSpec(InsnSpec, Elaboratable): result = Signal() m.d.comb += [ - self.pfv.cr.r_mask[::-1].bit_select(self.insn.BA, width=1).eq(1), - self.pfv.cr.r_mask[::-1].bit_select(self.insn.BB, width=1).eq(1), + self.pfv.cr.r_mask.bit_select(31-self.insn.BA, width=1).eq(1), + self.pfv.cr.r_mask.bit_select(31-self.insn.BB, width=1).eq(1), - src_a.eq(self.pfv.cr.r_data[::-1].bit_select(self.insn.BA, width=1)), - src_b.eq(self.pfv.cr.r_data[::-1].bit_select(self.insn.BB, width=1)), + src_a.eq(self.pfv.cr.r_data.bit_select(31-self.insn.BA, width=1)), + src_b.eq(self.pfv.cr.r_data.bit_select(31-self.insn.BB, width=1)), ] if isinstance(self.insn, CRAND): @@ -60,21 +63,146 @@ class CRSpec(InsnSpec, Elaboratable): m.d.comb += result.eq(src_a | ~src_b) m.d.comb += [ - self.pfv.cr.w_mask[::-1].bit_select(self.insn.BT, width=1).eq(1), - self.pfv.cr.w_data[::-1].bit_select(self.insn.BT, width=1).eq(result), + self.pfv.cr.w_mask.bit_select(31-self.insn.BT, width=1).eq(1), + self.pfv.cr.w_data.bit_select(31-self.insn.BT, width=1).eq(result), ] - elif isinstance(self.insn, MCRF): - field = Signal(4) + else: + assert False + + return m + + +class CRMoveSpec(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), + ] + if isinstance(self.insn, MCRF): + crf = Signal(4) m.d.comb += [ - field.eq(self.pfv.cr.r_data[::-1].word_select(self.insn.BFA, width=4)), + self.pfv.cr.r_mask.word_select(7-self.insn.BFA, width=4).eq(0xf), + crf.eq(self.pfv.cr.r_data.word_select(7-self.insn.BFA, width=4)), + + self.pfv.cr.w_mask.word_select(7-self.insn.BF, width=4).eq(0xf), + self.pfv.cr.w_data.word_select(7-self.insn.BF, width=4).eq(crf), + ] + + elif isinstance(self.insn, MCRXRX): + crf = Record([("ca32", 1), ("ca", 1), ("ov32", 1), ("ov", 1)]) - self.pfv.cr.r_mask[::-1].word_select(self.insn.BFA, width=4).eq(0b1111), - self.pfv.cr.w_mask[::-1].word_select(self.insn.BF, width=4).eq(0b1111), - self.pfv.cr.w_data[::-1].word_select(self.insn.BF, width=4).eq(field), + m.d.comb += [ + self.pfv.xer.r_mask.ov .eq(1), + self.pfv.xer.r_mask.ov32.eq(1), + self.pfv.xer.r_mask.ca .eq(1), + self.pfv.xer.r_mask.ca32.eq(1), + + crf.ov .eq(self.pfv.xer.r_data.ov), + crf.ov32.eq(self.pfv.xer.r_data.ov32), + crf.ca .eq(self.pfv.xer.r_data.ca), + crf.ca32.eq(self.pfv.xer.r_data.ca32), + + self.pfv.cr.w_mask.word_select(7-self.insn.BF, width=4).eq(0xf), + self.pfv.cr.w_data.word_select(7-self.insn.BF, width=4).eq(crf), ] + elif isinstance(self.insn, MTOCRF): + crf = Signal(4) + + m.submodules.fxm_enc = fxm_enc = Encoder(width=8) + m.d.comb += [ + fxm_enc.i.eq(self.insn.FXM), + + self.pfv.rs.index.eq(self.insn.RS), + self.pfv.rs.r_stb.eq(1), + crf.eq(self.pfv.rs.r_data.word_select(fxm_enc.o, width=4)), + + self.pfv.cr.w_mask.word_select(fxm_enc.o, width=4).eq(0xf), + self.pfv.cr.w_data.word_select(fxm_enc.o, width=4).eq(crf), + ] + + # Unless exactly one FXM bit is set to 1, CR contents are undefined. + if isinstance(platform, SymbiYosysPlatform): + m.d.comb += Assume(~fxm_enc.n) + + elif isinstance(self.insn, MTCRF): + m.d.comb += [ + self.pfv.rs.index.eq(self.insn.RS), + self.pfv.rs.r_stb.eq(1), + + self.pfv.cr.w_mask.eq(Cat(Repl(b, 4) for b in self.insn.FXM)), + self.pfv.cr.w_data.eq(self.pfv.rs.r_data[:32]), + ] + + elif isinstance(self.insn, MFOCRF): + crf = Signal(4) + + m.submodules.fxm_enc = fxm_enc = Encoder(width=8) + m.d.comb += [ + fxm_enc.i.eq(self.insn.FXM), + + self.pfv.cr.r_mask.word_select(fxm_enc.o, width=4).eq(Mux(fxm_enc.n, 0x0, 0xf)), + crf.eq(self.pfv.cr.r_data.word_select(fxm_enc.o, width=4)), + + self.pfv.rt.index.eq(self.insn.RT), + self.pfv.rt.w_stb.eq(1), + self.pfv.rt.w_data.word_select(fxm_enc.o, width=4).eq(crf), + ] + + # Unless exactly one FXM bit is set to 1, RT contents are undefined. + if isinstance(platform, SymbiYosysPlatform): + m.d.comb += Assume(~fxm_enc.n) + + elif isinstance(self.insn, MFCR): + m.d.comb += [ + self.pfv.cr.r_mask.eq(Repl(1, 32)), + self.pfv.rt.index .eq(self.insn.RT), + self.pfv.rt.w_stb .eq(1), + self.pfv.rt.w_data.eq(self.pfv.cr.r_data), + ] + + elif isinstance(self.insn, SETB): + crf = Signal(4) + m.d.comb += [ + self.pfv.cr.r_mask.word_select(7-self.insn.BFA, width=4).eq(0xf), + crf.eq(self.pfv.cr.r_data.word_select(7-self.insn.BFA, width=4)), + + self.pfv.rt.index.eq(self.insn.RT), + self.pfv.rt.w_stb.eq(1), + self.pfv.rt.w_data.eq(Mux(crf[3-0], Repl(1, 64), crf[3-1])), + ] + + elif isinstance(self.insn, (SETBC, SETBCR, SETNBC, SETNBCR)): + crb = Signal() + + m.d.comb += [ + self.pfv.cr.r_mask.bit_select(31-self.insn.BI, width=1).eq(1), + crb.eq(self.pfv.cr.r_data.bit_select(31-self.insn.BI, width=1)), + + self.pfv.rt.index.eq(self.insn.RT), + self.pfv.rt.w_stb.eq(1), + ] + + if isinstance(self.insn, SETBC): + m.d.comb += self.pfv.rt.w_data.eq(crb) + if isinstance(self.insn, SETBCR): + m.d.comb += self.pfv.rt.w_data.eq(~crb) + if isinstance(self.insn, SETNBC): + m.d.comb += self.pfv.rt.w_data.eq(Mux(crb, -1, 0)) + if isinstance(self.insn, SETNBCR): + m.d.comb += self.pfv.rt.w_data.eq(Mux(crb, 0, -1)) + else: assert False