From: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
Date: Sat, 25 Jul 2020 11:09:30 +0000 (+0100)
Subject: make trap proof section more readable
X-Git-Tag: semi_working_ecp5~556
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ad905e82a09f3daa051d267608d7283ff8fa5e03;p=soc.git

make trap proof section more readable
---

diff --git a/libreriscv b/libreriscv
index 9fe303b0..bd0f1cca 160000
--- 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 7a872272..0d704fe3 100644
--- 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: