From 692e8ec7c415f520ea58e90ba07cca68f843c788 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jean-Fran=C3=A7ois=20Nguyen?= Date: Tue, 31 May 2022 23:29:15 +0200 Subject: [PATCH] checks.insn: add checks for compare instructions. --- power_fv/checks/insn/_compare.py | 152 +++++++++++++++++++++++++++++++ power_fv/checks/insn/_fmt.py | 59 ++++++++++++ power_fv/checks/insn/_insn.py | 7 ++ power_fv/checks/insn/all.py | 9 ++ 4 files changed, 227 insertions(+) create mode 100644 power_fv/checks/insn/_compare.py diff --git a/power_fv/checks/insn/_compare.py b/power_fv/checks/insn/_compare.py new file mode 100644 index 0000000..fe07860 --- /dev/null +++ b/power_fv/checks/insn/_compare.py @@ -0,0 +1,152 @@ +from amaranth import * +from amaranth.asserts import * + +from .. import PowerFVCheck +from ... import pfv, tb + +from ._fmt import * +from ._insn import * + + +__all__ = ["CompareSpec", "CompareCheck"] + + +class CompareSpec(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 + + 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), + ] + + # GPRs + + spec_ra_r_stb = Signal() + spec_rb_r_stb = Signal() + + if isinstance(spec_insn, (CMPI, CMPLI, CMP, CMPL)): + m.d.comb += spec_ra_r_stb.eq(1) + else: + assert False + + if isinstance(spec_insn, (CMPI, CMPLI)): + m.d.comb += spec_rb_r_stb.eq(0) + elif isinstance(spec_insn, (CMP, CMPL)): + m.d.comb += spec_rb_r_stb.eq(1) + else: + assert False + + with m.If(self.post.stb & ~self.pfv.intr): + m.d.sync += [ + Assert(self.pfv.ra.r_stb == spec_ra_r_stb), + Assert(self.pfv.rb.r_stb == spec_rb_r_stb), + ] + + # CR + + spec_cr_w_stb = Signal(8) + spec_cr_w_data = Signal(32) + + a = Signal(signed(64)) + b = Signal(signed(64)) + c = Record([("lt", 1), ("gt", 1), ("eq_", 1), ("so", 1)]) + + if isinstance(spec_insn, (CMPI, CMP)): + with m.If(spec_insn.l): + m.d.comb += a.eq(self.pfv.ra.r_data) + with m.Else(): + m.d.comb += a.eq(self.pfv.ra.r_data[:32].as_signed()) + elif isinstance(spec_insn, (CMPL, CMPLI)): + with m.If(spec_insn.l): + m.d.comb += a.eq(self.pfv.ra.r_data) + with m.Else(): + m.d.comb += a.eq(self.pfv.ra.r_data[:32].as_unsigned()) + else: + assert False + + if isinstance(spec_insn, CMPI): + m.d.comb += b.eq(spec_insn.si) + elif isinstance(spec_insn, CMPLI): + m.d.comb += b.eq(spec_insn.ui) + elif isinstance(spec_insn, CMP): + with m.If(spec_insn.l): + m.d.comb += b.eq(self.pfv.rb.r_data) + with m.Else(): + m.d.comb += b.eq(self.pfv.rb.r_data[:32].as_signed()) + elif isinstance(spec_insn, CMPL): + with m.If(spec_insn.l): + m.d.comb += b.eq(self.pfv.rb.r_data) + with m.Else(): + m.d.comb += b.eq(self.pfv.rb.r_data[:32].as_unsigned()) + else: + assert False + + if isinstance(spec_insn, (CMPI, CMP)): + m.d.comb += [ + c.lt.eq(a.as_signed() < b.as_signed()), + c.gt.eq(a.as_signed() > b.as_signed()), + ] + elif isinstance(spec_insn, (CMPLI, CMPL)): + m.d.comb += [ + c.lt.eq(a.as_unsigned() < b.as_unsigned()), + c.gt.eq(a.as_unsigned() > b.as_unsigned()), + ] + else: + assert False + + m.d.comb += [ + c.eq_.eq(a == b), + c.so .eq(self.pfv.xer.r_data[63 - 32]), # XER.SO + ] + + m.d.comb += [ + spec_cr_w_stb[::-1].bit_select(spec_insn.bf, width=1).eq(1), + spec_cr_w_data[::-1].eq(Repl(c, 8)), + ] + + with m.If(self.post.stb & ~self.pfv.intr): + for i in range(8): + spec_cr_w_field = spec_cr_w_data .word_select(i, width=4) + pfv_cr_w_field = self.pfv.cr.w_data.word_select(i, width=4) + + m.d.sync += [ + Assert(self.pfv.cr.w_stb[i] == spec_cr_w_stb[i]), + Assert(spec_cr_w_stb[i].implies(pfv_cr_w_field == spec_cr_w_field)), + ] + + # XER + + spec_xer_r_mask = Signal(64) + + if isinstance(spec_insn, (CMPI, CMPLI, CMP, CMPL)): + m.d.comb += spec_xer_r_mask[63 - 32].eq(1) # XER.SO + else: + assert False + + with m.If(self.post.stb & ~self.pfv.intr): + m.d.sync += Assert((self.pfv.xer.r_mask & spec_xer_r_mask) == spec_xer_r_mask) + + return m + + +class CompareCheck(PowerFVCheck, name="_insn_compare"): + def __init_subclass__(cls, name, insn_cls): + super().__init_subclass__(name) + cls.insn_cls = insn_cls + + def get_testbench(self, dut, post): + tb_spec = CompareSpec(self.insn_cls, post) + tb_top = tb.Testbench(tb_spec, dut) + return tb_top diff --git a/power_fv/checks/insn/_fmt.py b/power_fv/checks/insn/_fmt.py index 548daca..b0b87b5 100644 --- a/power_fv/checks/insn/_fmt.py +++ b/power_fv/checks/insn/_fmt.py @@ -6,6 +6,8 @@ from amaranth.hdl.ast import ValueCastable __all__ = [ "Instruction_I", "Instruction_B", + "Instruction_D_cmp", + "Instruction_X_cmp", "Instruction_XL_bc", "Instruction_XL_crl", "Instruction_XL_crf", ] @@ -125,3 +127,60 @@ class Instruction_XL_crf(ValueCastable): @ValueCastable.lowermethod def as_value(self): return Cat(self._3, self.xo, self._2, self._1, self.bfa, self._0, self.bf, self.po) + + +class Instruction_D_cmp(ValueCastable): + po = None + bf = None + _0 = None + l = None + ra = None + _i = None + + def __init_subclass__(cls, *, po): + cls.po = Const(po, unsigned(6)) + + def __init__(self): + self.bf = AnyConst(unsigned(3)) + self._0 = AnyConst(unsigned(1)) + self.l = AnyConst(unsigned(1)) + self.ra = AnyConst(unsigned(5)) + self._i = AnyConst(16) + + @property + def si(self): + return self._i.as_signed() + + def ui(self): + return self._i.as_unsigned() + + @ValueCastable.lowermethod + def as_value(self): + return Cat(self._i, self.ra, self.l, self._0, self.bf, self.po) + + +class Instruction_X_cmp(ValueCastable): + po = None + bf = None + _0 = None + l = None + ra = None + rb = None + xo = None + _1 = None + + def __init_subclass__(cls, *, po, xo): + cls.po = Const(po, unsigned( 6)) + cls.xo = Const(xo, unsigned(10)) + + def __init__(self): + self.bf = AnyConst(unsigned(3)) + self._0 = AnyConst(unsigned(1)) + self.l = AnyConst(unsigned(1)) + self.ra = AnyConst(unsigned(5)) + self.rb = AnyConst(unsigned(5)) + self._1 = AnyConst(unsigned(1)) + + @ValueCastable.lowermethod + def as_value(self): + return Cat(self._1, self.xo, self.rb, self.ra, self.l, self._0, self.bf, self.po) diff --git a/power_fv/checks/insn/_insn.py b/power_fv/checks/insn/_insn.py index 7ac9218..094827d 100644 --- a/power_fv/checks/insn/_insn.py +++ b/power_fv/checks/insn/_insn.py @@ -31,3 +31,10 @@ class CREQV (_fmt.Instruction_XL_crl, po=19, xo=289): pass class CRORC (_fmt.Instruction_XL_crl, po=19, xo=417): pass class MCRF (_fmt.Instruction_XL_crf, po=19, xo=0): pass + +# Compare + +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 diff --git a/power_fv/checks/insn/all.py b/power_fv/checks/insn/all.py index 200a14c..514c567 100644 --- a/power_fv/checks/insn/all.py +++ b/power_fv/checks/insn/all.py @@ -1,6 +1,8 @@ from . import _insn from ._branch import BranchCheck from ._cr import CRCheck +from ._compare import CompareCheck + # Branches @@ -33,3 +35,10 @@ class CREQV (CRCheck, name="insn_creqv", insn_cls=_insn.CREQV ): pass class CRORC (CRCheck, name="insn_crorc", insn_cls=_insn.CRORC ): pass class MCRF (CRCheck, name="insn_mcrf", insn_cls=_insn.MCRF ): pass + +# Compare + +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