From: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
Date: Wed, 22 Jul 2020 12:45:58 +0000 (+0100)
Subject: comment on op.insn ordering
X-Git-Tag: semi_working_ecp5~629
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f737d372ea4178b3b01c988509cb327fb8be7a49;p=soc.git

comment on op.insn ordering
---

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():