checks.insn: add checks for CR logical instructions.

power_fv/checks/insn/_cr.py

@@ -0,0 +1,117 @@
+from amaranth import *
+from amaranth.asserts import *
+
+from .. import PowerFVCheck
+from ... import pfv, tb
+
+from ._fmt  import *
+from ._insn import *
+
+
+__all__ = ["CRSpec", "CRCheck"]
+
+
+class CRSpec(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),
+            ]
+
+        # CR
+
+        spec_cr_r_stb  = Signal( 8)
+        spec_cr_w_stb  = Signal( 8)
+        spec_cr_w_data = Signal(32)
+
+        if isinstance(spec_insn, (Instruction_XL_crl)):
+
+            ba_r_field = Signal(4)
+            bb_r_field = Signal(4)
+            bt_r_field = Signal(4)
+            ba_r_bit   = Signal()
+            bb_r_bit   = Signal()
+            bt_w_bit   = Signal()
+
+            m.d.comb += [
+                ba_r_field.eq(self.pfv.cr.r_data[::-1].word_select(spec_insn.ba[2:], width=4)),
+                bb_r_field.eq(self.pfv.cr.r_data[::-1].word_select(spec_insn.bb[2:], width=4)),
+                bt_r_field.eq(self.pfv.cr.r_data[::-1].word_select(spec_insn.bt[2:], width=4)),
+
+                ba_r_bit.eq(ba_r_field.bit_select(spec_insn.ba[:2], width=1)),
+                bb_r_bit.eq(bb_r_field.bit_select(spec_insn.bb[:2], width=1)),
+            ]
+
+            if isinstance(spec_insn, CRAND):
+                m.d.comb += bt_w_bit.eq(ba_r_bit & bb_r_bit)
+            elif isinstance(spec_insn, CROR):
+                m.d.comb += bt_w_bit.eq(ba_r_bit | bb_r_bit)
+            elif isinstance(spec_insn, CRNAND):
+                m.d.comb += bt_w_bit.eq(~(ba_r_bit & bb_r_bit))
+            elif isinstance(spec_insn, CRXOR):
+                m.d.comb += bt_w_bit.eq(ba_r_bit ^ bb_r_bit)
+            elif isinstance(spec_insn, CRNOR):
+                m.d.comb += bt_w_bit.eq(~(ba_r_bit | bb_r_bit))
+            elif isinstance(spec_insn, CRANDC):
+                m.d.comb += bt_w_bit.eq(ba_r_bit & ~bb_r_bit)
+            elif isinstance(spec_insn, CREQV):
+                m.d.comb += bt_w_bit.eq(ba_r_bit == bb_r_bit)
+            elif isinstance(spec_insn, CRORC):
+                m.d.comb += bt_w_bit.eq(ba_r_bit | ~bb_r_bit)
+            else:
+                assert False
+
+            spec_bt_w_field = Signal(4)
+
+            for i, spec_bt_w_bit in enumerate(spec_bt_w_field):
+                bt_r_bit = bt_r_field[i]
+                with m.If(spec_insn.bt[:2] == i):
+                    m.d.comb += spec_bt_w_bit.eq(bt_w_bit)
+                with m.Else():
+                    m.d.comb += spec_bt_w_bit.eq(bt_r_bit)
+
+            m.d.comb += [
+                spec_cr_r_stb[::-1].bit_select(spec_insn.ba[2:], width=1).eq(1),
+                spec_cr_r_stb[::-1].bit_select(spec_insn.bb[2:], width=1).eq(1),
+                spec_cr_w_stb[::-1].bit_select(spec_insn.bt[2:], width=1).eq(1),
+                spec_cr_w_data.eq(Repl(spec_bt_w_field, 8))
+            ]
+        else:
+            assert False
+
+        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(spec_cr_r_stb[i].implies(self.pfv.cr.r_stb[i])),
+                    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)),
+                ]
+
+        return m
+
+
+class CRCheck(PowerFVCheck, name="_insn_cr"):
+    def __init_subclass__(cls, name, insn_cls):
+        super().__init_subclass__(name)
+        cls.insn_cls = insn_cls
+
+    def get_testbench(self, dut, post):
+        tb_spec = CRSpec(self.insn_cls, post)
+        tb_top  = tb.Testbench(tb_spec, dut)
+        return tb_top

