From ec132548aaec2e0850e93637259bdf2f5e8b2b17 Mon Sep 17 00:00:00 2001 From: Luke Kenneth Casson Leighton Date: Wed, 22 Jul 2020 19:08:40 +0100 Subject: [PATCH] whoops forgot field accessor --- src/soc/fu/trap/formal/proof_main_stage.py | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/soc/fu/trap/formal/proof_main_stage.py b/src/soc/fu/trap/formal/proof_main_stage.py index eb9dce92..b43e2558 100644 --- a/src/soc/fu/trap/formal/proof_main_stage.py +++ b/src/soc/fu/trap/formal/proof_main_stage.py @@ -248,14 +248,15 @@ class Driver(Elaboratable): # which field it is (3 == HV etc.) # spec: MSR[51] <- (MSR[3] & SRR1[51]) | ((¬MSR[3] & MSR[51])) - with m.If(msr_i[3]): # HV - comb += Assert(msr_o[51] == srr1_i[51]) # ME from SRR1 + with m.If(field(msr_i, 3)): # HV + comb += Assert(field(msr_o, 51) == field(srr1_i, 51) # ME with m.Else(): - comb += Assert(msr_o[51] == msr_i[51]) # ME from MSR (in) + comb += Assert(field(msr_o, 51) == field(msr_i, 51)) # ME comb += [ # spec: MSR[3] <- (MSR[3] & SRR1[3]) - Assert(msr_o[3] == (srr1_i[3] & msr_i[3])), # HV + Assert(field(msr_o, 3) == (field(srr1_i, 3) & + field(msr_i, 3))), # HV ] # if (MSR[29:31] != 0b010) | (SRR1[29:31] != 0b000) then -- 2.30.2