From: Samuel A. Falvo II <kc5tja@arrl.net>
Date: Tue, 21 Jul 2020 19:16:09 +0000 (-0700)
Subject: Fix where msr_i gets its value from
X-Git-Tag: semi_working_ecp5~645
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b2dfa48d32204efcd2ec59c708ea62bd428271a5;p=soc.git

Fix where msr_i gets its value from
---

diff --git a/src/soc/fu/trap/formal/proof_main_stage.py b/src/soc/fu/trap/formal/proof_main_stage.py
index 7afb9b0b..0a1afbdb 100644
--- a/src/soc/fu/trap/formal/proof_main_stage.py
+++ b/src/soc/fu/trap/formal/proof_main_stage.py
@@ -46,7 +46,7 @@ class Driver(Elaboratable):
 
         # frequently used aliases
         op = dut.i.ctx.op
-        msr_o, msr_i = dut.o.msr, dut.i.msr
+        msr_o, msr_i = dut.o.msr, op.msr
         srr1_o, srr1_i = dut.o.srr1, dut.i.srr1
 
         comb += op.eq(rec)
@@ -57,9 +57,9 @@ class Driver(Elaboratable):
                 comb += [
                     Assert(dut.o.srr0.ok),
                     Assert(srr1_o.ok),
-#                   Assert(msr_o.ok),
+                    Assert(msr_o.ok),
 
-                    Assert(dut.o.srr0.data == (dut.i.cia + 4)[0:64]),
+                    Assert(dut.o.srr0.data == (op.cia + 4)[0:64]),
                     Assert(field(srr1_o, 33, 36) == 0),
                     Assert(field(srr1_o, 42, 47) == 0),
                     Assert(field(srr1_o, 0, 32) == field(msr_i, 0, 32)),