diff --git a/power_fv/checks/cr.py b/power_fv/checks/cr.py index 978ccbc..f5eb977 100644 --- a/power_fv/checks/cr.py +++ b/power_fv/checks/cr.py @@ -48,7 +48,7 @@ class Check(Elaboratable): ] cr_written_any |= cr_field.written - with m.If(self.pfv.stb & (self.pfv.order <= spec_order)): + with m.If(self.pfv.stb & ~self.pfv.intr & (self.pfv.order <= spec_order)): for cr_field in cr_map: with m.If(cr_field.pfv.w_stb): m.d.sync += [ @@ -62,8 +62,9 @@ class Check(Elaboratable): Assume(Past(self.pfv.order) == spec_order), Assume(cr_written_any), ] - for cr_field in cr_map: - with m.If(Past(cr_field.pfv.r_stb)): - m.d.sync += Assert(Past(cr_field.pfv.r_data) == Past(cr_field.shadow)) + with m.If(~Past(self.pfv.intr)): + for cr_field in cr_map: + with m.If(Past(cr_field.pfv.r_stb)): + m.d.sync += Assert(Past(cr_field.pfv.r_data) == Past(cr_field.shadow)) return m diff --git a/power_fv/checks/gpr.py b/power_fv/checks/gpr.py index f0cd5e4..0f98de4 100644 --- a/power_fv/checks/gpr.py +++ b/power_fv/checks/gpr.py @@ -10,9 +10,10 @@ __all__ = ["Check"] class Check(Elaboratable): """General Purpose Registers check. - Checks that reads from GPRs are consistent with the last value that was written to them. - Also checks that simultaneous writes to multiple GPRs by the same instruction (e.g. a load - with update) do not target the same register. + Checks that: + * reads from a GPR are consistent with the last value that was written to it; + * writes to multiple GPRs by a single instruction (e.g. load with update) do not target the + same register. """ def __init__(self): self.pfv = pfv.Interface() @@ -47,7 +48,7 @@ class Check(Elaboratable): gpr_rt_write.eq(self.pfv.rt.w_stb & (self.pfv.rt.index == spec_gpr_index)), ] - with m.If(self.pfv.stb & (self.pfv.order <= spec_order)): + with m.If(self.pfv.stb & ~self.pfv.intr & (self.pfv.order <= spec_order)): with m.If(gpr_ra_write & gpr_rt_write): m.d.sync += gpr_conflict.eq(1) with m.If(gpr_ra_write | gpr_rt_write): @@ -61,15 +62,16 @@ class Check(Elaboratable): m.d.sync += [ Assume(Past(self.pfv.stb)), Assume(Past(self.pfv.order) == spec_order), - Assert(gpr_written.implies(~gpr_conflict)), ] - with m.If(gpr_written & Past(gpr_ra_read)): - m.d.sync += Assert(Past(gpr_shadow) == Past(self.pfv.ra.r_data)) - with m.If(gpr_written & Past(gpr_rb_read)): - m.d.sync += Assert(Past(gpr_shadow) == Past(self.pfv.rb.r_data)) - with m.If(gpr_written & Past(gpr_rs_read)): - m.d.sync += Assert(Past(gpr_shadow) == Past(self.pfv.rs.r_data)) - with m.If(gpr_written & Past(gpr_rt_read)): - m.d.sync += Assert(Past(gpr_shadow) == Past(self.pfv.rt.r_data)) + with m.If(~Past(self.pfv.intr)): + m.d.sync += Assert(gpr_written.implies(~gpr_conflict)) + with m.If(gpr_written & Past(gpr_ra_read)): + m.d.sync += Assert(Past(gpr_shadow) == Past(self.pfv.ra.r_data)) + with m.If(gpr_written & Past(gpr_rb_read)): + m.d.sync += Assert(Past(gpr_shadow) == Past(self.pfv.rb.r_data)) + with m.If(gpr_written & Past(gpr_rs_read)): + m.d.sync += Assert(Past(gpr_shadow) == Past(self.pfv.rs.r_data)) + with m.If(gpr_written & Past(gpr_rt_read)): + m.d.sync += Assert(Past(gpr_shadow) == Past(self.pfv.rt.r_data)) return m