src/soc/fu/spr/formal/proof_main_stage.py

   1 # Proof of correctness for SPR pipeline, main stage
   2
   3
   4 """
   5 Links:
   6 * https://bugs.libre-soc.org/show_bug.cgi?id=418
   7 """
   8
   9 import unittest
  10
  11 from nmigen import (Elaboratable, Module, Signal, Cat)
  12 from nmigen.asserts import Assert, AnyConst, Assume
  13 from nmigen.cli import rtlil
  14
  15 from nmutil.formaltest import FHDLTestCase
  16
  17 from soc.fu.spr.main_stage import SPRMainStage
  18 from soc.fu.spr.pipe_data import SPRPipeSpec
  19 from soc.fu.spr.spr_input_record import CompSPROpSubset
  20
  21 from openpower.decoder.power_decoder2 import decode_spr_num
  22 from openpower.decoder.power_enums import MicrOp, SPR, XER_bits
  23 from openpower.decoder.power_fields import DecodeFields
  24 from openpower.decoder.power_fieldsn import SignalBitRange
  25
  26 # use POWER numbering. sigh.
  27
  28
  29 def xer_bit(name):
  30     return 63-XER_bits[name]
  31
  32
  33 class Driver(Elaboratable):
  34     """
  35     Defines a module to drive the device under test and assert properties
  36     about its outputs.
  37     """
  38
  39     def elaborate(self, platform):
  40         m = Module()
  41         comb = m.d.comb
  42
  43         # cookie-cutting most of this from alu formal proof_main_stage.py
  44
  45         rec = CompSPROpSubset()
  46         # Setup random inputs for dut.op
  47         for p in rec.ports():
  48             width = p.width
  49             comb += p.eq(AnyConst(width))
  50
  51         pspec = SPRPipeSpec(id_wid=2, parent_pspec=None)
  52         m.submodules.dut = dut = SPRMainStage(pspec)
  53
  54         # frequently used aliases
  55         a = dut.i.a
  56         ca_in = dut.i.xer_ca[0]   # CA carry in
  57         ca32_in = dut.i.xer_ca[1]  # CA32 carry in 32
  58         so_in = dut.i.xer_so      # SO sticky overflow
  59         ov_in = dut.i.xer_ov[0]   # XER OV in
  60         ov32_in = dut.i.xer_ov[1]  # XER OV32 in
  61         o = dut.o.o
  62
  63         # setup random inputs
  64         comb += [a.eq(AnyConst(64)),
  65                  ca_in.eq(AnyConst(0b11)),
  66                  so_in.eq(AnyConst(1))]
  67
  68         # and for the context muxid
  69         width = dut.i.ctx.muxid.width
  70         comb += dut.i.ctx.muxid.eq(AnyConst(width))
  71
  72         # assign the PowerDecode2 operation subset
  73         comb += dut.i.ctx.op.eq(rec)
  74
  75         # check that the operation (op) is passed through (and muxid)
  76         comb += Assert(dut.o.ctx.op == dut.i.ctx.op)
  77         comb += Assert(dut.o.ctx.muxid == dut.i.ctx.muxid)
  78
  79         # MTSPR
  80         fields = DecodeFields(SignalBitRange, [dut.i.ctx.op.insn])
  81         fields.create_specs()
  82         xfx = fields.FormXFX
  83         spr = Signal(len(xfx.SPR))
  84         comb += spr.eq(decode_spr_num(xfx.SPR))
  85
  86         with m.Switch(dut.i.ctx.op.insn_type):
  87
  88             # OP_MTSPR
  89             with m.Case(MicrOp.OP_MTSPR):
  90                 with m.Switch(spr):
  91                     with m.Case(SPR.CTR, SPR.LR, SPR.TAR, SPR.SRR0, SPR.SRR1):
  92                         comb += [
  93                             Assert(dut.o.fast1.data == a),
  94                             Assert(dut.o.fast1.ok),
  95
  96                             # If a fast-path SPR is referenced, no other OKs
  97                             # can fire.
  98                             Assert(~dut.o.xer_so.ok),
  99                             Assert(~dut.o.xer_ov.ok),
 100                             Assert(~dut.o.xer_ca.ok),
 101                         ]
 102                     with m.Case(SPR.XER):
 103                         comb += [
 104                             Assert(dut.o.xer_so.data == a[xer_bit('SO')]),
 105                             Assert(dut.o.xer_so.ok),
 106                             Assert(dut.o.xer_ov.data == Cat(
 107                                 a[xer_bit('OV')], a[xer_bit('OV32')]
 108                             )),
 109                             Assert(dut.o.xer_ov.ok),
 110                             Assert(dut.o.xer_ca.data == Cat(
 111                                 a[xer_bit('CA')], a[xer_bit('CA32')]
 112                             )),
 113                             Assert(dut.o.xer_ca.ok),
 114
 115                             # XER is not a fast-path SPR.
 116                             Assert(~dut.o.fast1.ok),
 117                         ]
 118                     # slow SPRs TODO
 119
 120             # OP_MFSPR
 121             with m.Case(MicrOp.OP_MFSPR):
 122                 comb += Assert(o.ok)
 123                 with m.Switch(spr):
 124                     with m.Case(SPR.CTR, SPR.LR, SPR.TAR, SPR.SRR0, SPR.SRR1):
 125                         comb += Assert(o.data == dut.i.fast1)
 126                     with m.Case(SPR.XER):
 127                         bits = {
 128                             'SO': so_in,
 129                             'OV': ov_in,
 130                             'OV32': ov32_in,
 131                             'CA': ca_in,
 132                             'CA32': ca32_in,
 133                         }
 134                         comb += [
 135                             Assert(o[xer_bit(b)] == bits[b])
 136                             for b in bits
 137                         ]
 138                     # slow SPRs TODO
 139
 140         return m
 141
 142
 143 class SPRMainStageTestCase(FHDLTestCase):
 144     def test_formal(self):
 145         self.assertFormal(Driver(), mode="bmc", depth=100)
 146         self.assertFormal(Driver(), mode="cover", depth=100)
 147
 148     def test_ilang(self):
 149         vl = rtlil.convert(Driver(), ports=[])
 150         with open("spr_main_stage.il", "w") as f:
 151             f.write(vl)
 152
 153
 154 if __name__ == '__main__':
 155     unittest.main()