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

   1 # Proof of correctness for trap pipeline, main stage
   2
   3
   4 """
   5 Links:
   6 * https://bugs.libre-soc.org/show_bug.cgi?id=421
   7 """
   8
   9
  10 import unittest
  11
  12 from nmigen import Cat, Const, Elaboratable, Module, Signal
  13 from nmigen.asserts import Assert, AnyConst
  14 from nmigen.cli import rtlil
  15
  16 from nmutil.formaltest import FHDLTestCase
  17
  18 from soc.consts import MSR
  19
  20 from soc.decoder.power_enums import MicrOp
  21
  22 from soc.fu.trap.main_stage import TrapMainStage
  23 from soc.fu.trap.pipe_data import TrapPipeSpec
  24 from soc.fu.trap.trap_input_record import CompTrapOpSubset
  25
  26
  27 def field(r, start, end):
  28     """Answers with a subfield of the signal r ("register"), where
  29     the start and end bits use IBM conventions.  start < end.
  30     """
  31     return r[63-end:64-start]
  32
  33
  34 class Driver(Elaboratable):
  35     """
  36     """
  37
  38     def elaborate(self, platform):
  39         m = Module()
  40         comb = m.d.comb
  41
  42         rec = CompTrapOpSubset()
  43         pspec = TrapPipeSpec(id_wid=2)
  44
  45         m.submodules.dut = dut = TrapMainStage(pspec)
  46
  47         # frequently used aliases
  48         op = dut.i.ctx.op
  49         msr_o, msr_i = dut.o.msr, op.msr
  50         srr1_o, srr1_i = dut.o.srr1, dut.i.srr1
  51
  52         comb += op.eq(rec)
  53
  54         # start of properties
  55         with m.Switch(op.insn_type):
  56             with m.Case(MicrOp.OP_SC):
  57                 comb += [
  58                     Assert(dut.o.srr0.ok),
  59                     Assert(srr1_o.ok),
  60                     Assert(msr_o.ok),
  61
  62                     Assert(dut.o.srr0.data == (op.cia + 4)[0:64]),
  63                     Assert(field(srr1_o, 33, 36) == 0),
  64                     Assert(field(srr1_o, 42, 47) == 0),
  65                     Assert(field(srr1_o, 0, 32) == field(msr_i, 0, 32)),
  66                     Assert(field(srr1_o, 37, 41) == field(msr_i, 37, 41)),
  67                     Assert(field(srr1_o, 48, 63) == field(msr_i, 48, 63)),
  68
  69                     Assert(msr_o[0:16] == msr_i[0:16]),
  70                     Assert(msr_o[22:27] == msr_i[22:27]),
  71                     Assert(msr_o[31:64] == msr_i[31:64]),
  72                     Assert(msr_o[MSR.IR] == 0),  # No LPCR register input,
  73                     Assert(msr_o[MSR.DR] == 0),  # so assuming AIL=0.
  74                     Assert(msr_o[MSR.FE0] == 0),
  75                     Assert(msr_o[MSR.FE1] == 0),
  76                     Assert(msr_o[MSR.EE] == 0),
  77                     Assert(msr_o[MSR.RI] == 0),
  78                 ]
  79                 with m.If(field(op.insn, 20, 26) == 1):
  80                     comb += Assert(msr_o[MSR.HV] == 1)
  81                 with m.Else():
  82                     comb += Assert(msr_o[MSR.HV] == 0)
  83
  84             with m.Case(MicrOp.OP_RFID):
  85                 comb += [
  86                     Assert(msr_o.ok),
  87                     Assert(dut.o.nia.ok),
  88
  89                     Assert(msr_o[MSR.HV] == (srr1_i[MSR.HV] & msr_i[MSR.HV])),
  90                     Assert(msr_o[MSR.EE] == (srr1_i[MSR.EE] | srr1_i[MSR.PR])),
  91                     Assert(msr_o[MSR.IR] == (srr1_i[MSR.IR] | srr1_i[MSR.PR])),
  92                     Assert(msr_o[MSR.DR] == (srr1_i[MSR.DR] | srr1_i[MSR.PR])),
  93                     Assert(field(msr_o, 0, 2) == field(srr1_i, 0, 2)),
  94                     Assert(field(msr_o, 4, 28) == field(srr1_i, 4, 28)),
  95                     Assert(msr_o[63-32] == srr1_i[63-32]),
  96                     Assert(field(msr_o, 37, 41) == field(srr1_i, 37, 41)),
  97                     Assert(field(msr_o, 49, 50) == field(srr1_i, 49, 50)),
  98                     Assert(field(msr_o, 52, 57) == field(srr1_i, 52, 57)),
  99                     Assert(field(msr_o, 60, 63) == field(srr1_i, 60, 63)),
 100                     Assert(dut.o.nia.data == Cat(Const(0, 2), dut.i.srr0[2:])),
 101                 ]
 102                 with m.If(msr_i[MSR.HV]):
 103                     comb += Assert(msr_o[MSR.ME] == srr1_i[MSR.ME])
 104                 with m.Else():
 105                     comb += Assert(msr_o[MSR.ME] == msr_i[MSR.ME])
 106                 with m.If((field(msr_i , 29, 31) != 0b010) | # MSR
 107                           (field(srr1_i, 29, 31) != 0b000)): # SRR1
 108                     comb += Assert(field(msr_o.data, 29, 31) ==
 109                                    field(srr1_i, 29, 31))
 110                 with m.Else():
 111                     comb += Assert(field(msr_o.data, 29, 31) ==
 112                                    field(msr_i, 29, 31))
 113
 114         comb += dut.i.ctx.matches(dut.o.ctx)
 115
 116         return m
 117
 118
 119 class TrapMainStageTestCase(FHDLTestCase):
 120     def test_formal(self):
 121         self.assertFormal(Driver(), mode="bmc", depth=10)
 122         self.assertFormal(Driver(), mode="cover", depth=10)
 123
 124     def test_ilang(self):
 125         vl = rtlil.convert(Driver(), ports=[])
 126         with open("trap_main_stage.il", "w") as f:
 127             f.write(vl)
 128
 129
 130 if __name__ == '__main__':
 131     unittest.main()
 132