checks.insn: add checks for compare instructions.

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

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)

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

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