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, MSRb, PI, TT, field
  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 class Driver(Elaboratable):
  32     """
  33     """
  34
  35     def elaborate(self, platform):
  36         m = Module()
  37         comb = m.d.comb
  38
  39         rec = CompTrapOpSubset()
  40         pspec = TrapPipeSpec(id_wid=2)
  41
  42         m.submodules.dut = dut = TrapMainStage(pspec)
  43
  44         # frequently used aliases
  45         op = dut.i.ctx.op
  46         msr_o, msr_i = dut.o.msr, op.msr
  47         srr0_o, srr0_i = dut.o.srr0, dut.i.srr0
  48         srr1_o, srr1_i = dut.o.srr1, dut.i.srr1
  49         nia_o = dut.o.nia
  50         rs = dut.i.a
  51
  52         comb += op.eq(rec)
  53
  54         # expected values
  55         exp_msr = Signal(len(msr_o.data))
  56         exp_srr1 = Signal(len(srr1_o.data))
  57
  58         d_fields = dut.fields.FormD
  59         sc_fields = dut.fields.FormSC
  60         x_fields = dut.fields.FormX
  61
  62         L = x_fields.L[0:-1]
  63
  64         # This alias exists because some of our assertions exceed PEP8
  65         # width constraints.  Avoid using this alias in the general
  66         # case; ONLY use it when you're simultaneously trying to preserve
  67         # line-oriented readibility while preserving PEP8 compliance.
  68         F = field
  69
  70         # start of properties
  71         with m.Switch(op.insn_type):
  72
  73             ###############
  74             # TDI/TWI/TD/TW.  v3.0B p90-91
  75             ###############
  76             with m.Case(MicrOp.OP_TRAP):
  77                 to = Signal(len(d_fields.TO))
  78                 comb += to.eq(d_fields.TO[0:-1])
  79
  80                 a_i = Signal(64)
  81                 b_i = Signal(64)
  82                 comb += a_i.eq(dut.i.a)
  83                 comb += b_i.eq(dut.i.b)
  84
  85                 a_s = Signal(signed(64), reset_less=True)
  86                 b_s = Signal(signed(64), reset_less=True)
  87                 a = Signal(64, reset_less=True)
  88                 b = Signal(64, reset_less=True)
  89
  90                 with m.If(op.is_32bit):
  91                     comb += a_s.eq(exts(a_i, 32, 64))
  92                     comb += b_s.eq(exts(b_i, 32, 64))
  93                     comb += a.eq(a_i[0:32])
  94                     comb += b.eq(b_i[0:32])
  95                 with m.Else():
  96                     comb += a_s.eq(a_i)
  97                     comb += b_s.eq(b_i)
  98                     comb += a.eq(a_i)
  99                     comb += b.eq(b_i)
 100
 101                 lt_s = Signal(reset_less=True)
 102                 gt_s = Signal(reset_less=True)
 103                 lt_u = Signal(reset_less=True)
 104                 gt_u = Signal(reset_less=True)
 105                 equal = Signal(reset_less=True)
 106
 107                 comb += lt_s.eq(a_s < b_s)
 108                 comb += gt_s.eq(a_s > b_s)
 109                 comb += lt_u.eq(a < b)
 110                 comb += gt_u.eq(a > b)
 111                 comb += equal.eq(a == b)
 112
 113                 trapbits = Signal(5, reset_less=True)
 114                 comb += trapbits.eq(Cat(gt_u, lt_u, equal, gt_s, lt_s))
 115
 116                 take_trap = Signal()
 117                 traptype = op.traptype
 118                 comb += take_trap.eq(traptype.any() | (trapbits & to).any())
 119
 120                 with m.If(take_trap):
 121                     comb += exp_msr.eq(op.msr)
 122
 123                     comb += field(exp_msr, MSRb.IR).eq(0)
 124                     comb += field(exp_msr, MSRb.DR).eq(0)
 125                     comb += field(exp_msr, MSRb.FE0).eq(0)
 126                     comb += field(exp_msr, MSRb.FE1).eq(0)
 127                     comb += field(exp_msr, MSRb.EE).eq(0)
 128                     comb += field(exp_msr, MSRb.RI).eq(0)
 129                     comb += field(exp_msr, MSRb.SF).eq(1)
 130                     comb += field(exp_msr, MSRb.TM).eq(0)
 131                     comb += field(exp_msr, MSRb.VEC).eq(0)
 132                     comb += field(exp_msr, MSRb.VSX).eq(0)
 133                     comb += field(exp_msr, MSRb.PR).eq(0)
 134                     comb += field(exp_msr, MSRb.FP).eq(0)
 135                     comb += field(exp_msr, MSRb.PMM).eq(0)
 136
 137                     # still wrong.
 138                     # see https://bugs.libre-soc.org/show_bug.cgi?id=325#c120
 139                     #
 140                     # saf2: no it's not.  Proof by substitution:
 141                     #
 142                     # field(R,MSRb.TEs,MSRb.TEe).eq(0)
 143                     # == field(R,53,54).eq(0)
 144                     # == R[field_slice(53,54)].eq(0)
 145                     # == R[slice(63-54, (63-53)+1)].eq(0)
 146                     # == R[slice(9, 11)].eq(0)
 147                     # == R[9:11].eq(0)
 148                     #
 149                     # Also put proof in py-doc for field().
 150
 151                     comb += field(exp_msr, MSRb.TEs, MSRb.TEe).eq(0)
 152
 153                     comb += field(exp_msr, MSRb.UND).eq(0)
 154                     comb += field(exp_msr, MSRb.LE).eq(1)
 155
 156                     comb += exp_srr1.eq(op.msr)
 157
 158                     # Per V3.0B, page 1075
 159                     comb += field(exp_srr1, 33, 36).eq(0)
 160                     comb += field(exp_srr1, 42).eq(0)  # TM_BAD_THING
 161                     comb += field(exp_srr1, 43).eq(traptype[0])    # FP
 162                     comb += field(exp_srr1, 44).eq(traptype[4])    # ILLEG
 163                     comb += field(exp_srr1, 45).eq(traptype[1])    # PRIV
 164                     comb += field(exp_srr1, 46).eq(traptype == 0)  # TRAP
 165                     comb += field(exp_srr1, 47).eq(traptype[3])    # ADDR
 166
 167                     comb += [
 168                         Assert(msr_o.ok),
 169                         Assert(msr_o.data == exp_msr),
 170                         Assert(srr0_o.ok),
 171                         Assert(srr0_o.data == op.cia),
 172                         Assert(srr1_o.ok),
 173                         Assert(srr1_o.data == exp_srr1),
 174                         Assert(nia_o.ok),
 175                         Assert(nia_o.data == op.trapaddr << 4),
 176                     ]
 177
 178             ###################
 179             # MTMSR
 180             # Specs found on V3.0B, page 977.
 181             ###################
 182
 183             with m.Case(MicrOp.OP_MTMSR):
 184                 comb += exp_msr.eq(msr_i)    # will copy and override
 185
 186                 with m.If(L == 0):
 187                     comb += [
 188                         field(exp_msr, 48).eq(F(rs, 48) | F(rs, 49)),
 189                         field(exp_msr, 58).eq(F(rs, 58) | F(rs, 49)),
 190                         field(exp_msr, 59).eq(F(rs, 59) | F(rs, 49)),
 191                         field(exp_msr, 32, 47).eq(field(rs, 32, 47)),
 192                         field(exp_msr, 49, 50).eq(field(rs, 49, 50)),
 193                         field(exp_msr, 52, 57).eq(field(rs, 52, 57)),
 194                         field(exp_msr, 60, 62).eq(field(rs, 60, 62)),
 195                     ]
 196                 with m.Else():
 197                     comb += [
 198                         field(exp_msr, 48).eq(field(rs, 48)),
 199                         field(exp_msr, 62).eq(field(rs, 62)),
 200                     ]
 201
 202                 comb += [
 203                     # L=1 only checks 48 and 62
 204                     Assert(msr_o.data == exp_msr),
 205                     Assert(msr_o.ok),
 206                 ]
 207
 208             ###################
 209             # MTMSRD
 210             # Specs found on V3.0B, page 978.
 211             ###################
 212
 213             with m.Case(MicrOp.OP_MTMSRD):
 214                 msr_od = msr_o.data
 215
 216                 with m.If(L == 0):
 217                     # if (MSR[29:31] != 0b010) | (SRR1[29:31] != 0b000) then
 218                     #     MSR[29:31] <- SRR1[29:31]
 219                     with m.If((field(msr_i, 29, 31) != 0b010) |
 220                               (field(rs, 29, 31) != 0b000)):
 221                         comb += Assert(F(msr_od, 29, 31) == F(rs, 29, 31))
 222                     with m.Else():
 223                         comb += Assert(F(msr_od, 29, 31) == F(msr_i, 29, 31))
 224
 225                     # MSR[48] <- (RS)[48] | (RS)[49]
 226                     # MSR[58] <- (RS)[58] | (RS)[49]
 227                     # MSR[59] <- (RS)[59] | (RS)[49]
 228                     PR = field(rs, 49) # alias/copy of SRR1 PR field
 229                     comb += [
 230                         Assert(field(msr_od, 48) == F(rs, 48) | PR),
 231                         Assert(field(msr_od, 58) == F(rs, 58) | PR),
 232                         Assert(field(msr_od, 59) == F(rs, 59) | PR),
 233                     ]
 234
 235                     comb += [
 236                         # XXX Ambiguity in specification on page 978 of V3.0B:
 237                         #   MSR[4:28] <- RS[4 6:28].
 238                         #
 239                         # I've decided to follow the prose in the programmer
 240                         # note just underneath the typographical ambiguity.
 241                         #   MSR[4:28] <- RS[4:28].
 242
 243                         # range = 0:2 4:28 32:40 42:47 49:50 52:57 60:62
 244                         # MSR[range] <- (RS)[range]
 245                         Assert(field(msr_od, 0, 2) == field(rs, 0, 2)),
 246                         Assert(field(msr_od, 4, 28) == field(rs, 4, 28)),
 247                         Assert(field(msr_od, 32, 47) == field(rs, 32, 47)),
 248                         Assert(field(msr_od, 49, 50) == field(rs, 49, 50)),
 249                         Assert(field(msr_od, 52, 57) == field(rs, 52, 57)),
 250                         Assert(field(msr_od, 60, 62) == field(rs, 60, 62)),
 251                     ]
 252                 with m.Else():
 253                     # L=1 only checks 48 and 62
 254                     comb += [
 255                         Assert(field(msr_od, 48) == field(rs, 48)),
 256                         Assert(field(msr_od, 62) == field(rs, 62)),
 257                     ]
 258
 259                 comb += Assert(msr_o.ok)
 260
 261             ###################
 262             # MFMSR
 263             ###################
 264
 265             with m.Case(MicrOp.OP_MFMSR):
 266                 comb += [
 267                     Assert(dut.o.o.ok),
 268                     Assert(dut.o.o.data == msr_i),
 269                 ]
 270
 271             ###################
 272             # RFID.  v3.0B p955
 273             ###################
 274             with m.Case(MicrOp.OP_RFID):
 275                 msr_od = msr_o.data
 276                 comb += [
 277                     Assert(msr_o.ok),
 278                     Assert(nia_o.ok),
 279                 ]
 280
 281                 # Note: going through the spec pseudo-code, line-by-line,
 282                 # in order, with these assertions.  idea is: compare
 283                 # *directly* against the pseudo-code.  therefore, leave
 284                 # numbering in (from pseudo-code) and add *comments* about
 285                 # which field it is (3 == HV etc.)
 286
 287                 # spec: MSR[51] <- MSR[3] & SRR1[51]
 288                 comb += Assert(field(msr_o, 3) == field(srr1_i, 3))
 289
 290                 # if (MSR[29:31] != 0b010) | (SRR1[29:31] != 0b000) then
 291                 #     MSR[29:31] <- SRR1[29:31]
 292                 with m.If((field(msr_i , 29, 31) != 0b010) |
 293                           (field(srr1_i, 29, 31) != 0b000)):
 294                     comb += Assert(F(msr_od, 29, 31) == F(srr1_i, 29, 31))
 295                 with m.Else():
 296                     comb += Assert(F(msr_od, 29, 31) == F(msr_i, 29, 31))
 297
 298                 # check EE (48) IR (58), DR (59): PR (49) will over-ride
 299                 # MSR[48] <- (RS)[48] | (RS)[49]
 300                 # MSR[58] <- (RS)[58] | (RS)[49]
 301                 # MSR[59] <- (RS)[59] | (RS)[49]
 302                 PR = field(srr1_i, 49) # alias/copy of SRR1 PR field
 303                 comb += [
 304                     Assert(field(msr_od, 48) == field(srr1_i, 48) | PR),
 305                     Assert(field(msr_od, 58) == field(srr1_i, 58) | PR),
 306                     Assert(field(msr_od, 59) == field(srr1_i, 59) | PR),
 307                 ]
 308
 309                 # remaining bits: straight copy.  don't know what these are:
 310                 # just trust the v3.0B spec is correct.
 311                 # range = 0:2 4:28 32:40 42:47 49:50 52:57 60:62
 312                 # MSR[range] <- (RS)[range]
 313                 comb += [
 314                     Assert(field(msr_od, 0, 2) == field(srr1_i, 0, 2)),
 315                     Assert(field(msr_od, 4, 28) == field(srr1_i, 4, 28)),
 316                     Assert(field(msr_od, 32) == field(srr1_i, 32)),
 317                     Assert(field(msr_od, 37, 41) == field(srr1_i, 37, 41)),
 318                     Assert(field(msr_od, 49, 50) == field(srr1_i, 49, 50)),
 319                     Assert(field(msr_od, 52, 57) == field(srr1_i, 52, 57)),
 320                     Assert(field(msr_od, 60, 63) == field(srr1_i, 60, 63)),
 321                 ]
 322
 323                 # check NIA against SRR0.  2 LSBs are set to zero (word-align)
 324                 comb += Assert(nia_o.data == Cat(Const(0, 2), dut.i.srr0[2:]))
 325
 326             #################
 327             # SC.  v3.0B p952
 328             #################
 329             with m.Case(MicrOp.OP_SC):
 330                 comb += exp_msr.eq(op.msr)
 331                 # Unless otherwise documented, these exceptions to the MSR bits
 332                 # are documented in Power ISA V3.0B, page 1063 or 1064.
 333                 # We are not supporting hypervisor or transactional semantics,
 334                 # so we skip enforcing those fields' properties.
 335                 comb += field(exp_msr, MSRb.IR).eq(0)
 336                 comb += field(exp_msr, MSRb.DR).eq(0)
 337                 comb += field(exp_msr, MSRb.FE0).eq(0)
 338                 comb += field(exp_msr, MSRb.FE1).eq(0)
 339                 comb += field(exp_msr, MSRb.EE).eq(0)
 340                 comb += field(exp_msr, MSRb.RI).eq(0)
 341                 comb += field(exp_msr, MSRb.SF).eq(1)
 342                 comb += field(exp_msr, MSRb.TM).eq(0)
 343                 comb += field(exp_msr, MSRb.VEC).eq(0)
 344                 comb += field(exp_msr, MSRb.VSX).eq(0)
 345                 comb += field(exp_msr, MSRb.PR).eq(0)
 346                 comb += field(exp_msr, MSRb.FP).eq(0)
 347                 comb += field(exp_msr, MSRb.PMM).eq(0)
 348                 comb += field(exp_msr, MSRb.TEs, MSRb.TEe).eq(0)
 349                 comb += field(exp_msr, MSRb.UND).eq(0)
 350                 comb += field(exp_msr, MSRb.LE).eq(1)
 351
 352                 comb += [
 353                     Assert(dut.o.srr0.ok),
 354                     Assert(srr1_o.ok),
 355                     Assert(msr_o.ok),
 356
 357                     Assert(dut.o.srr0.data == (op.cia + 4)[0:64]),
 358                     Assert(field(srr1_o, 33, 36) == 0),
 359                     Assert(field(srr1_o, 42, 47) == 0),
 360                     Assert(field(srr1_o, 0, 32) == field(msr_i, 0, 32)),
 361                     Assert(field(srr1_o, 37, 41) == field(msr_i, 37, 41)),
 362                     Assert(field(srr1_o, 48, 63) == field(msr_i, 48, 63)),
 363
 364                     Assert(msr_o.data == exp_msr),
 365                 ]
 366
 367         comb += dut.i.ctx.matches(dut.o.ctx)
 368
 369         return m
 370
 371
 372 class TrapMainStageTestCase(FHDLTestCase):
 373     def test_formal(self):
 374         self.assertFormal(Driver(), mode="bmc", depth=10)
 375         self.assertFormal(Driver(), mode="cover", depth=10)
 376
 377     def test_ilang(self):
 378         vl = rtlil.convert(Driver(), ports=[])
 379         with open("trap_main_stage.il", "w") as f:
 380             f.write(vl)
 381
 382
 383 if __name__ == '__main__':
 384     unittest.main()
 385