From: Michael Nolan <mtnolan2640@gmail.com>
Date: Wed, 20 May 2020 20:21:15 +0000 (-0400)
Subject: Add proof for OP_MFCR
X-Git-Tag: div_pipeline~1004
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b9a3b94d0ed88221b1ca19027bf8f23b806c8e8b;p=soc.git

Add proof for OP_MFCR
---

diff --git a/src/soc/fu/cr/formal/proof_main_stage.py b/src/soc/fu/cr/formal/proof_main_stage.py
index 79c16103..d109f81f 100644
--- a/src/soc/fu/cr/formal/proof_main_stage.py
+++ b/src/soc/fu/cr/formal/proof_main_stage.py
@@ -43,6 +43,7 @@ class Driver(Elaboratable):
         a = dut.i.a
         cr = dut.i.cr
         cr_o = dut.o.cr
+        o = dut.o.o
 
         # setup random inputs
         comb += [a.eq(AnyConst(64)),
@@ -62,12 +63,21 @@ class Driver(Elaboratable):
 
         xl_fields = dut.fields.FormXL
         xfx_fields = dut.fields.FormXFX
+        FXM = xfx_fields.FXM[0:-1]
         with m.Switch(rec.insn_type):
             with m.Case(InternalOp.OP_MTCRF):
-                FXM = xfx_fields.FXM[0:-1]
                 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])
+            with m.Case(InternalOp.OP_MFCR):
+                with m.If(rec.insn[20]):  # mfocrf
+                    for i in range(8):
+                        with m.If(FXM[i]):
+                            comb += Assert(o[4*i:4*i+4] == cr[4*i:4*i+4])
+                        with m.Else():
+                            comb += Assert(o[4*i:4*i+4] == 0)
+                with m.Else(): # mfcrf
+                    comb += Assert(o == cr)
             with m.Case(InternalOp.OP_CROP):
                 bt = Signal(xl_fields.BT[0:-1].shape(), reset_less=True)
                 ba = Signal(xl_fields.BA[0:-1].shape(), reset_less=True)