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