From 5bb619e6f18cacdb606eefe8b0bdb89da4131487 Mon Sep 17 00:00:00 2001 From: Luke Kenneth Casson Leighton Date: Wed, 22 Jul 2020 13:50:31 +0100 Subject: [PATCH] add comment headings with spec page numbers --- src/soc/fu/trap/formal/proof_main_stage.py | 10 ++++++++++ 1 file changed, 10 insertions(+) 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), -- 2.30.2