From: Samuel A. Falvo II <kc5tja@arrl.net>
Date: Fri, 24 Jul 2020 23:31:09 +0000 (-0700)
Subject: Properties for MFMSR
X-Git-Tag: semi_working_ecp5~557
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0957767a91d6a657aa5e8b48a5e562f411a5742c;p=soc.git

Properties for MFMSR
---

diff --git a/src/soc/fu/trap/formal/proof_main_stage.py b/src/soc/fu/trap/formal/proof_main_stage.py
index a5d5e7e9..7a872272 100644
--- a/src/soc/fu/trap/formal/proof_main_stage.py
+++ b/src/soc/fu/trap/formal/proof_main_stage.py
@@ -171,6 +171,12 @@ class Driver(Elaboratable):
             # MFMSR
             ###################
 
+            with m.Case(MicrOp.OP_MFMSR):
+                comb += [
+                    Assert(dut.o.o.ok),
+                    Assert(dut.o.o.data == msr_i),
+                ]
+
             ###################
             # RFID.  v3.0B p955
             ###################