From 0957767a91d6a657aa5e8b48a5e562f411a5742c Mon Sep 17 00:00:00 2001 From: "Samuel A. Falvo II" Date: Fri, 24 Jul 2020 16:31:09 -0700 Subject: [PATCH] Properties for MFMSR --- src/soc/fu/trap/formal/proof_main_stage.py | 6 ++++++ 1 file changed, 6 insertions(+) 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 ################### -- 2.30.2