From f737d372ea4178b3b01c988509cb327fb8be7a49 Mon Sep 17 00:00:00 2001 From: Luke Kenneth Casson Leighton Date: Wed, 22 Jul 2020 13:45:58 +0100 Subject: [PATCH] comment on op.insn ordering --- src/soc/fu/trap/formal/proof_main_stage.py | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/soc/fu/trap/formal/proof_main_stage.py b/src/soc/fu/trap/formal/proof_main_stage.py index 65723ed6..b2e4c498 100644 --- a/src/soc/fu/trap/formal/proof_main_stage.py +++ b/src/soc/fu/trap/formal/proof_main_stage.py @@ -212,7 +212,9 @@ class Driver(Elaboratable): # see https://bugs.libre-soc.org/show_bug.cgi?id=421#c24 # XXX what is this for? it is not possible to identify # it because the "direct access to insn bits" provides - # absolutely no clue as to its purpose + # absolutely no clue as to its purpose. + # also: this is likely to be wrong because of PowerISA + # field ordering (see V3.0B p4 section 1.3.4) with m.If(field(op.insn, 20, 26) == 1): comb += Assert(msr_o[MSR.HV] == 1) with m.Else(): -- 2.30.2