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

Add proof for OP_MCRF
---

diff --git a/src/soc/fu/cr/formal/proof_main_stage.py b/src/soc/fu/cr/formal/proof_main_stage.py
index d109f81f..16223a45 100644
--- a/src/soc/fu/cr/formal/proof_main_stage.py
+++ b/src/soc/fu/cr/formal/proof_main_stage.py
@@ -78,6 +78,15 @@ class Driver(Elaboratable):
                             comb += Assert(o[4*i:4*i+4] == 0)
                 with m.Else(): # mfcrf
                     comb += Assert(o == cr)
+            with m.Case(InternalOp.OP_MCRF):
+                BF = xl_fields.BF[0:-1]
+                BFA = xl_fields.BFA[0:-1]
+                for i in range(4):
+                    comb += Assert(cr_o_arr[BF*4+i] == cr_arr[BFA*4+i])
+                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])
+
             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)