From fee59d225749665d34dea4f60267d39a8552d1d4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jean-Fran=C3=A7ois=20Nguyen?= Date: Wed, 25 May 2022 19:49:06 +0200 Subject: [PATCH] checks.insn: add checks for CR logical instructions. --- power_fv/checks/insn/_cr.py | 117 ++++++++++++++++++++++++++++++++++ power_fv/checks/insn/_fmt.py | 25 +++++++- power_fv/checks/insn/_insn.py | 11 ++++ power_fv/checks/insn/all.py | 12 ++++ 4 files changed, 164 insertions(+), 1 deletion(-) create mode 100644 power_fv/checks/insn/_cr.py diff --git a/power_fv/checks/insn/_cr.py b/power_fv/checks/insn/_cr.py new file mode 100644 index 0000000..aee8d5e --- /dev/null +++ b/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 diff --git a/power_fv/checks/insn/_fmt.py b/power_fv/checks/insn/_fmt.py index 1d898bb..14a1322 100644 --- a/power_fv/checks/insn/_fmt.py +++ b/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) diff --git a/power_fv/checks/insn/_insn.py b/power_fv/checks/insn/_insn.py index ed17c90..7799bc5 100644 --- a/power_fv/checks/insn/_insn.py +++ b/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 diff --git a/power_fv/checks/insn/all.py b/power_fv/checks/insn/all.py index 95d17e0..4ee9080 100644 --- a/power_fv/checks/insn/all.py +++ b/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