diff --git a/power_fv/checks/__init__.py b/power_fv/checks/__init__.py index a2dccb0..6be9fc6 100644 --- a/power_fv/checks/__init__.py +++ b/power_fv/checks/__init__.py @@ -1 +1,2 @@ from .unique import * +from .ia_fwd import * diff --git a/power_fv/checks/ia_fwd.py b/power_fv/checks/ia_fwd.py new file mode 100644 index 0000000..e76a7d8 --- /dev/null +++ b/power_fv/checks/ia_fwd.py @@ -0,0 +1,74 @@ +from amaranth import * +from amaranth.asserts import * + +from .. import pfv + + +__all__ = ["IAForwardCheck", "IAForwardCover"] + + +class IAForwardCheck(Elaboratable): + """IA forward check. + + Given two instructions retiring in order, check that the NIA of the first matches the CIA + of the second. + """ + def __init__(self): + self.pre = Signal() + self.post = Signal() + self.pfv = pfv.Interface() + + def elaborate(self, platform): + m = Module() + + pred_order = AnyConst(self.pfv.order.width) + pred_stb = Signal() + pred_nia = Signal.like(self.pfv.nia) + + with m.If(self.pfv.stb & (self.pfv.order == pred_order)): + m.d.sync += [ + pred_stb.eq(1), + pred_nia.eq(self.pfv.nia) + ] + + with m.If(self.post): + m.d.sync += [ + Assume(self.pfv.stb), + Assume(self.pfv.order == pred_order + 1), + Assume(self.pfv.order > 0), + Assert(pred_stb.implies(self.pfv.cia == pred_nia)), + ] + + return m + + +class IAForwardCover(Elaboratable): + def __init__(self): + self.pre = Signal() + self.post = Signal() + self.pfv = pfv.Interface() + + def elaborate(self, platform): + m = Module() + + insn_count = Signal(range(4)) + pred_branch = Signal() + + with m.If(self.pfv.stb): + m.d.sync += [ + insn_count .eq(insn_count + 1), + pred_branch.eq(self.pfv.nia != (self.pfv.cia + 4)), + ] + + cover_1 = Signal() + cover_2 = Signal() + + m.d.comb += [ + cover_1.eq((insn_count > 1) & pred_branch), + cover_2.eq(cover_1 & self.pfv.stb), + + Cover(cover_1), + Cover(cover_2), + ] + + return m