diff --git a/power_fv/checks/__init__.py b/power_fv/checks/__init__.py index f68fdfc..6d2c528 100644 --- a/power_fv/checks/__init__.py +++ b/power_fv/checks/__init__.py @@ -1,3 +1,4 @@ +from .cr import * from .gpr import * from .ia_fwd import * from .unique import * diff --git a/power_fv/checks/cr.py b/power_fv/checks/cr.py new file mode 100644 index 0000000..b9312ac --- /dev/null +++ b/power_fv/checks/cr.py @@ -0,0 +1,57 @@ +from amaranth import * +from amaranth.asserts import * + +from .. import pfv + + +__all__ = ["CRCheck"] + + +class CRCheck(Elaboratable): + """Condition Register check. + + Checks that reads from CR fields are consistent with the last value that was written to them. + """ + def __init__(self): + self.pre = Signal() + self.post = Signal() + self.pfv = pfv.Interface() + + def elaborate(self, platform): + m = Module() + + spec_order = AnyConst(self.pfv.order.width) + + cr = Array(Record([ + ("written", 1), + ("shadow", 4), + ], name=f"cr{i}") for i in range(8)) + + cr_written_any = 0 + + with m.If(self.pfv.stb & (self.pfv.order <= spec_order)): + for i, cr_field in enumerate(cr): + pfv_cr_field = getattr(self.pfv, f"cr{i}") + + with m.If(pfv_cr_field.w_stb): + m.d.sync += [ + cr_field.written.eq(1), + cr_field.shadow .eq(pfv_cr_field.w_data), + ] + + cr_written_any |= cr_field.written + + with m.If(self.post): + m.d.sync += [ + Assume(Past(self.pfv.stb)), + Assume(Past(self.pfv.order) == spec_order), + Assume(cr_written_any), + ] + + for i, cr_field in enumerate(cr): + pfv_cr_field = getattr(self.pfv, f"cr{i}") + + with m.If(Past(pfv_cr_field.r_stb)): + m.d.sync += Assert(Past(pfv_cr_field.r_data) == Past(cr_field.shadow)) + + return m