From ad905e82a09f3daa051d267608d7283ff8fa5e03 Mon Sep 17 00:00:00 2001 From: Luke Kenneth Casson Leighton Date: Sat, 25 Jul 2020 12:09:30 +0100 Subject: [PATCH] make trap proof section more readable --- libreriscv | 2 +- src/soc/fu/trap/formal/proof_main_stage.py | 16 ++++------------ 2 files changed, 5 insertions(+), 13 deletions(-) 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: -- 2.30.2