corrections to trap proof see

https://bugs.libre-soc.org/show_bug.cgi?id=421#c17 and
https://bugs.libre-soc.org/show_bug.cgi?id=421#c18

diff --git a/src/soc/fu/trap/formal/proof_main_stage.py b/src/soc/fu/trap/formal/proof_main_stage.py
index d9234a447106b83b562539813e0ea09211aa82e3..e701cadd1e7e46c46e07e7e0b99032a9813f88e2 100644 (file)
--- a/src/soc/fu/trap/formal/proof_main_stage.py
+++ b/src/soc/fu/trap/formal/proof_main_stage.py
@@ -25,7 +25,7 @@ from soc.fu.trap.trap_input_record import CompTrapOpSubset
 
 
 def field(r, start, end):
-    return r[63-end:63-start]
+    return r[63-end:63-start+1] # slices ends are +1, POWER spec is not
 
 
 class Driver(Elaboratable):
@@ -84,9 +84,13 @@ class Driver(Elaboratable):
                     comb += Assert(msr_o[MSR.ME] == srr1_i[MSR.ME])
                 with m.Else():
                     comb += Assert(msr_o[MSR.ME] == msr_i[MSR.ME])
-                with m.If((field(msr_i, 29, 31) != 0b010) |
-                          (field(msr_i, 29, 31) != 0b000)):
-                    comb += Assert(field(msr_o.data, 29, 31) == field(srr1_i, 29, 31))
+                with m.If((field(msr_i , 29, 31) != 0b010) | # MSR
+                          (field(srr1_i, 29, 31) != 0b000)): # SRR1
+                    comb += Assert(field(msr_o.data, 29, 31) ==
+                                   field(srr1_i, 29, 31))
+                with m.Else():
+                    comb += Assert(field(msr_o.data, 29, 31) ==
+                                   field(msr_i, 29, 31))
 
         comb += dut.i.ctx.matches(dut.o.ctx)