From 8cf56ab5dc1940a53a2f45bd70b138a27bd454cf Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jean-Fran=C3=A7ois=20Nguyen?= Date: Tue, 31 May 2022 23:32:46 +0200 Subject: [PATCH] checks.insn: add checks for MTSPR and MFSPR instructions. --- power_fv/checks/insn/_fmt.py | 30 +++++++ power_fv/checks/insn/_insn.py | 5 ++ power_fv/checks/insn/_spr.py | 165 ++++++++++++++++++++++++++++++++++ power_fv/checks/insn/all.py | 6 ++ 4 files changed, 206 insertions(+) create mode 100644 power_fv/checks/insn/_spr.py diff --git a/power_fv/checks/insn/_fmt.py b/power_fv/checks/insn/_fmt.py index b0b87b5..a117947 100644 --- a/power_fv/checks/insn/_fmt.py +++ b/power_fv/checks/insn/_fmt.py @@ -9,6 +9,7 @@ __all__ = [ "Instruction_D_cmp", "Instruction_X_cmp", "Instruction_XL_bc", "Instruction_XL_crl", "Instruction_XL_crf", + "Instruction_XFX_spr", ] @@ -184,3 +185,32 @@ class Instruction_X_cmp(ValueCastable): @ValueCastable.lowermethod def as_value(self): return Cat(self._1, self.xo, self.rb, self.ra, self.l, self._0, self.bf, self.po) + + +class Instruction_XFX_spr(ValueCastable): + po = None + _gpr = None + spr = None + xo = None + _0 = None + + def __init_subclass__(cls, *, po, xo): + cls.po = Const(po, unsigned( 6)) + cls.xo = Const(xo, unsigned(10)) + + def __init__(self): + self._gpr = AnyConst(unsigned( 5)) + self.spr = AnyConst(unsigned(10)) + self._0 = AnyConst(unsigned( 1)) + + @property + def rs(self): + return self._gpr + + @property + def rt(self): + return self._gpr + + @ValueCastable.lowermethod + def as_value(self): + return Cat(self._0, self.xo, self.spr, self._gpr, self.po) diff --git a/power_fv/checks/insn/_insn.py b/power_fv/checks/insn/_insn.py index 094827d..d95b68f 100644 --- a/power_fv/checks/insn/_insn.py +++ b/power_fv/checks/insn/_insn.py @@ -38,3 +38,8 @@ class CMPI (_fmt.Instruction_D_cmp, po=11): pass class CMPLI (_fmt.Instruction_D_cmp, po=10): pass class CMP (_fmt.Instruction_X_cmp, po=31, xo= 0): pass class CMPL (_fmt.Instruction_X_cmp, po=31, xo= 32): pass + +# Move To/From SPR + +class MTSPR (_fmt.Instruction_XFX_spr, po=31, xo=467): pass +class MFSPR (_fmt.Instruction_XFX_spr, po=31, xo=339): pass diff --git a/power_fv/checks/insn/_spr.py b/power_fv/checks/insn/_spr.py new file mode 100644 index 0000000..972044d --- /dev/null +++ b/power_fv/checks/insn/_spr.py @@ -0,0 +1,165 @@ +from amaranth import * +from amaranth.asserts import * + +from .. import PowerFVCheck +from ... import pfv, tb + +from ._fmt import * +from ._insn import * + + +__all__ = ["SPRMoveSpec", "SPRMoveCheck"] + + +class SPRMoveSpec(Elaboratable): + def __init__(self, insn_cls, post): + self.insn_cls = insn_cls + self.pfv = pfv.Interface() + self.post = tb.Trigger(cycle=post) + + def triggers(self): + yield self.post + + # TODO: + # - don't hardcode SPRs, let cores declare what they support. + # - access restrictions (i.e. R/W, privileged) + + def elaborate(self, platform): + m = Module() + + spec_insn = self.insn_cls() + + with m.If(self.post.stb): + m.d.sync += [ + Assume(self.pfv.stb), + Assume(self.pfv.insn[32:] == spec_insn), + ] + + spr = Record([ + ("num", 10), + ("reserved", 1), + ("undefined", 1), + ("pfv", [ + ("r_mask", 64), + ("r_data", 64), + ("w_mask", 64), + ("w_data", 64), + ]), + ]) + + if isinstance(spec_insn, (MTSPR, MFSPR)): + m.d.comb += spr.num.eq(Cat(spec_insn.spr[5:10], spec_insn.spr[0:5])) + else: + assert False + + with m.Switch(spr.num): + for num in range(808, 812): + with m.Case(num): + m.d.comb += spr.reserved.eq(1) + + pfv_sprs = [ + ( 1, self.pfv.xer ), + ( 8, self.pfv.lr ), + ( 9, self.pfv.ctr ), + ( 26, self.pfv.srr0), + ( 27, self.pfv.srr1), + (815, self.pfv.tar ), + ] + + for num, pfv_spr in pfv_sprs: + with m.Case(num): + m.d.comb += [ + spr.pfv.r_mask.eq(pfv_spr.r_mask), + spr.pfv.r_data.eq(pfv_spr.r_data), + spr.pfv.w_mask.eq(pfv_spr.w_mask), + spr.pfv.w_data.eq(pfv_spr.w_data), + ] + + with m.Default(): + m.d.comb += spr.undefined.eq(1) + + with m.If(self.post.stb): + # TODO: turn into assert + m.d.sync += Assume(spr.undefined.implies(self.pfv.intr)) + + # # MSR + # pfv_msr_pr = Signal() + # m.d.comb += pfv_msr_pr.eq(self.pfv.msr.r_data[63 - 49]) + + # with m.If(self.post.stb): + # m.d.sync += Assert(self.pfv.msr.r_mask[63 - 49]) + + # GPR + + spec_rs_r_stb = Signal() + spec_rt_w_stb = Signal() + # spec_rt_w_mask = Signal(64) + spec_rt_w_data = Signal(64) + + if isinstance(spec_insn, MTSPR): + m.d.comb += [ + spec_rs_r_stb.eq(~spr.reserved), + spec_rt_w_stb.eq(0), + ] + + elif isinstance(spec_insn, MFSPR): + m.d.comb += [ + spec_rs_r_stb .eq(0), + spec_rt_w_stb .eq(~spr.reserved), + spec_rt_w_data.eq(spr.pfv.r_data), + ] + + # # In problem state, reserved fields must return 0, so we include them in the mask. + # # In privileged state, reserved fields may return anything. + # with m.If(pfv_msr_pr): + # m.d.comb += spec_rt_w_mask.eq(Repl(1, 64)) + # with m.Else(): + # m.d.comb += spec_rt_w_mask.eq(spr.pfv.r_mask) + + else: + assert False + + with m.If(self.post.stb & ~self.pfv.intr): + m.d.sync += [ + Assert(spec_rs_r_stb.implies(self.pfv.rs.r_stb)), + Assert(self.pfv.rt.w_stb == spec_rt_w_stb), + Assert(spec_rt_w_stb.implies(self.pfv.rt.w_data == (spr.pfv.r_data & spr.pfv.r_mask))), + ] + # with m.If(spec_rt_w_stb): + # for i in range(64): + # with m.If(spr.pfv.w_mask[i]): + # m.d.sync += Assert(self.pfv.rt.w_data[i] == spec_rt_w_data[i]) + + # SPR + + spec_spr_w_stb = Signal() + spec_spr_w_data = Signal(64) + + if isinstance(spec_insn, MTSPR): + m.d.comb += [ + spec_spr_w_stb .eq(1), + spec_spr_w_data.eq(self.pfv.rs.r_data), + ] + elif isinstance(spec_insn, MFSPR): + m.d.comb += spec_spr_w_stb.eq(0) + else: + assert False + + with m.If(self.post.stb & ~self.pfv.intr): + m.d.sync += [ + Assert(spec_spr_w_stb == spr.pfv.w_mask.any()), + Assert((spr.pfv.w_data & spr.pfv.w_mask) == (spec_spr_w_data & spr.pfv.w_mask)), + ] + + return m + + +class SPRMoveCheck(PowerFVCheck, name="_insn_spr"): + def __init_subclass__(cls, name, insn_cls): + super().__init_subclass__(name) + cls.insn_cls = insn_cls + + def get_testbench(self, dut, post): + tb_spec = SPRMoveSpec(self.insn_cls, post) + tb_top = tb.Testbench(tb_spec, dut) + return tb_top diff --git a/power_fv/checks/insn/all.py b/power_fv/checks/insn/all.py index 514c567..7154cba 100644 --- a/power_fv/checks/insn/all.py +++ b/power_fv/checks/insn/all.py @@ -2,6 +2,7 @@ from . import _insn from ._branch import BranchCheck from ._cr import CRCheck from ._compare import CompareCheck +from ._spr import SPRMoveCheck # Branches @@ -42,3 +43,8 @@ class CMPI (CompareCheck, name="insn_cmpi", insn_cls=_insn.CMPI ): pass class CMPLI (CompareCheck, name="insn_cmpli", insn_cls=_insn.CMPLI ): pass class CMP (CompareCheck, name="insn_cmp", insn_cls=_insn.CMP ): pass class CMPL (CompareCheck, name="insn_cmpl", insn_cls=_insn.CMPL ): pass + +# Move To/From SPR + +class MTSPR (SPRMoveCheck, name="insn_mtspr", insn_cls=_insn.MTSPR): pass +class MFSPR (SPRMoveCheck, name="insn_mfspr", insn_cls=_insn.MFSPR): pass