assign and test on Data, TODO add Data.ok checking in CR proof

[soc.git] / src / soc / fu / cr / formal / proof_main_stage.py

diff --git a/src/soc/fu/cr/formal/proof_main_stage.py b/src/soc/fu/cr/formal/proof_main_stage.py
index a046495d84c03317d5292b7b2fd23b2bac7af693..26ebc79ebb1785c50b187c19937963f30e11253a 100644 (file)
--- a/src/soc/fu/cr/formal/proof_main_stage.py
+++ b/src/soc/fu/cr/formal/proof_main_stage.py
@@ -48,8 +48,8 @@ class Driver(Elaboratable):
         a = dut.i.a
         b = dut.i.b
         cr = full_cr_in
-        full_cr_out = dut.o.full_cr
-        o = dut.o.o
+        full_cr_out = dut.o.full_cr.data
+        o = dut.o.o.data
 
         # setup random inputs
         comb += [a.eq(AnyConst(64)),
@@ -103,7 +103,7 @@ class Driver(Elaboratable):
                     with m.If(i != bt):
                         comb += cr_output_arr[i].eq(cr_input_arr[i])
                     with m.Else():
-                        comb += cr_output_arr[i].eq(dut.o.cr_o)
+                        comb += cr_output_arr[i].eq(dut.o.cr_o.data)
 
             with m.Case(InternalOp.OP_MCRF):
                 # This does a similar thing to OP_CROP above, with
@@ -123,16 +123,24 @@ class Driver(Elaboratable):
                     with m.If(i != bf):
                         comb += cr_output_arr[i].eq(cr_input_arr[i])
                     with m.Else():
-                        comb += cr_output_arr[i].eq(dut.o.cr_o)
+                        comb += cr_output_arr[i].eq(dut.o.cr_o.data)
 
             # For the other two, they take the full CR as input, and
             # output a full CR. This handles that
             with m.Default():
                 comb += dut.i.full_cr.eq(full_cr_in)
-                comb += cr_o.eq(dut.o.full_cr)
+                comb += cr_o.eq(full_cr_out)
 
         comb += dut.i.ctx.op.eq(rec)
 
+        # test signals for output conditions.  these must only be enabled for
+        # specific instructions, indicating that they generated the output.
+        # this is critically important because the "ok" signals are used by
+        # MultiCompUnit to request a write to the regfile.
+        o_ok = Signal()
+        cr_o_ok = Signal()
+        full_cr_o_ok = Signal()
+
         # Assert that op gets copied from the input to output
         for rec_sig in rec.ports():
             name = rec_sig.name
@@ -149,6 +157,8 @@ class Driver(Elaboratable):
                 for i in range(8):
                     with m.If(FXM[i]):
                         comb += Assert(cr_o[4*i:4*i+4] == a[4*i:4*i+4])
+                comb += cr_o_ok.eq(1)
+
             with m.Case(InternalOp.OP_MFCR):
                 with m.If(rec.insn[20]):  # mfocrf
                     for i in range(8):
@@ -158,6 +168,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]
@@ -166,6 +178,7 @@ class Driver(Elaboratable):
                 for i in range(8):
                     with m.If(BF != 7-i):
                         comb += Assert(cr_o[i*4:i*4+4] == cr[i*4:i*4+4])
+                comb += cr_o_ok.eq(1)
 
             with m.Case(InternalOp.OP_CROP):
                 bt = Signal(xl_fields.BT[0:-1].shape(), reset_less=True)
@@ -212,6 +225,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