From 58bef1a741bcf108f0040e5a295e10639a7f0e2f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jean-Fran=C3=A7ois=20Nguyen?= Date: Mon, 16 May 2022 18:04:51 +0200 Subject: [PATCH] checks: add checks for branch instructions. --- cores/microwatt/run.py | 17 +++ power_fv/checks/_branch.py | 210 +++++++++++++++++++++++++++++++++ power_fv/checks/insn_b.py | 9 ++ power_fv/checks/insn_ba.py | 9 ++ power_fv/checks/insn_bc.py | 9 ++ power_fv/checks/insn_bca.py | 9 ++ power_fv/checks/insn_bcctr.py | 9 ++ power_fv/checks/insn_bcctrl.py | 9 ++ power_fv/checks/insn_bcl.py | 9 ++ power_fv/checks/insn_bcla.py | 10 ++ power_fv/checks/insn_bclr.py | 9 ++ power_fv/checks/insn_bclrl.py | 9 ++ power_fv/checks/insn_bctar.py | 9 ++ power_fv/checks/insn_bctarl.py | 9 ++ power_fv/checks/insn_bl.py | 9 ++ power_fv/checks/insn_bla.py | 9 ++ power_fv/insn.py | 88 ++++++++++++++ 17 files changed, 442 insertions(+) create mode 100644 power_fv/checks/_branch.py create mode 100644 power_fv/checks/insn_b.py create mode 100644 power_fv/checks/insn_ba.py create mode 100644 power_fv/checks/insn_bc.py create mode 100644 power_fv/checks/insn_bca.py create mode 100644 power_fv/checks/insn_bcctr.py create mode 100644 power_fv/checks/insn_bcctrl.py create mode 100644 power_fv/checks/insn_bcl.py create mode 100644 power_fv/checks/insn_bcla.py create mode 100644 power_fv/checks/insn_bclr.py create mode 100644 power_fv/checks/insn_bclrl.py create mode 100644 power_fv/checks/insn_bctar.py create mode 100644 power_fv/checks/insn_bctarl.py create mode 100644 power_fv/checks/insn_bl.py create mode 100644 power_fv/checks/insn_bla.py create mode 100644 power_fv/insn.py diff --git a/cores/microwatt/run.py b/cores/microwatt/run.py index 34fbf16..4782c23 100644 --- a/cores/microwatt/run.py +++ b/cores/microwatt/run.py @@ -98,6 +98,23 @@ if __name__ == "__main__": ("gpr", None, 15), ("cr", None, 15), ("spr", None, 15), + + ("insn_b", None, 15), + ("insn_ba", None, 15), + ("insn_bl", None, 15), + ("insn_bla", None, 15), + ("insn_bc", None, 15), + ("insn_bca", None, 15), + ("insn_bcla", None, 15), + + # TODO: + #("insn_bcl", None, 15), + #("insn_bclr", None, 15), + #("insn_bclrl", None, 15), + #("insn_bcctr", None, 15), + #("insn_bcctrl", None, 15), + #("insn_bctar", None, 15), + #("insn_bctarl", None, 15), ] with multiprocessing.Pool(processes=args.jobs) as pool: diff --git a/power_fv/checks/_branch.py b/power_fv/checks/_branch.py new file mode 100644 index 0000000..45fcd0e --- /dev/null +++ b/power_fv/checks/_branch.py @@ -0,0 +1,210 @@ +from amaranth import * +from amaranth.asserts import * + +from .. import pfv +from ..insn import * + + +__all__ = ["Check"] + + +class Check(Elaboratable): + _insn_cls = None + + def __init_subclass__(cls, *, insn_cls): + cls._insn_cls = insn_cls + + def __init__(self): + self.pfv = pfv.Interface() + self.trig = Record([ + ("pre", 1), + ("post", 1), + ]) + + def elaborate(self, platform): + m = Module() + + # TODO: + # - support MSR (stop assuming 64-bit mode) + # - support interrupts (detect illegal forms) + + spec_insn = self._insn_cls() + + with m.If(self.trig.post): + m.d.sync += [ + Assume(self.pfv.stb), + Assume(self.pfv.insn[32:] == spec_insn), + ] + + if isinstance(spec_insn, (Instruction_B, Instruction_XL_b)): + bo_valid_patterns = [ + "0000-", + "0001-", + "001--", + "0100-", + "0101-", + "011--", + "1-00-", + "1-01-" + ] + if not isinstance(spec_insn, Instruction_B): + # "Branch always" mnemonics are undefined for B-form conditional branches. + # (Appendix C.2.2, Book I) + bo_valid_patterns.append("1-1--") + + bo_valid = Signal() + m.d.comb += bo_valid.eq(spec_insn.bo.matches(*bo_valid_patterns)) + + # FIXME(microwatt,interrupts): turn this into an assert + with m.If(self.trig.post): + m.d.sync += Assume(bo_valid | self.pfv.intr) + + # NIA + + spec_nia = Signal(unsigned(64)) + taken = Signal() + offset = Signal(signed(62)) + + if isinstance(spec_insn, Instruction_I): + m.d.comb += [ + taken .eq(1), + offset.eq(spec_insn.li) + ] + + elif isinstance(spec_insn, (Instruction_B, Instruction_XL_b)): + cond_bit = Signal() + ctr_any = Signal() + cond_ok = Signal() + ctr_ok = Signal() + + m.d.comb += [ + cond_bit.eq(self.pfv.cr.r_data[::-1].bit_select(spec_insn.bi, width=1)), + ctr_any .eq(self.pfv.ctr.w_data.any()), + cond_ok .eq(spec_insn.bo[4] | (spec_insn.bo[3] == cond_bit)), + ctr_ok .eq(spec_insn.bo[2] | (ctr_any ^ spec_insn.bo[1])), + ] + + if isinstance(spec_insn, Instruction_XL_b) and spec_insn.xo.value == 528: # bcctr/bcctrl + m.d.comb += taken.eq(cond_ok) + else: + m.d.comb += taken.eq(cond_ok & ctr_ok) + + if isinstance(spec_insn, Instruction_B): + m.d.comb += offset.eq(spec_insn.bd) + elif spec_insn.xo.value == 16: # bclr/bclrl + m.d.comb += offset.eq(self.pfv.lr .r_data[:61]) + elif spec_insn.xo.value == 528: # bcctr/bcctrl + m.d.comb += offset.eq(self.pfv.ctr.r_data[:61]) + elif spec_insn.xo.value == 560: # bctar/bctarl + m.d.comb += offset.eq(self.pfv.tar.r_data[:61]) + else: + assert False + + else: + assert False + + with m.If(taken): + if isinstance(spec_insn, (Instruction_I, Instruction_B)) and spec_insn.aa.value == 0: + m.d.comb += spec_nia.eq(self.pfv.cia + (offset << 2)) + else: + m.d.comb += spec_nia.eq(offset << 2) + with m.Else(): + m.d.comb += spec_nia.eq(self.pfv.cia + 4) + + with m.If(self.trig.post & ~self.pfv.intr): + m.d.sync += Assert(self.pfv.nia == spec_nia) + + # CR + + spec_cr_r_stb = Signal(8) + + if isinstance(spec_insn, Instruction_I): + m.d.comb += spec_cr_r_stb.eq(0) + elif isinstance(spec_insn, (Instruction_B, Instruction_XL_b)): + m.d.comb += spec_cr_r_stb[::-1].bit_select(spec_insn.bi[2:], width=1).eq(1) + else: + assert False + + with m.If(self.trig.post & ~self.pfv.intr): + for i, spec_cr_r_stb_bit in enumerate(spec_cr_r_stb): + pfv_cr_r_stb_bit = self.pfv.cr.r_stb[i] + m.d.sync += Assert(spec_cr_r_stb_bit.implies(pfv_cr_r_stb_bit)) + + # LR + + spec_lr_r_stb = Signal() + spec_lr_w_stb = Signal() + spec_lr_w_data = Signal(64) + + if isinstance(spec_insn, (Instruction_I, Instruction_B)): + m.d.comb += spec_lr_r_stb.eq(0) + elif isinstance(spec_insn, (Instruction_XL_b)): + m.d.comb += spec_lr_r_stb.eq(spec_insn.xo == 16) # bclr/bclrl + else: + assert False + + m.d.comb += [ + spec_lr_w_stb .eq(spec_insn.lk), + spec_lr_w_data.eq(self.pfv.cia + 4), + ] + + with m.If(self.trig.post & ~self.pfv.intr): + m.d.sync += [ + Assert(self.pfv.lr.r_stb == spec_lr_r_stb), + Assert(self.pfv.lr.w_stb == spec_lr_w_stb), + Assert(self.pfv.lr.w_stb.implies(self.pfv.lr.w_data == spec_lr_w_data)), + ] + + # CTR + + spec_ctr_r_stb = Signal() + spec_ctr_w_stb = Signal() + spec_ctr_w_data = Signal(64) + + if isinstance(spec_insn, Instruction_I): + m.d.comb += spec_ctr_r_stb.eq(0) + elif isinstance(spec_insn, Instruction_B): + m.d.comb += spec_ctr_r_stb.eq(~spec_insn.bo[2]) + elif isinstance(spec_insn, (Instruction_B, Instruction_XL_b)): + m.d.comb += spec_ctr_r_stb.eq(1) + else: + assert False + + if isinstance(spec_insn, Instruction_I): + m.d.comb += spec_ctr_w_stb.eq(0) + elif isinstance(spec_insn, Instruction_B): + m.d.comb += spec_ctr_w_stb.eq(~spec_insn.bo[2]) + elif isinstance(spec_insn, Instruction_XL_b): + if spec_insn.xo.value == 528: # bcctr/bcctrl + m.d.comb += spec_ctr_w_stb.eq(0) + else: + m.d.comb += spec_ctr_w_stb.eq(~spec_insn.bo[2]) + else: + assert False + + m.d.comb += spec_ctr_w_data.eq(self.pfv.ctr.r_data - 1) + + with m.If(self.trig.post & ~self.pfv.intr): + m.d.sync += [ + Assert(self.pfv.ctr.r_stb == spec_ctr_r_stb), + Assert(self.pfv.ctr.w_stb == spec_ctr_w_stb), + Assert(self.pfv.ctr.w_stb.implies(self.pfv.ctr.w_data == spec_ctr_w_data)), + ] + + # TAR + + spec_tar_r_stb = Signal() + + if isinstance(spec_insn, (Instruction_I, Instruction_B)): + m.d.comb += spec_tar_r_stb.eq(0) + elif isinstance(spec_insn, (Instruction_XL_b)): + m.d.comb += spec_tar_r_stb.eq(spec_insn.xo == 560) # bctar/bctarl + else: + assert False + + with m.If(self.trig.post & ~self.pfv.intr): + m.d.sync += [ + Assert(self.pfv.tar.r_stb == spec_tar_r_stb), + ] + + return m diff --git a/power_fv/checks/insn_b.py b/power_fv/checks/insn_b.py new file mode 100644 index 0000000..5a3a830 --- /dev/null +++ b/power_fv/checks/insn_b.py @@ -0,0 +1,9 @@ +from . import _branch +from .. import insn + + +__all__ = ["Check"] + + +class Check(_branch.Check, insn_cls=insn.B): + pass diff --git a/power_fv/checks/insn_ba.py b/power_fv/checks/insn_ba.py new file mode 100644 index 0000000..03b4ddc --- /dev/null +++ b/power_fv/checks/insn_ba.py @@ -0,0 +1,9 @@ +from . import _branch +from .. import insn + + +__all__ = ["Check"] + + +class Check(_branch.Check, insn_cls=insn.BA): + pass diff --git a/power_fv/checks/insn_bc.py b/power_fv/checks/insn_bc.py new file mode 100644 index 0000000..470e64b --- /dev/null +++ b/power_fv/checks/insn_bc.py @@ -0,0 +1,9 @@ +from . import _branch +from .. import insn + + +__all__ = ["Check"] + + +class Check(_branch.Check, insn_cls=insn.BC): + pass diff --git a/power_fv/checks/insn_bca.py b/power_fv/checks/insn_bca.py new file mode 100644 index 0000000..ba31123 --- /dev/null +++ b/power_fv/checks/insn_bca.py @@ -0,0 +1,9 @@ +from . import _branch +from .. import insn + + +__all__ = ["Check"] + + +class Check(_branch.Check, insn_cls=insn.BCA): + pass diff --git a/power_fv/checks/insn_bcctr.py b/power_fv/checks/insn_bcctr.py new file mode 100644 index 0000000..cdc0790 --- /dev/null +++ b/power_fv/checks/insn_bcctr.py @@ -0,0 +1,9 @@ +from . import _branch +from .. import insn + + +__all__ = ["Check"] + + +class Check(_branch.Check, insn_cls=insn.BCCTR): + pass diff --git a/power_fv/checks/insn_bcctrl.py b/power_fv/checks/insn_bcctrl.py new file mode 100644 index 0000000..96725fc --- /dev/null +++ b/power_fv/checks/insn_bcctrl.py @@ -0,0 +1,9 @@ +from . import _branch +from .. import insn + + +__all__ = ["Check"] + + +class Check(_branch.Check, insn_cls=insn.BCTRL): + pass diff --git a/power_fv/checks/insn_bcl.py b/power_fv/checks/insn_bcl.py new file mode 100644 index 0000000..4d287f2 --- /dev/null +++ b/power_fv/checks/insn_bcl.py @@ -0,0 +1,9 @@ +from . import _branch +from .. import insn + + +__all__ = ["Check"] + + +class Check(_branch.Check, insn_cls=insn.BCL): + pass diff --git a/power_fv/checks/insn_bcla.py b/power_fv/checks/insn_bcla.py new file mode 100644 index 0000000..960d28e --- /dev/null +++ b/power_fv/checks/insn_bcla.py @@ -0,0 +1,10 @@ +from . import _branch + +from .. import insn + + +__all__ = ["Check"] + + +class Check(_branch.Check, insn_cls=insn.BCLA): + pass diff --git a/power_fv/checks/insn_bclr.py b/power_fv/checks/insn_bclr.py new file mode 100644 index 0000000..a6e639f --- /dev/null +++ b/power_fv/checks/insn_bclr.py @@ -0,0 +1,9 @@ +from . import _branch +from .. import insn + + +__all__ = ["Check"] + + +class Check(_branch.Check, insn_cls=insn.BCLR): + pass diff --git a/power_fv/checks/insn_bclrl.py b/power_fv/checks/insn_bclrl.py new file mode 100644 index 0000000..236ea26 --- /dev/null +++ b/power_fv/checks/insn_bclrl.py @@ -0,0 +1,9 @@ +from . import _branch +from .. import insn + + +__all__ = ["Check"] + + +class Check(_branch.Check, insn_cls=insn.BCLRL): + pass diff --git a/power_fv/checks/insn_bctar.py b/power_fv/checks/insn_bctar.py new file mode 100644 index 0000000..df26f1e --- /dev/null +++ b/power_fv/checks/insn_bctar.py @@ -0,0 +1,9 @@ +from . import _branch +from .. import insn + + +__all__ = ["Check"] + + +class Check(_branch.Check, insn_cls=insn.BCTAR): + pass diff --git a/power_fv/checks/insn_bctarl.py b/power_fv/checks/insn_bctarl.py new file mode 100644 index 0000000..908056c --- /dev/null +++ b/power_fv/checks/insn_bctarl.py @@ -0,0 +1,9 @@ +from . import _branch +from .. import insn + + +__all__ = ["Check"] + + +class Check(_branch.Check, insn_cls=insn.BCTARL): + pass diff --git a/power_fv/checks/insn_bl.py b/power_fv/checks/insn_bl.py new file mode 100644 index 0000000..05fe1c1 --- /dev/null +++ b/power_fv/checks/insn_bl.py @@ -0,0 +1,9 @@ +from . import _branch +from .. import insn + + +__all__ = ["Check"] + + +class Check(_branch.Check, insn_cls=insn.BL): + pass diff --git a/power_fv/checks/insn_bla.py b/power_fv/checks/insn_bla.py new file mode 100644 index 0000000..a34d516 --- /dev/null +++ b/power_fv/checks/insn_bla.py @@ -0,0 +1,9 @@ +from . import _branch +from .. import insn + + +__all__ = ["Check"] + + +class Check(_branch.Check, insn_cls=insn.BLA): + pass diff --git a/power_fv/insn.py b/power_fv/insn.py new file mode 100644 index 0000000..c00de79 --- /dev/null +++ b/power_fv/insn.py @@ -0,0 +1,88 @@ +from amaranth import * +from amaranth.asserts import AnyConst +from amaranth.hdl.ast import ValueCastable + + +class Instruction_I(ValueCastable): + po = None + li = None + aa = None + lk = None + + def __init_subclass__(cls, *, po, aa, lk): + cls.po = Const(po, unsigned(6)) + cls.aa = Const(aa, 1) + cls.lk = Const(lk, 1) + + def __init__(self): + self.li = AnyConst(signed(24)) + + @ValueCastable.lowermethod + def as_value(self): + return Cat(self.lk, self.aa, self.li, self.po) + + +class Instruction_B(ValueCastable): + po = None + bo = None + bi = None + bd = None + aa = None + lk = None + + def __init_subclass__(cls, *, po, aa, lk): + cls.po = Const(po, unsigned(6)) + cls.aa = Const(aa, 1) + cls.lk = Const(lk, 1) + + def __init__(self): + self.bo = AnyConst(unsigned( 5)) + self.bi = AnyConst(unsigned( 5)) + self.bd = AnyConst( signed(14)) + + @ValueCastable.lowermethod + def as_value(self): + return Cat(self.lk, self.aa, self.bd, self.bi, self.bo, self.po) + + +class Instruction_XL_b(ValueCastable): + po = None + bo = None + bi = None + _0 = None + bh = None + xo = None + lk = None + + def __init_subclass__(cls, *, po, xo, lk): + cls.po = Const(po, unsigned(6)) + cls.xo = Const(xo, unsigned(9)) + cls.lk = Const(1) + + def __init__(self): + self.bo = AnyConst(unsigned(5)) + self.bi = AnyConst(unsigned(5)) + self._0 = AnyConst(unsigned(3)) + self.bh = AnyConst(unsigned(2)) + + @ValueCastable.lowermethod + def as_value(self): + return Cat(self.lk, self.xo, self.bh, self._0, self.bi, self.bo, self.po) + + +class B (Instruction_I, po=18, aa=0, lk=0): pass +class BA (Instruction_I, po=18, aa=1, lk=0): pass +class BL (Instruction_I, po=18, aa=0, lk=1): pass +class BLA (Instruction_I, po=18, aa=1, lk=1): pass + +class BC (Instruction_B, po=16, aa=0, lk=0): pass +class BCA (Instruction_B, po=16, aa=1, lk=0): pass +class BCL (Instruction_B, po=16, aa=0, lk=1): pass +class BCLA (Instruction_B, po=16, aa=1, lk=1): pass + +class BCLR (Instruction_XL_b, po=19, xo= 16, lk=0): pass +class BCLRL (Instruction_XL_b, po=19, xo= 16, lk=1): pass +class BCCTR (Instruction_XL_b, po=19, xo=528, lk=0): pass +class BCCTRL (Instruction_XL_b, po=19, xo=528, lk=1): pass +class BCTAR (Instruction_XL_b, po=19, xo=560, lk=0): pass +class BCTARL (Instruction_XL_b, po=19, xo=560, lk=1): pass