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                     Assert(msr_o.data == exp_msr),
 204                     Assert(msr_o.ok),
 205                 ]
 206
 207             ###################
 208             # MTMSRD
 209             # Specs found on V3.0B, page 978.
 210             ###################
 211
 212             with m.Case(MicrOp.OP_MTMSRD):
 213                 comb += exp_msr.eq(msr_i)    # will copy and override
 214
 215                 with m.If(L == 0):
 216                     with m.If((field(msr_i, 29, 31) != 0b010) |
 217                               (field(rs, 29, 31) != 0b000)):
 218                         comb += field(exp_msr, 29, 31).eq(F(rs, 29, 31)),
 219
 220                     comb += [
 221                         field(exp_msr, 48).eq(F(rs, 48) | F(rs, 49)),
 222                         field(exp_msr, 58).eq(F(rs, 58) | F(rs, 49)),
 223                         field(exp_msr, 59).eq(F(rs, 59) | F(rs, 49)),
 224                         field(exp_msr, 0, 2).eq(field(rs, 0, 2)),
 225
 226                         # Ambiguity in specification on page 978 of V3.0B:
 227                         # MSR[4:28] <- RS[4 6:28].
 228                         #
 229                         # I've decided to follow the prose in the programmer
 230                         # note just underneath the typographical ambiguity.
 231                         # MSR[4:28] <- RS[4:28].
 232                         field(exp_msr, 4, 28).eq(field(rs, 4, 28)),
 233
 234                         field(exp_msr, 32, 47).eq(field(rs, 32, 47)),
 235                         field(exp_msr, 49, 50).eq(field(rs, 49, 50)),
 236                         field(exp_msr, 52, 57).eq(field(rs, 52, 57)),
 237                         field(exp_msr, 60, 62).eq(field(rs, 60, 62)),
 238                     ]
 239                 with m.Else():
 240                     comb += [
 241                         field(exp_msr, 48).eq(field(rs, 48)),
 242                         field(exp_msr, 62).eq(field(rs, 62)),
 243                     ]
 244
 245                 comb += [
 246                     Assert(msr_o.data == exp_msr),
 247                     Assert(msr_o.ok),
 248                 ]
 249
 250             ###################
 251             # MFMSR
 252             ###################
 253
 254             with m.Case(MicrOp.OP_MFMSR):
 255                 comb += [
 256                     Assert(dut.o.o.ok),
 257                     Assert(dut.o.o.data == msr_i),
 258                 ]
 259
 260             ###################
 261             # RFID.  v3.0B p955
 262             ###################
 263             with m.Case(MicrOp.OP_RFID):
 264                 comb += [
 265                     Assert(msr_o.ok),
 266                     Assert(nia_o.ok),
 267                 ]
 268
 269                 # Note: going through the spec pseudo-code, line-by-line,
 270                 # in order, with these assertions.  idea is: compare
 271                 # *directly* against the pseudo-code.  therefore, leave
 272                 # numbering in (from pseudo-code) and add *comments* about
 273                 # which field it is (3 == HV etc.)
 274
 275                 # spec: MSR[51] <- (MSR[3] & SRR1[51]) | ((¬MSR[3] & MSR[51]))
 276                 with m.If(field(msr_i, 3)): # HV
 277                     comb += Assert(field(msr_o, 51) == field(srr1_i, 51)) # ME
 278                 with m.Else():
 279                     comb += Assert(field(msr_o, 51) == field(msr_i, 51)) # ME
 280
 281                 # if (MSR[29:31] != 0b010) | (SRR1[29:31] != 0b000) then
 282                 #     MSR[29:31] <- SRR1[29:31]
 283                 with m.If((field(msr_i , 29, 31) != 0b010) |
 284                           (field(srr1_i, 29, 31) != 0b000)):
 285                     comb += Assert(field(msr_o.data, 29, 31) ==
 286                                    field(srr1_i, 29, 31))
 287                 with m.Else():
 288                     comb += Assert(field(msr_o.data, 29, 31) ==
 289                                    field(msr_i, 29, 31))
 290
 291                 # check EE (48) IR (58), DR (59): PR (49) will over-ride
 292                 PR = field(srr1_i, 49) # alias/copy of SRR1 PR field
 293                 comb += [
 294                     Assert(field(msr_o, 48) == field(srr1_i, 48) | PR), # EE
 295                     Assert(field(msr_o, 58) == field(srr1_i, 58) | PR), # IR
 296                     Assert(field(msr_o, 59) == field(srr1_i, 59) | PR), # DR
 297                 ]
 298
 299                 # remaining bits: straight copy.  don't know what these are:
 300                 # just trust the v3.0B spec is correct.
 301                 comb += [
 302                     Assert(field(msr_o, 0, 2) == field(srr1_i, 0, 2)),
 303                     Assert(field(msr_o, 4, 28) == field(srr1_i, 4, 28)),
 304                     Assert(field(msr_o, 32) == field(srr1_i, 32)),
 305                     Assert(field(msr_o, 37, 41) == field(srr1_i, 37, 41)),
 306                     Assert(field(msr_o, 49, 50) == field(srr1_i, 49, 50)),
 307                     Assert(field(msr_o, 52, 57) == field(srr1_i, 52, 57)),
 308                     Assert(field(msr_o, 60, 63) == field(srr1_i, 60, 63)),
 309                 ]
 310
 311                 # check NIA against SRR0.  2 LSBs are set to zero (word-align)
 312                 comb += Assert(nia_o.data == Cat(Const(0, 2), dut.i.srr0[2:]))
 313
 314             #################
 315             # SC.  v3.0B p952
 316             #################
 317             with m.Case(MicrOp.OP_SC):
 318                 comb += exp_msr.eq(op.msr)
 319                 # Unless otherwise documented, these exceptions to the MSR bits
 320                 # are documented in Power ISA V3.0B, page 1063 or 1064.
 321                 # We are not supporting hypervisor or transactional semantics,
 322                 # so we skip enforcing those fields' properties.
 323                 comb += field(exp_msr, MSRb.IR).eq(0)
 324                 comb += field(exp_msr, MSRb.DR).eq(0)
 325                 comb += field(exp_msr, MSRb.FE0).eq(0)
 326                 comb += field(exp_msr, MSRb.FE1).eq(0)
 327                 comb += field(exp_msr, MSRb.EE).eq(0)
 328                 comb += field(exp_msr, MSRb.RI).eq(0)
 329                 comb += field(exp_msr, MSRb.SF).eq(1)
 330                 comb += field(exp_msr, MSRb.TM).eq(0)
 331                 comb += field(exp_msr, MSRb.VEC).eq(0)
 332                 comb += field(exp_msr, MSRb.VSX).eq(0)
 333                 comb += field(exp_msr, MSRb.PR).eq(0)
 334                 comb += field(exp_msr, MSRb.FP).eq(0)
 335                 comb += field(exp_msr, MSRb.PMM).eq(0)
 336                 comb += field(exp_msr, MSRb.TEs, MSRb.TEe).eq(0)
 337                 comb += field(exp_msr, MSRb.UND).eq(0)
 338                 comb += field(exp_msr, MSRb.LE).eq(1)
 339
 340                 comb += [
 341                     Assert(dut.o.srr0.ok),
 342                     Assert(srr1_o.ok),
 343                     Assert(msr_o.ok),
 344
 345                     Assert(dut.o.srr0.data == (op.cia + 4)[0:64]),
 346                     Assert(field(srr1_o, 33, 36) == 0),
 347                     Assert(field(srr1_o, 42, 47) == 0),
 348                     Assert(field(srr1_o, 0, 32) == field(msr_i, 0, 32)),
 349                     Assert(field(srr1_o, 37, 41) == field(msr_i, 37, 41)),
 350                     Assert(field(srr1_o, 48, 63) == field(msr_i, 48, 63)),
 351
 352                     Assert(msr_o.data == exp_msr),
 353                 ]
 354
 355         comb += dut.i.ctx.matches(dut.o.ctx)
 356
 357         return m
 358
 359
 360 class TrapMainStageTestCase(FHDLTestCase):
 361     def test_formal(self):
 362         self.assertFormal(Driver(), mode="bmc", depth=10)
 363         self.assertFormal(Driver(), mode="cover", depth=10)
 364
 365     def test_ilang(self):
 366         vl = rtlil.convert(Driver(), ports=[])
 367         with open("trap_main_stage.il", "w") as f:
 368             f.write(vl)
 369
 370
 371 if __name__ == '__main__':
 372     unittest.main()
 373