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, signed
  13 from nmigen.asserts import Assert, AnyConst
  14 from nmigen.cli import rtlil
  15
  16 from nmutil.extend import exts
  17 from nmutil.formaltest import FHDLTestCase
  18
  19 from soc.consts import MSR, PI, TT
  20
  21 from soc.decoder.power_enums import MicrOp
  22
  23 from soc.fu.trap.main_stage import TrapMainStage
  24 from soc.fu.trap.pipe_data import TrapPipeSpec
  25 from soc.fu.trap.trap_input_record import CompTrapOpSubset
  26
  27
  28 def field(r, start, end):
  29     """Answers with a subfield of the signal r ("register"), where
  30     the start and end bits use IBM conventions.  start < end.
  31     """
  32     return r[63-end:64-start]
  33
  34
  35 class Driver(Elaboratable):
  36     """
  37     """
  38
  39     def elaborate(self, platform):
  40         m = Module()
  41         comb = m.d.comb
  42
  43         rec = CompTrapOpSubset()
  44         pspec = TrapPipeSpec(id_wid=2)
  45
  46         m.submodules.dut = dut = TrapMainStage(pspec)
  47
  48         # frequently used aliases
  49         op = dut.i.ctx.op
  50         msr_o, msr_i = dut.o.msr, op.msr
  51         srr0_o, srr0_i = dut.o.srr0, dut.i.srr0
  52         srr1_o, srr1_i = dut.o.srr1, dut.i.srr1
  53         nia_o = dut.o.nia
  54
  55         comb += op.eq(rec)
  56
  57         # start of properties
  58         with m.Switch(op.insn_type):
  59             with m.Case(MicrOp.OP_TRAP):
  60                 to = Signal(5)
  61                 comb += to.eq(op.insn[31-10:31-5])
  62
  63                 a_i = Signal(64)
  64                 b_i = Signal(64)
  65                 comb += a_i.eq(dut.i.a)
  66                 comb += b_i.eq(dut.i.b)
  67
  68                 a_s = Signal(signed(64), reset_less=True)
  69                 b_s = Signal(signed(64), reset_less=True)
  70                 a = Signal(64, reset_less=True)
  71                 b = Signal(64, reset_less=True)
  72
  73                 with m.If(op.is_32bit):
  74                     comb += a_s.eq(exts(a_i, 32, 64))
  75                     comb += b_s.eq(exts(b_i, 32, 64))
  76                     comb += a.eq(a_i[0:32])
  77                     comb += b.eq(b_i[0:32])
  78                 with m.Else():
  79                     comb += a_s.eq(a_i)
  80                     comb += b_s.eq(b_i)
  81                     comb += a.eq(a_i)
  82                     comb += b.eq(b_i)
  83
  84                 lt_s = Signal(reset_less=True)
  85                 gt_s = Signal(reset_less=True)
  86                 lt_u = Signal(reset_less=True)
  87                 gt_u = Signal(reset_less=True)
  88                 equal = Signal(reset_less=True)
  89
  90                 comb += lt_s.eq(a_s < b_s)
  91                 comb += gt_s.eq(a_s > b_s)
  92                 comb += lt_u.eq(a < b)
  93                 comb += gt_u.eq(a > b)
  94                 comb += equal.eq(a == b)
  95
  96                 trapbits = Signal(5, reset_less=True)
  97                 comb += trapbits.eq(Cat(gt_u, lt_u, equal, gt_s, lt_s))
  98
  99                 take_trap = Signal()
 100                 traptype = op.traptype
 101                 comb += take_trap.eq(traptype.any() | (trapbits & to).any())
 102
 103                 with m.If(take_trap):
 104                     expected_msr = Signal(len(msr_o.data))
 105                     comb += expected_msr.eq(op.msr)
 106
 107                     comb += expected_msr[MSR.IR].eq(0)
 108                     comb += expected_msr[MSR.DR].eq(0)
 109                     comb += expected_msr[MSR.FE0].eq(0)
 110                     comb += expected_msr[MSR.FE1].eq(0)
 111                     comb += expected_msr[MSR.EE].eq(0)
 112                     comb += expected_msr[MSR.RI].eq(0)
 113                     comb += expected_msr[MSR.SF].eq(1)
 114                     comb += expected_msr[MSR.TM].eq(0)
 115                     comb += expected_msr[MSR.VEC].eq(0)
 116                     comb += expected_msr[MSR.VSX].eq(0)
 117                     comb += expected_msr[MSR.PR].eq(0)
 118                     comb += expected_msr[MSR.FP].eq(0)
 119                     comb += expected_msr[MSR.PMM].eq(0)
 120                     comb += expected_msr[MSR.TEs:MSR.TEe+1].eq(0)
 121                     comb += expected_msr[MSR.UND].eq(0)
 122                     comb += expected_msr[MSR.LE].eq(1)
 123
 124                     with m.If(op.msr[MSR.TSs:MSR.TSe+1] == 0b10):
 125                         comb += expected_msr[MSR.TSs:MSR.TSe+1].eq(0b01)
 126                     with m.Else():
 127                         comb += expected_msr[MSR.TSs:MSR.TSe+1].eq(
 128                             op.msr[MSR.TSs:MSR.TSe+1]
 129                         )
 130
 131                     expected_srr1 = Signal(len(srr1_o.data))
 132                     comb += expected_srr1.eq(op.msr)
 133
 134                     comb += expected_srr1[63-36:63-32].eq(0)
 135                     comb += expected_srr1[PI.TRAP].eq(traptype == 0)
 136                     comb += expected_srr1[PI.PRIV].eq(traptype[1])
 137                     comb += expected_srr1[PI.FP].eq(traptype[0])
 138                     comb += expected_srr1[PI.ADR].eq(traptype[3])
 139                     comb += expected_srr1[PI.ILLEG].eq(traptype[4])
 140                     comb += expected_srr1[PI.TM_BAD_THING].eq(0)
 141
 142                     comb += [
 143                         Assert(msr_o.ok),
 144                         Assert(msr_o.data == expected_msr),
 145                         Assert(srr0_o.ok),
 146                         Assert(srr0_o.data == op.cia),
 147                         Assert(srr1_o.ok),
 148                         Assert(srr1_o.data == expected_srr1),
 149                         Assert(nia_o.ok),
 150                         Assert(nia_o.data == op.trapaddr << 4),
 151                     ]
 152
 153             with m.Case(MicrOp.OP_SC):
 154                 expected_msr = Signal(len(msr_o.data))
 155                 comb += expected_msr.eq(op.msr)
 156                 # Unless otherwise documented, these exceptions to the MSR bits
 157                 # are documented in Power ISA V3.0B, page 1063 or 1064.
 158                 comb += expected_msr[MSR.IR].eq(0)
 159                 comb += expected_msr[MSR.DR].eq(0)
 160                 comb += expected_msr[MSR.FE0].eq(0)
 161                 comb += expected_msr[MSR.FE1].eq(0)
 162                 comb += expected_msr[MSR.EE].eq(0)
 163                 comb += expected_msr[MSR.RI].eq(0)
 164                 comb += expected_msr[MSR.SF].eq(1)
 165                 comb += expected_msr[MSR.TM].eq(0)
 166                 comb += expected_msr[MSR.VEC].eq(0)
 167                 comb += expected_msr[MSR.VSX].eq(0)
 168                 comb += expected_msr[MSR.PR].eq(0)
 169                 comb += expected_msr[MSR.FP].eq(0)
 170                 comb += expected_msr[MSR.PMM].eq(0)
 171                 comb += expected_msr[MSR.TEs:MSR.TEe+1].eq(0)
 172                 comb += expected_msr[MSR.UND].eq(0)
 173                 comb += expected_msr[MSR.LE].eq(1)
 174
 175                 with m.If(op.msr[MSR.TSs:MSR.TSe+1] == 0b10):
 176                     comb += expected_msr[MSR.TSs:MSR.TSe+1].eq(0b01)
 177                 with m.Else():
 178                     comb += expected_msr[MSR.TSs:MSR.TSe+1].eq(
 179                         op.msr[MSR.TSs:MSR.TSe+1]
 180                     )
 181
 182                 # Power ISA V3.0B, Book 2, Section 3.3.1
 183                 with m.If(field(op.insn, 20, 26) == 1):
 184                     comb += expected_msr[MSR.HV].eq(1)
 185                 with m.Else():
 186                     comb += expected_msr[MSR.HV].eq(0)
 187
 188                 comb += [
 189                     Assert(dut.o.srr0.ok),
 190                     Assert(srr1_o.ok),
 191                     Assert(msr_o.ok),
 192
 193                     Assert(dut.o.srr0.data == (op.cia + 4)[0:64]),
 194                     Assert(field(srr1_o, 33, 36) == 0),
 195                     Assert(field(srr1_o, 42, 47) == 0),
 196                     Assert(field(srr1_o, 0, 32) == field(msr_i, 0, 32)),
 197                     Assert(field(srr1_o, 37, 41) == field(msr_i, 37, 41)),
 198                     Assert(field(srr1_o, 48, 63) == field(msr_i, 48, 63)),
 199
 200                     Assert(msr_o.data == expected_msr),
 201                 ]
 202                 with m.If(field(op.insn, 20, 26) == 1):
 203                     comb += Assert(msr_o[MSR.HV] == 1)
 204                 with m.Else():
 205                     comb += Assert(msr_o[MSR.HV] == 0)
 206
 207             with m.Case(MicrOp.OP_RFID):
 208                 comb += [
 209                     Assert(msr_o.ok),
 210                     Assert(nia_o.ok),
 211
 212                     Assert(msr_o[MSR.HV] == (srr1_i[MSR.HV] & msr_i[MSR.HV])),
 213                     Assert(msr_o[MSR.EE] == (srr1_i[MSR.EE] | srr1_i[MSR.PR])),
 214                     Assert(msr_o[MSR.IR] == (srr1_i[MSR.IR] | srr1_i[MSR.PR])),
 215                     Assert(msr_o[MSR.DR] == (srr1_i[MSR.DR] | srr1_i[MSR.PR])),
 216                     Assert(field(msr_o, 0, 2) == field(srr1_i, 0, 2)),
 217                     Assert(field(msr_o, 4, 28) == field(srr1_i, 4, 28)),
 218                     Assert(msr_o[63-32] == srr1_i[63-32]),
 219                     Assert(field(msr_o, 37, 41) == field(srr1_i, 37, 41)),
 220                     Assert(field(msr_o, 49, 50) == field(srr1_i, 49, 50)),
 221                     Assert(field(msr_o, 52, 57) == field(srr1_i, 52, 57)),
 222                     Assert(field(msr_o, 60, 63) == field(srr1_i, 60, 63)),
 223                     Assert(nia_o.data == Cat(Const(0, 2), dut.i.srr0[2:])),
 224                 ]
 225                 with m.If(msr_i[MSR.HV]):
 226                     comb += Assert(msr_o[MSR.ME] == srr1_i[MSR.ME])
 227                 with m.Else():
 228                     comb += Assert(msr_o[MSR.ME] == msr_i[MSR.ME])
 229                 with m.If((field(msr_i , 29, 31) != 0b010) |
 230                           (field(srr1_i, 29, 31) != 0b000)):
 231                     comb += Assert(field(msr_o.data, 29, 31) ==
 232                                    field(srr1_i, 29, 31))
 233                 with m.Else():
 234                     comb += Assert(field(msr_o.data, 29, 31) ==
 235                                    field(msr_i, 29, 31))
 236
 237         comb += dut.i.ctx.matches(dut.o.ctx)
 238
 239         return m
 240
 241
 242 class TrapMainStageTestCase(FHDLTestCase):
 243     def test_formal(self):
 244         self.assertFormal(Driver(), mode="bmc", depth=10)
 245         self.assertFormal(Driver(), mode="cover", depth=10)
 246
 247     def test_ilang(self):
 248         vl = rtlil.convert(Driver(), ports=[])
 249         with open("trap_main_stage.il", "w") as f:
 250             f.write(vl)
 251
 252
 253 if __name__ == '__main__':
 254     unittest.main()
 255