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                 expected_msr = Signal(len(msr_o.data))
  58                 comb += expected_msr.eq(op.msr)
  59                 # Unless otherwise documented, these exceptions to the MSR bits are
  60                 # documented in Power ISA V3.0B, page 1063 or 1064.
  61                 comb += expected_msr[MSR.IR].eq(0)
  62                 comb += expected_msr[MSR.DR].eq(0)
  63                 comb += expected_msr[MSR.FE0].eq(0)
  64                 comb += expected_msr[MSR.FE1].eq(0)
  65                 comb += expected_msr[MSR.EE].eq(0)
  66                 comb += expected_msr[MSR.RI].eq(0)
  67                 comb += expected_msr[MSR.SF].eq(1)
  68                 comb += expected_msr[MSR.TM].eq(0)
  69                 comb += expected_msr[MSR.VEC].eq(0)
  70                 comb += expected_msr[MSR.VSX].eq(0)
  71                 comb += expected_msr[MSR.PR].eq(0)
  72                 comb += expected_msr[MSR.FP].eq(0)
  73                 comb += expected_msr[MSR.PMM].eq(0)
  74                 comb += expected_msr[MSR.TEs:MSR.TEe+1].eq(0)
  75                 comb += expected_msr[MSR.UND].eq(0)
  76                 comb += expected_msr[MSR.LE].eq(1)
  77
  78                 with m.If(op.msr[MSR.TSs:MSR.TSe+1] == 0b10):
  79                     comb += expected_msr[MSR.TSs:MSR.TSe+1].eq(0b01)
  80                 with m.Else():
  81                     comb += expected_msr[MSR.TSs:MSR.TSe+1].eq(op.msr[MSR.TSs:MSR.TSe+1])
  82
  83                 # Power ISA V3.0B, Book 2, Section 3.3.1
  84                 with m.If(field(op.insn, 20, 26) == 1):
  85                     comb += expected_msr[MSR.HV].eq(1)
  86                 with m.Else():
  87                     comb += expected_msr[MSR.HV].eq(0)
  88
  89                 comb += [
  90                     Assert(dut.o.srr0.ok),
  91                     Assert(srr1_o.ok),
  92                     Assert(msr_o.ok),
  93
  94                     Assert(dut.o.srr0.data == (op.cia + 4)[0:64]),
  95                     Assert(field(srr1_o, 33, 36) == 0),
  96                     Assert(field(srr1_o, 42, 47) == 0),
  97                     Assert(field(srr1_o, 0, 32) == field(msr_i, 0, 32)),
  98                     Assert(field(srr1_o, 37, 41) == field(msr_i, 37, 41)),
  99                     Assert(field(srr1_o, 48, 63) == field(msr_i, 48, 63)),
 100
 101                     Assert(msr_o.data == expected_msr),
 102                 ]
 103                 with m.If(field(op.insn, 20, 26) == 1):
 104                     comb += Assert(msr_o[MSR.HV] == 1)
 105                 with m.Else():
 106                     comb += Assert(msr_o[MSR.HV] == 0)
 107
 108             with m.Case(MicrOp.OP_RFID):
 109                 comb += [
 110                     Assert(msr_o.ok),
 111                     Assert(dut.o.nia.ok),
 112
 113                     Assert(msr_o[MSR.HV] == (srr1_i[MSR.HV] & msr_i[MSR.HV])),
 114                     Assert(msr_o[MSR.EE] == (srr1_i[MSR.EE] | srr1_i[MSR.PR])),
 115                     Assert(msr_o[MSR.IR] == (srr1_i[MSR.IR] | srr1_i[MSR.PR])),
 116                     Assert(msr_o[MSR.DR] == (srr1_i[MSR.DR] | srr1_i[MSR.PR])),
 117                     Assert(field(msr_o, 0, 2) == field(srr1_i, 0, 2)),
 118                     Assert(field(msr_o, 4, 28) == field(srr1_i, 4, 28)),
 119                     Assert(msr_o[63-32] == srr1_i[63-32]),
 120                     Assert(field(msr_o, 37, 41) == field(srr1_i, 37, 41)),
 121                     Assert(field(msr_o, 49, 50) == field(srr1_i, 49, 50)),
 122                     Assert(field(msr_o, 52, 57) == field(srr1_i, 52, 57)),
 123                     Assert(field(msr_o, 60, 63) == field(srr1_i, 60, 63)),
 124                     Assert(dut.o.nia.data == Cat(Const(0, 2), dut.i.srr0[2:])),
 125                 ]
 126                 with m.If(msr_i[MSR.HV]):
 127                     comb += Assert(msr_o[MSR.ME] == srr1_i[MSR.ME])
 128                 with m.Else():
 129                     comb += Assert(msr_o[MSR.ME] == msr_i[MSR.ME])
 130                 with m.If((field(msr_i , 29, 31) != 0b010) |
 131                           (field(srr1_i, 29, 31) != 0b000)):
 132                     comb += Assert(field(msr_o.data, 29, 31) ==
 133                                    field(srr1_i, 29, 31))
 134                 with m.Else():
 135                     comb += Assert(field(msr_o.data, 29, 31) ==
 136                                    field(msr_i, 29, 31))
 137
 138         comb += dut.i.ctx.matches(dut.o.ctx)
 139
 140         return m
 141
 142
 143 class TrapMainStageTestCase(FHDLTestCase):
 144     def test_formal(self):
 145         self.assertFormal(Driver(), mode="bmc", depth=10)
 146         self.assertFormal(Driver(), mode="cover", depth=10)
 147
 148     def test_ilang(self):
 149         vl = rtlil.convert(Driver(), ports=[])
 150         with open("trap_main_stage.il", "w") as f:
 151             f.write(vl)
 152
 153
 154 if __name__ == '__main__':
 155     unittest.main()
 156