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 * https://libre-soc.org/openpower/isa/fixedtrap/
   8 * https://libre-soc.org/openpower/isa/sprset/
   9 * https://libre-soc.org/openpower/isa/system/
  10 """
  11
  12
  13 import unittest
  14
  15 from nmigen import Cat, Const, Elaboratable, Module, Signal, signed
  16 from nmigen.asserts import Assert, AnyConst
  17 from nmigen.cli import rtlil
  18
  19 from nmutil.extend import exts
  20 from nmutil.formaltest import FHDLTestCase
  21
  22 from soc.consts import MSR, PI, TT
  23
  24 from soc.decoder.power_enums import MicrOp
  25
  26 from soc.fu.trap.main_stage import TrapMainStage
  27 from soc.fu.trap.pipe_data import TrapPipeSpec
  28 from soc.fu.trap.trap_input_record import CompTrapOpSubset
  29
  30
  31 def field(r, start, end=None):
  32     """Answers with a subfield of the signal r ("register"), where
  33     the start and end bits use IBM conventions.  start < end.
  34     """
  35     if end is None:
  36         return r[63-start]
  37     return r[63-end:64-start]
  38
  39
  40 class Driver(Elaboratable):
  41     """
  42     """
  43
  44     def elaborate(self, platform):
  45         m = Module()
  46         comb = m.d.comb
  47
  48         rec = CompTrapOpSubset()
  49         pspec = TrapPipeSpec(id_wid=2)
  50
  51         m.submodules.dut = dut = TrapMainStage(pspec)
  52
  53         # frequently used aliases
  54         op = dut.i.ctx.op
  55         msr_o, msr_i = dut.o.msr, op.msr
  56         srr0_o, srr0_i = dut.o.srr0, dut.i.srr0
  57         srr1_o, srr1_i = dut.o.srr1, dut.i.srr1
  58         nia_o = dut.o.nia
  59
  60         comb += op.eq(rec)
  61
  62         # start of properties
  63         with m.Switch(op.insn_type):
  64
  65             ###############
  66             # TDI/TWI/TD/TW.  v3.0B p90-91
  67             ###############
  68             with m.Case(MicrOp.OP_TRAP):
  69                 # TODO: put back use of fields, do not access insn bits direct
  70                 # see https://bugs.libre-soc.org/show_bug.cgi?id=421#c24
  71                 to = Signal(5)
  72                 comb += to.eq(op.insn[31-10:31-5])
  73
  74                 a_i = Signal(64)
  75                 b_i = Signal(64)
  76                 comb += a_i.eq(dut.i.a)
  77                 comb += b_i.eq(dut.i.b)
  78
  79                 a_s = Signal(signed(64), reset_less=True)
  80                 b_s = Signal(signed(64), reset_less=True)
  81                 a = Signal(64, reset_less=True)
  82                 b = Signal(64, reset_less=True)
  83
  84                 with m.If(op.is_32bit):
  85                     comb += a_s.eq(exts(a_i, 32, 64))
  86                     comb += b_s.eq(exts(b_i, 32, 64))
  87                     comb += a.eq(a_i[0:32])
  88                     comb += b.eq(b_i[0:32])
  89                 with m.Else():
  90                     comb += a_s.eq(a_i)
  91                     comb += b_s.eq(b_i)
  92                     comb += a.eq(a_i)
  93                     comb += b.eq(b_i)
  94
  95                 lt_s = Signal(reset_less=True)
  96                 gt_s = Signal(reset_less=True)
  97                 lt_u = Signal(reset_less=True)
  98                 gt_u = Signal(reset_less=True)
  99                 equal = Signal(reset_less=True)
 100
 101                 comb += lt_s.eq(a_s < b_s)
 102                 comb += gt_s.eq(a_s > b_s)
 103                 comb += lt_u.eq(a < b)
 104                 comb += gt_u.eq(a > b)
 105                 comb += equal.eq(a == b)
 106
 107                 trapbits = Signal(5, reset_less=True)
 108                 comb += trapbits.eq(Cat(gt_u, lt_u, equal, gt_s, lt_s))
 109
 110                 take_trap = Signal()
 111                 traptype = op.traptype
 112                 comb += take_trap.eq(traptype.any() | (trapbits & to).any())
 113
 114                 with m.If(take_trap):
 115                     expected_msr = Signal(len(msr_o.data))
 116                     comb += expected_msr.eq(op.msr)
 117
 118                     comb += expected_msr[MSR.IR].eq(0)
 119                     comb += expected_msr[MSR.DR].eq(0)
 120                     comb += expected_msr[MSR.FE0].eq(0)
 121                     comb += expected_msr[MSR.FE1].eq(0)
 122                     comb += expected_msr[MSR.EE].eq(0)
 123                     comb += expected_msr[MSR.RI].eq(0)
 124                     comb += expected_msr[MSR.SF].eq(1)
 125                     comb += expected_msr[MSR.TM].eq(0)
 126                     comb += expected_msr[MSR.VEC].eq(0)
 127                     comb += expected_msr[MSR.VSX].eq(0)
 128                     comb += expected_msr[MSR.PR].eq(0)
 129                     comb += expected_msr[MSR.FP].eq(0)
 130                     comb += expected_msr[MSR.PMM].eq(0)
 131                     comb += expected_msr[MSR.TEs:MSR.TEe+1].eq(0)
 132                     comb += expected_msr[MSR.UND].eq(0)
 133                     comb += expected_msr[MSR.LE].eq(1)
 134
 135                     with m.If(op.msr[MSR.TSs:MSR.TSe+1] == 0b10):
 136                         comb += expected_msr[MSR.TSs:MSR.TSe+1].eq(0b01)
 137                     with m.Else():
 138                         comb += expected_msr[MSR.TSs:MSR.TSe+1].eq(
 139                             op.msr[MSR.TSs:MSR.TSe+1]
 140                         )
 141
 142                     expected_srr1 = Signal(len(srr1_o.data))
 143                     comb += expected_srr1.eq(op.msr)
 144
 145                     comb += expected_srr1[63-36:63-32].eq(0)
 146                     comb += expected_srr1[PI.TRAP].eq(traptype == 0)
 147                     comb += expected_srr1[PI.PRIV].eq(traptype[1])
 148                     comb += expected_srr1[PI.FP].eq(traptype[0])
 149                     comb += expected_srr1[PI.ADR].eq(traptype[3])
 150                     comb += expected_srr1[PI.ILLEG].eq(traptype[4])
 151                     comb += expected_srr1[PI.TM_BAD_THING].eq(0)
 152
 153                     comb += [
 154                         Assert(msr_o.ok),
 155                         Assert(msr_o.data == expected_msr),
 156                         Assert(srr0_o.ok),
 157                         Assert(srr0_o.data == op.cia),
 158                         Assert(srr1_o.ok),
 159                         Assert(srr1_o.data == expected_srr1),
 160                         Assert(nia_o.ok),
 161                         Assert(nia_o.data == op.trapaddr << 4),
 162                     ]
 163
 164             #################
 165             # SC.  v3.0B p952
 166             #################
 167             with m.Case(MicrOp.OP_SC):
 168                 expected_msr = Signal(len(msr_o.data))
 169                 comb += expected_msr.eq(op.msr)
 170                 # Unless otherwise documented, these exceptions to the MSR bits
 171                 # are documented in Power ISA V3.0B, page 1063 or 1064.
 172                 comb += expected_msr[MSR.IR].eq(0)
 173                 comb += expected_msr[MSR.DR].eq(0)
 174                 comb += expected_msr[MSR.FE0].eq(0)
 175                 comb += expected_msr[MSR.FE1].eq(0)
 176                 comb += expected_msr[MSR.EE].eq(0)
 177                 comb += expected_msr[MSR.RI].eq(0)
 178                 comb += expected_msr[MSR.SF].eq(1)
 179                 comb += expected_msr[MSR.TM].eq(0)
 180                 comb += expected_msr[MSR.VEC].eq(0)
 181                 comb += expected_msr[MSR.VSX].eq(0)
 182                 comb += expected_msr[MSR.PR].eq(0)
 183                 comb += expected_msr[MSR.FP].eq(0)
 184                 comb += expected_msr[MSR.PMM].eq(0)
 185                 # TODO: check ordering (which is smaller, which is larger)
 186                 # MSR.TSs or MSR.TSe+1?
 187                 comb += expected_msr[MSR.TEs:MSR.TEe+1].eq(0)
 188                 comb += expected_msr[MSR.UND].eq(0)
 189                 comb += expected_msr[MSR.LE].eq(1)
 190
 191                 # TODO: check ordering (which is smaller, which is larger)
 192                 # MSR.TSs or MSR.TSe+1?
 193                 # see https://bugs.libre-soc.org/show_bug.cgi?id=325#c107
 194                 with m.If(op.msr[MSR.TSs:MSR.TSe+1] == 0b10):
 195                     comb += expected_msr[MSR.TSs:MSR.TSe+1].eq(0b01)
 196                 with m.Else():
 197                     comb += expected_msr[MSR.TSs:MSR.TSe+1].eq(
 198                         op.msr[MSR.TSs:MSR.TSe+1]
 199                     )
 200
 201                 # Power ISA V3.0B, Book 2, Section 3.3.1
 202                 # TODO: put back use of fields, do not access insn bits direct
 203                 # see https://bugs.libre-soc.org/show_bug.cgi?id=421#c24
 204                 with m.If(field(op.insn, 20, 26) == 1):
 205                     comb += expected_msr[MSR.HV].eq(1)
 206                 with m.Else():
 207                     comb += expected_msr[MSR.HV].eq(0)
 208
 209                 comb += [
 210                     Assert(dut.o.srr0.ok),
 211                     Assert(srr1_o.ok),
 212                     Assert(msr_o.ok),
 213
 214                     Assert(dut.o.srr0.data == (op.cia + 4)[0:64]),
 215                     Assert(field(srr1_o, 33, 36) == 0),
 216                     Assert(field(srr1_o, 42, 47) == 0),
 217                     Assert(field(srr1_o, 0, 32) == field(msr_i, 0, 32)),
 218                     Assert(field(srr1_o, 37, 41) == field(msr_i, 37, 41)),
 219                     Assert(field(srr1_o, 48, 63) == field(msr_i, 48, 63)),
 220
 221                     Assert(msr_o.data == expected_msr),
 222                 ]
 223                 # TODO: put back use of fields, do not access insn bits direct
 224                 # see https://bugs.libre-soc.org/show_bug.cgi?id=421#c24
 225                 # XXX what is this for?  it is not possible to identify
 226                 # it because the "direct access to insn bits" provides
 227                 # absolutely no clue as to its purpose.
 228                 # also: this is likely to be wrong because of PowerISA
 229                 # field ordering (see V3.0B p4 section 1.3.4)
 230                 with m.If(field(op.insn, 20, 26) == 1):
 231                     comb += Assert(msr_o[MSR.HV] == 1)
 232                 with m.Else():
 233                     comb += Assert(msr_o[MSR.HV] == 0)
 234
 235             ###################
 236             # RFID.  v3.0B p955
 237             ###################
 238             with m.Case(MicrOp.OP_RFID):
 239                 comb += [
 240                     Assert(msr_o.ok),
 241                     Assert(nia_o.ok),
 242                     ]
 243
 244                 # Note: going through the spec pseudo-code, line-by-line,
 245                 # in order, with these assertions.  idea is: compare
 246                 # *directly* against the pseudo-code.  therefore, leave
 247                 # numbering in (from pseudo-code) and add *comments* about
 248                 # which field it is (3 == HV etc.)
 249
 250                 # spec: MSR[51] <- (MSR[3] & SRR1[51]) | ((¬MSR[3] & MSR[51]))
 251                 with m.If(field(msr_i, 3)): # HV
 252                     comb += Assert(field(msr_o, 51) == field(srr1_i, 51) # ME
 253                 with m.Else():
 254                     comb += Assert(field(msr_o, 51) == field(msr_i, 51)) # ME
 255
 256                 comb += [
 257                     # spec: MSR[3] <- (MSR[3] & SRR1[3])
 258                     Assert(field(msr_o, 3) == (field(srr1_i, 3) &
 259                                                field(msr_i, 3))), # HV
 260                 ]
 261
 262                 # if (MSR[29:31] != 0b010) | (SRR1[29:31] != 0b000) then
 263                 #     MSR[29:31] <- SRR1[29:31]
 264                 with m.If((field(msr_i , 29, 31) != 0b010) |
 265                           (field(srr1_i, 29, 31) != 0b000)):
 266                     comb += Assert(field(msr_o.data, 29, 31) ==
 267                                    field(srr1_i, 29, 31))
 268                 with m.Else():
 269                     comb += Assert(field(msr_o.data, 29, 31) ==
 270                                    field(msr_i, 29, 31))
 271
 272                 # check EE (48) IR (58), DR (59): PR (49) will over-ride
 273                 comb += [
 274                     Assert(msr_o[48] == (srr1_i[48] | srr1_i[48])), # EE
 275                     Assert(msr_o[58] == (srr1_i[58] | srr1_i[58])), # IR
 276                     Assert(msr_o[59] == (srr1_i[59] | srr1_i[59])), # DR
 277                 ]
 278
 279                 # remaining bits: straight copy.  don't know what these are:
 280                 # just trust the v3.0B spec is correct.
 281                 comb += [
 282                     Assert(field(msr_o, 0, 2) == field(srr1_i, 0, 2)),
 283                     Assert(field(msr_o, 4, 28) == field(srr1_i, 4, 28)),
 284                     Assert(field(msr_o, 32) == field(srr1_i, 32)),
 285                     Assert(field(msr_o, 37, 41) == field(srr1_i, 37, 41)),
 286                     Assert(field(msr_o, 49, 50) == field(srr1_i, 49, 50)),
 287                     Assert(field(msr_o, 52, 57) == field(srr1_i, 52, 57)),
 288                     Assert(field(msr_o, 60, 63) == field(srr1_i, 60, 63)),
 289                 ]
 290
 291                 # check NIA against SRR0.  2 LSBs are set to zero (word-align)
 292                 comb += Assert(nia_o.data == Cat(Const(0, 2), dut.i.srr0[2:]))
 293
 294         comb += dut.i.ctx.matches(dut.o.ctx)
 295
 296         return m
 297
 298
 299 class TrapMainStageTestCase(FHDLTestCase):
 300     def test_formal(self):
 301         self.assertFormal(Driver(), mode="bmc", depth=10)
 302         self.assertFormal(Driver(), mode="cover", depth=10)
 303
 304     def test_ilang(self):
 305         vl = rtlil.convert(Driver(), ports=[])
 306         with open("trap_main_stage.il", "w") as f:
 307             f.write(vl)
 308
 309
 310 if __name__ == '__main__':
 311     unittest.main()
 312