power_fv/checks/insn/_fmt.py

@@ -3,7 +3,7 @@ from amaranth.asserts import AnyConst
 from amaranth.hdl.ast import ValueCastable
 
 
-__all__ = ["Instruction_I", "Instruction_B", "Instruction_XL_bc"]
+__all__ = ["Instruction_I", "Instruction_B", "Instruction_XL_bc", "Instruction_XL_crl"]
 
 
 class Instruction_I(ValueCastable):
@@ -71,3 +71,26 @@ class Instruction_XL_bc(ValueCastable):
     @ValueCastable.lowermethod
     def as_value(self):
         return Cat(self.lk, self.xo, self.bh, self._0, self.bi, self.bo, self.po)
+
+
+class Instruction_XL_crl(ValueCastable):
+    po = None
+    bt = None
+    ba = None
+    bb = 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.bt = AnyConst(unsigned(5))
+        self.ba = AnyConst(unsigned(5))
+        self.bb = AnyConst(unsigned(5))
+        self._0 = AnyConst(unsigned(1))
+
+    @ValueCastable.lowermethod
+    def as_value(self):
+        return Cat(self._0, self.xo, self.bb, self.ba, self.bt, self.po)

power_fv/checks/insn/_insn.py

@@ -18,3 +18,14 @@ class BCCTR  (_fmt.Instruction_XL_bc, po=19, xo=528, lk=0): pass
 class BCCTRL (_fmt.Instruction_XL_bc, po=19, xo=528, lk=1): pass
 class BCTAR  (_fmt.Instruction_XL_bc, po=19, xo=560, lk=0): pass
 class BCTARL (_fmt.Instruction_XL_bc, po=19, xo=560, lk=1): pass
+
+# CR
+
+class CRAND  (_fmt.Instruction_XL_crl, po=19, xo=257): pass
+class CROR   (_fmt.Instruction_XL_crl, po=19, xo=449): pass
+class CRNAND (_fmt.Instruction_XL_crl, po=19, xo=225): pass
+class CRXOR  (_fmt.Instruction_XL_crl, po=19, xo=193): pass
+class CRNOR  (_fmt.Instruction_XL_crl, po=19, xo= 33): pass
+class CRANDC (_fmt.Instruction_XL_crl, po=19, xo=129): pass
+class CREQV  (_fmt.Instruction_XL_crl, po=19, xo=289): pass
+class CRORC  (_fmt.Instruction_XL_crl, po=19, xo=417): pass

power_fv/checks/insn/all.py

@@ -1,5 +1,6 @@
 from . import _insn
 from ._branch import BranchCheck
+from ._cr import CRCheck
 
 # Branches
 
@@ -19,3 +20,14 @@ class BCCTR  (BranchCheck, name="insn_bcctr",  insn_cls=_insn.BCCTR ): pass
 class BCCTRL (BranchCheck, name="insn_bcctrl", insn_cls=_insn.BCCTRL): pass
 class BCTAR  (BranchCheck, name="insn_bctar",  insn_cls=_insn.BCTAR ): pass
 class BCTARL (BranchCheck, name="insn_bctarl", insn_cls=_insn.BCTARL): pass
+
+# CR
+
+class CRAND  (CRCheck, name="insn_crand",  insn_cls=_insn.CRAND ): pass
+class CROR   (CRCheck, name="insn_cror",   insn_cls=_insn.CROR  ): pass
+class CRNAND (CRCheck, name="insn_crnand", insn_cls=_insn.CRNAND): pass
+class CRXOR  (CRCheck, name="insn_crxor",  insn_cls=_insn.CRXOR ): pass
+class CRNOR  (CRCheck, name="insn_crnor",  insn_cls=_insn.CRNOR ): pass
+class CRANDC (CRCheck, name="insn_crandc", insn_cls=_insn.CRANDC): pass
+class CREQV  (CRCheck, name="insn_creqv",  insn_cls=_insn.CREQV ): pass
+class CRORC  (CRCheck, name="insn_crorc",  insn_cls=_insn.CRORC ): pass