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 a5d5e7e997c46f205c76c0bbb8c7cc783d9b9eef..7a8722720142f29fdfa02dc37dbb14983e1ffa7f 100644 (file)
--- 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
             ###################