convert CR pipeline to Data.ok

diff --git a/src/soc/fu/cr/formal/proof_main_stage.py b/src/soc/fu/cr/formal/proof_main_stage.py
index a046495d84c03317d5292b7b2fd23b2bac7af693..2cb30c82b0ef62d75a53d1ed4b28e57dabb3c6f5 100644 (file)
--- a/src/soc/fu/cr/formal/proof_main_stage.py
+++ b/src/soc/fu/cr/formal/proof_main_stage.py
@@ -49,7 +49,7 @@ class Driver(Elaboratable):
         b = dut.i.b
         cr = full_cr_in
         full_cr_out = dut.o.full_cr
-        o = dut.o.o
+        o = dut.o.o.data
 
         # setup random inputs
         comb += [a.eq(AnyConst(64)),
@@ -133,6 +133,8 @@ class Driver(Elaboratable):
 
         comb += dut.i.ctx.op.eq(rec)
 
+        o_ok = Signal()
+
         # Assert that op gets copied from the input to output
         for rec_sig in rec.ports():
             name = rec_sig.name
@@ -158,6 +160,8 @@ class Driver(Elaboratable):
                             comb += Assert(o[4*i:4*i+4] == 0)
                 with m.Else(): # mfcrf
                     comb += Assert(o == cr)
+                comb += o_ok.eq(1)
+
             with m.Case(InternalOp.OP_MCRF):
                 BF = xl_fields.BF[0:-1]
                 BFA = xl_fields.BFA[0:-1]
@@ -212,6 +216,10 @@ class Driver(Elaboratable):
 
                 # select a or b as output
                 comb += Assert(o == Mux(cr_bit, a, b))
+                comb += o_ok.eq(1)
+
+        # check that data ok was only enabled when op actioned
+        comb += Assert(dut.o.o.ok == o_ok)
 
         return m
 

diff --git a/src/soc/fu/cr/main_stage.py b/src/soc/fu/cr/main_stage.py
index 41a0acd0901ddd15491b7c3dd0a4ce901b707828..7c43fffd97157e4d8f9ffbfefb38c015cad24bdc 100644 (file)
--- a/src/soc/fu/cr/main_stage.py
+++ b/src/soc/fu/cr/main_stage.py
@@ -127,11 +127,12 @@ class CRMainStage(PipeModBase):
                 # mfocrf
                 with m.If(move_one):
                     # output register RT
-                    comb += rt_o.eq(full_cr & mask)
+                    comb += rt_o.data.eq(full_cr & mask)
                 # mfcrf
                 with m.Else():
                     # output register RT
-                    comb += rt_o.eq(full_cr)
+                    comb += rt_o.data.eq(full_cr)
+                comb += rt_o.ok.eq(1) # indicate "INT reg changed"
 
             # ##### isel #####
             with m.Case(InternalOp.OP_ISEL):
@@ -147,6 +148,7 @@ class CRMainStage(PipeModBase):
 
                 # select a or b as output
                 comb += rt_o.eq(Mux(cr_bit, a, b))
+                comb += rt_o.ok.eq(1) # indicate "INT reg changed"
 
         comb += self.o.ctx.eq(self.i.ctx)