From 3af7a728eebe2ce97238825470d2995e4be96ca7 Mon Sep 17 00:00:00 2001 From: "Samuel A. Falvo II" Date: Fri, 17 Jul 2020 10:30:10 -0700 Subject: [PATCH] Flesh out SPR-related FV properties. --- src/soc/fu/spr/formal/proof_main_stage.py | 83 +++++++++++++++++++---- 1 file changed, 71 insertions(+), 12 deletions(-) diff --git a/src/soc/fu/spr/formal/proof_main_stage.py b/src/soc/fu/spr/formal/proof_main_stage.py index b831bc63..730ffdbd 100644 --- a/src/soc/fu/spr/formal/proof_main_stage.py +++ b/src/soc/fu/spr/formal/proof_main_stage.py @@ -6,7 +6,9 @@ Links: * https://bugs.libre-soc.org/show_bug.cgi?id=418 """ -from nmigen import (Elaboratable, Module) +import unittest + +from nmigen import (Elaboratable, Module, Signal, Cat) from nmigen.asserts import Assert, AnyConst, Assume from nmigen.cli import rtlil @@ -15,8 +17,15 @@ from nmutil.formaltest import FHDLTestCase from soc.fu.spr.main_stage import SPRMainStage from soc.fu.spr.pipe_data import SPRPipeSpec from soc.fu.spr.spr_input_record import CompSPROpSubset -from soc.decoder.power_enums import MicrOp -import unittest + +from soc.decoder.power_decoder2 import decode_spr_num +from soc.decoder.power_enums import MicrOp, SPR, XER_bits +from soc.decoder.power_fields import DecodeFields +from soc.decoder.power_fieldsn import SignalBitRange + + +def xer_bit(name): + return 63-XER_bits[name] class Driver(Elaboratable): @@ -40,17 +49,12 @@ class Driver(Elaboratable): pspec = SPRPipeSpec(id_wid=2) m.submodules.dut = dut = SPRMainStage(pspec) - # convenience variables + # frequently used aliases a = dut.i.a ca_in = dut.i.xer_ca[0] # CA carry in ca32_in = dut.i.xer_ca[1] # CA32 carry in 32 so_in = dut.i.xer_so # SO sticky overflow - - ca_o = dut.o.xer_ca.data[0] # CA carry out - ca32_o = dut.o.xer_ca.data[1] # CA32 carry out32 - ov_o = dut.o.xer_ov.data[0] # OV overflow - ov32_o = dut.o.xer_ov.data[1] # OV32 overflow32 - o = dut.o.o.data + o = dut.o.o # setup random inputs comb += [a.eq(AnyConst(64)), @@ -68,12 +72,67 @@ class Driver(Elaboratable): comb += Assert(dut.o.ctx.op == dut.i.ctx.op ) comb += Assert(dut.o.ctx.muxid == dut.i.ctx.muxid ) + # MTSPR + fields = DecodeFields(SignalBitRange, [dut.i.ctx.op.insn]) + fields.create_specs() + xfx = fields.FormXFX + spr = Signal(len(xfx.SPR)) + comb += spr.eq(decode_spr_num(xfx.SPR)) + + with m.Switch(dut.i.ctx.op.insn_type): + with m.Case(MicrOp.OP_MTSPR): + with m.Switch(spr): + with m.Case(SPR.CTR, SPR.LR, SPR.TAR, SPR.SRR0, SPR.SRR1): + comb += [ + Assert(dut.o.fast1.data == a), + Assert(dut.o.fast1.ok), + + # If a fast-path SPR is referenced, no other OKs + # can fire. + Assert(~dut.o.xer_so.ok), + Assert(~dut.o.xer_ov.ok), + Assert(~dut.o.xer_ca.ok), + ] + with m.Case(SPR.XER): + comb += [ + Assert(dut.o.xer_so.data == a[xer_bit('SO')]), + Assert(dut.o.xer_so.ok), + Assert(dut.o.xer_ov.data == Cat( + a[xer_bit('OV')], a[xer_bit('OV32')] + )), + Assert(dut.o.xer_ov.ok), + Assert(dut.o.xer_ca.data == Cat( + a[xer_bit('CA')], a[xer_bit('CA32')] + )), + Assert(dut.o.xer_ca.ok), + + # XER is not a fast-path SPR. + Assert(~dut.o.fast1.ok), + ] + # slow SPRs TODO + with m.Case(MicrOp.OP_MFSPR): + comb += Assert(o.ok) + with m.Switch(spr): + with m.Case(SPR.CTR, SPR.LR, SPR.TAR, SPR.SRR0, SPR.SRR1): + comb += Assert(o.data == dut.i.fast1) + with m.Case(SPR.XER): + bits = { + 'SO': so_in, + 'OV': dut.i.xer_ov[0], + 'OV32': dut.i.xer_ov[1], + 'CA': ca_in, + 'CA32': ca32_in, + } + comb += [ + Assert(o[xer_bit(b)] == bits[b]) + for b in bits + ] + # slow SPRs TODO + return m class SPRMainStageTestCase(FHDLTestCase): - #don't worry about it - tests are run manually anyway. fail is fine. - #@skipUnless(getenv("FORMAL_SPR"), "Exercise SPR formal tests [WIP]") def test_formal(self): self.assertFormal(Driver(), mode="bmc", depth=100) self.assertFormal(Driver(), mode="cover", depth=100) -- 2.30.2