make trap proof section more readable

diff --git a/libreriscv b/libreriscv
index 9fe303b064624df441a038f4853dd2954c506df7..bd0f1cca8b46ff5647398d5e41a90bed8ea4c0b2 160000 (submodule)
--- a/libreriscv
+++ b/libreriscv
@@ -1 +1 @@
-Subproject commit 9fe303b064624df441a038f4853dd2954c506df7
+Subproject commit bd0f1cca8b46ff5647398d5e41a90bed8ea4c0b2

diff --git a/src/soc/fu/trap/formal/proof_main_stage.py b/src/soc/fu/trap/formal/proof_main_stage.py
index 7a8722720142f29fdfa02dc37dbb14983e1ffa7f..0d704fe3b2d5ffbf0f447625c928ff9b04a421fd 100644 (file)
--- a/src/soc/fu/trap/formal/proof_main_stage.py
+++ b/src/soc/fu/trap/formal/proof_main_stage.py
@@ -209,19 +209,11 @@ class Driver(Elaboratable):
                                    field(msr_i, 29, 31))
 
                 # check EE (48) IR (58), DR (59): PR (49) will over-ride
+                PR = field(srr1_i, 49) # alias/copy of SRR1 PR field
                 comb += [
-                    Assert(
-                        field(msr_o, 48) ==
-                        field(srr1_i, 48) | field(srr1_i, 49)
-                    ),
-                    Assert(
-                        field(msr_o, 58) ==
-                        field(srr1_i, 58) | field(srr1_i, 49)
-                    ),
-                    Assert(
-                        field(msr_o, 59) ==
-                        field(srr1_i, 59) | field(srr1_i, 49)
-                    ),
+                    Assert(field(msr_o, 48) == field(srr1_i, 48) | PR), # EE
+                    Assert(field(msr_o, 58) == field(srr1_i, 58) | PR), # IR
+                    Assert(field(msr_o, 59) == field(srr1_i, 59) | PR), # DR
                 ]
 
                 # remaining bits: straight copy.  don't know what these are: