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[3-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                 comb += expected_msr[MSR.TEs:MSR.TEe+1].eq(0)
 186                 comb += expected_msr[MSR.UND].eq(0)
 187                 comb += expected_msr[MSR.LE].eq(1)
 188
 189                 with m.If(op.msr[MSR.TSs:MSR.TSe+1] == 0b10):
 190                     comb += expected_msr[MSR.TSs:MSR.TSe+1].eq(0b01)
 191                 with m.Else():
 192                     comb += expected_msr[MSR.TSs:MSR.TSe+1].eq(
 193                         op.msr[MSR.TSs:MSR.TSe+1]
 194                     )
 195
 196                 # Power ISA V3.0B, Book 2, Section 3.3.1
 197                 # TODO: put back use of fields, do not access insn bits direct
 198                 # see https://bugs.libre-soc.org/show_bug.cgi?id=421#c24
 199                 with m.If(field(op.insn, 20, 26) == 1):
 200                     comb += expected_msr[MSR.HV].eq(1)
 201                 with m.Else():
 202                     comb += expected_msr[MSR.HV].eq(0)
 203
 204                 comb += [
 205                     Assert(dut.o.srr0.ok),
 206                     Assert(srr1_o.ok),
 207                     Assert(msr_o.ok),
 208
 209                     Assert(dut.o.srr0.data == (op.cia + 4)[0:64]),
 210                     Assert(field(srr1_o, 33, 36) == 0),
 211                     Assert(field(srr1_o, 42, 47) == 0),
 212                     Assert(field(srr1_o, 0, 32) == field(msr_i, 0, 32)),
 213                     Assert(field(srr1_o, 37, 41) == field(msr_i, 37, 41)),
 214                     Assert(field(srr1_o, 48, 63) == field(msr_i, 48, 63)),
 215
 216                     Assert(msr_o.data == expected_msr),
 217                 ]
 218                 # TODO: put back use of fields, do not access insn bits direct
 219                 # see https://bugs.libre-soc.org/show_bug.cgi?id=421#c24
 220                 # XXX what is this for?  it is not possible to identify
 221                 # it because the "direct access to insn bits" provides
 222                 # absolutely no clue as to its purpose.
 223                 # also: this is likely to be wrong because of PowerISA
 224                 # field ordering (see V3.0B p4 section 1.3.4)
 225                 with m.If(field(op.insn, 20, 26) == 1):
 226                     comb += Assert(msr_o[MSR.HV] == 1)
 227                 with m.Else():
 228                     comb += Assert(msr_o[MSR.HV] == 0)
 229
 230             ###################
 231             # RFID.  v3.0B p955
 232             ###################
 233             with m.Case(MicrOp.OP_RFID):
 234                 comb += [
 235                     Assert(msr_o.ok),
 236                     Assert(nia_o.ok),
 237                     ]
 238
 239                 # Note: going through the spec pseudo-code, line-by-line,
 240                 # in order, with these assertions.  idea is: compare
 241                 # *directly* against the pseudo-code.  therefore, leave
 242                 # numbering in (from pseudo-code) and add *comments* about
 243                 # which field it is (3 == HV etc.)
 244
 245                 # spec: MSR[51] <- (MSR[3] & SRR1[51]) | ((¬MSR[3] & MSR[51]))
 246                 with m.If(msr_i[3]): # HV
 247                     comb += Assert(msr_o[51] == srr1_i[51]) # ME from SRR1
 248                 with m.Else():
 249                     comb += Assert(msr_o[51] == msr_i[51]) # ME from MSR (in)
 250
 251                 comb += [
 252                     # spec: MSR[3] <- (MSR[3] & SRR1[3])
 253                     Assert(msr_o[3] == (srr1_i[3] & msr_i[3])), # HV
 254                 ]
 255
 256                 # if (MSR[29:31] != 0b010) | (SRR1[29:31] != 0b000) then
 257                 #     MSR[29:31] <- SRR1[29:31]
 258                 with m.If((field(msr_i , 29, 31) != 0b010) |
 259                           (field(srr1_i, 29, 31) != 0b000)):
 260                     comb += Assert(field(msr_o.data, 29, 31) ==
 261                                    field(srr1_i, 29, 31))
 262                 with m.Else():
 263                     comb += Assert(field(msr_o.data, 29, 31) ==
 264                                    field(msr_i, 29, 31))
 265
 266                 # check EE (48) IR (58), DR (59): PR (49) will over-ride
 267                 comb += [
 268                     Assert(msr_o[48] == (srr1_i[48] | srr1_i[48])), # EE
 269                     Assert(msr_o[58] == (srr1_i[58] | srr1_i[58])), # IR
 270                     Assert(msr_o[59] == (srr1_i[59] | srr1_i[59])), # DR
 271                 ]
 272
 273                 # remaining bits: straight copy.  don't know what these are:
 274                 # just trust the v3.0B spec is correct.
 275                 comb += [
 276                     Assert(field(msr_o, 0, 2) == field(srr1_i, 0, 2)),
 277                     Assert(field(msr_o, 4, 28) == field(srr1_i, 4, 28)),
 278                     Assert(field(msr_o, 32) == field(srr1_i, 32),
 279                     Assert(field(msr_o, 37, 41) == field(srr1_i, 37, 41)),
 280                     Assert(field(msr_o, 49, 50) == field(srr1_i, 49, 50)),
 281                     Assert(field(msr_o, 52, 57) == field(srr1_i, 52, 57)),
 282                     Assert(field(msr_o, 60, 63) == field(srr1_i, 60, 63)),
 283                 ]
 284
 285                 # check NIA against SRR0.  2 LSBs are set to zero (word-align)
 286                 comb += Assert(nia_o.data == Cat(Const(0, 2), dut.i.srr0[2:]))
 287
 288         comb += dut.i.ctx.matches(dut.o.ctx)
 289
 290         return m
 291
 292
 293 class TrapMainStageTestCase(FHDLTestCase):
 294     def test_formal(self):
 295         self.assertFormal(Driver(), mode="bmc", depth=10)
 296         self.assertFormal(Driver(), mode="cover", depth=10)
 297
 298     def test_ilang(self):
 299         vl = rtlil.convert(Driver(), ports=[])
 300         with open("trap_main_stage.il", "w") as f:
 301             f.write(vl)
 302
 303
 304 if __name__ == '__main__':
 305     unittest.main()
 306