From: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
Date: Wed, 22 Jul 2020 12:50:31 +0000 (+0100)
Subject: add comment headings with spec page numbers
X-Git-Tag: semi_working_ecp5~628
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5bb619e6f18cacdb606eefe8b0bdb89da4131487;p=soc.git

add comment headings with spec page numbers
---

diff --git a/src/soc/fu/trap/formal/proof_main_stage.py b/src/soc/fu/trap/formal/proof_main_stage.py
index b2e4c498..dc257292 100644
--- a/src/soc/fu/trap/formal/proof_main_stage.py
+++ b/src/soc/fu/trap/formal/proof_main_stage.py
@@ -61,6 +61,10 @@ class Driver(Elaboratable):
 
         # start of properties
         with m.Switch(op.insn_type):
+
+            ###############
+            # TDI/TWI/TD/TW.  v3.0B p90-91
+            ###############
             with m.Case(MicrOp.OP_TRAP):
                 # TODO: put back use of fields, do not access insn bits direct
                 # see https://bugs.libre-soc.org/show_bug.cgi?id=421#c24
@@ -157,6 +161,9 @@ class Driver(Elaboratable):
                         Assert(nia_o.data == op.trapaddr << 4),
                     ]
 
+            #################
+            # SC.  v3.0B p952
+            #################
             with m.Case(MicrOp.OP_SC):
                 expected_msr = Signal(len(msr_o.data))
                 comb += expected_msr.eq(op.msr)
@@ -220,6 +227,9 @@ class Driver(Elaboratable):
                 with m.Else():
                     comb += Assert(msr_o[MSR.HV] == 0)
 
+            ###################
+            # RFID.  v3.0B p955
+            ###################
             with m.Case(MicrOp.OP_RFID):
                 comb += [
                     Assert(msr_o.ok),