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
  51         comb += op.eq(rec)
  52
  53         d_fields = dut.fields.FormD
  54         sc_fields = dut.fields.FormSC
  55
  56         # start of properties
  57         with m.Switch(op.insn_type):
  58
  59             ###############
  60             # TDI/TWI/TD/TW.  v3.0B p90-91
  61             ###############
  62             with m.Case(MicrOp.OP_TRAP):
  63                 to = Signal(len(d_fields.TO))
  64                 comb += to.eq(d_fields.TO[0:-1])
  65
  66                 a_i = Signal(64)
  67                 b_i = Signal(64)
  68                 comb += a_i.eq(dut.i.a)
  69                 comb += b_i.eq(dut.i.b)
  70
  71                 a_s = Signal(signed(64), reset_less=True)
  72                 b_s = Signal(signed(64), reset_less=True)
  73                 a = Signal(64, reset_less=True)
  74                 b = Signal(64, reset_less=True)
  75
  76                 with m.If(op.is_32bit):
  77                     comb += a_s.eq(exts(a_i, 32, 64))
  78                     comb += b_s.eq(exts(b_i, 32, 64))
  79                     comb += a.eq(a_i[0:32])
  80                     comb += b.eq(b_i[0:32])
  81                 with m.Else():
  82                     comb += a_s.eq(a_i)
  83                     comb += b_s.eq(b_i)
  84                     comb += a.eq(a_i)
  85                     comb += b.eq(b_i)
  86
  87                 lt_s = Signal(reset_less=True)
  88                 gt_s = Signal(reset_less=True)
  89                 lt_u = Signal(reset_less=True)
  90                 gt_u = Signal(reset_less=True)
  91                 equal = Signal(reset_less=True)
  92
  93                 comb += lt_s.eq(a_s < b_s)
  94                 comb += gt_s.eq(a_s > b_s)
  95                 comb += lt_u.eq(a < b)
  96                 comb += gt_u.eq(a > b)
  97                 comb += equal.eq(a == b)
  98
  99                 trapbits = Signal(5, reset_less=True)
 100                 comb += trapbits.eq(Cat(gt_u, lt_u, equal, gt_s, lt_s))
 101
 102                 take_trap = Signal()
 103                 traptype = op.traptype
 104                 comb += take_trap.eq(traptype.any() | (trapbits & to).any())
 105
 106                 with m.If(take_trap):
 107                     expected_msr = Signal(len(msr_o.data))
 108                     comb += expected_msr.eq(op.msr)
 109
 110                     comb += field(expected_msr, MSRb.IR).eq(0)
 111                     comb += field(expected_msr, MSRb.DR).eq(0)
 112                     comb += field(expected_msr, MSRb.FE0).eq(0)
 113                     comb += field(expected_msr, MSRb.FE1).eq(0)
 114                     comb += field(expected_msr, MSRb.EE).eq(0)
 115                     comb += field(expected_msr, MSRb.RI).eq(0)
 116                     comb += field(expected_msr, MSRb.SF).eq(1)
 117                     comb += field(expected_msr, MSRb.TM).eq(0)
 118                     comb += field(expected_msr, MSRb.VEC).eq(0)
 119                     comb += field(expected_msr, MSRb.VSX).eq(0)
 120                     comb += field(expected_msr, MSRb.PR).eq(0)
 121                     comb += field(expected_msr, MSRb.FP).eq(0)
 122                     comb += field(expected_msr, MSRb.PMM).eq(0)
 123
 124                     # still wrong.
 125                     # see https://bugs.libre-soc.org/show_bug.cgi?id=325#c120
 126                     #
 127                     # saf2: no it's not.  Proof by substitution:
 128                     #
 129                     # field(R,MSRb.TEs,MSRb.TEe).eq(0)
 130                     # == field(R,53,54).eq(0)
 131                     # == R[field_slice(53,54)].eq(0)
 132                     # == R[slice(63-54, (63-53)+1)].eq(0)
 133                     # == R[slice(9, 11)].eq(0)
 134                     # == R[9:11].eq(0)
 135                     #
 136                     # Also put proof in py-doc for field().
 137
 138                     comb += field(expected_msr, MSRb.TEs, MSRb.TEe).eq(0)
 139
 140                     comb += field(expected_msr, MSRb.UND).eq(0)
 141                     comb += field(expected_msr, MSRb.LE).eq(1)
 142
 143                     expected_srr1 = Signal(len(srr1_o.data))
 144                     comb += expected_srr1.eq(op.msr)
 145
 146                     # Per V3.0B, page 1075
 147                     comb += field(expected_srr1, 33, 36).eq(0)
 148                     comb += field(expected_srr1, 42).eq(0)  # TM_BAD_THING
 149                     comb += field(expected_srr1, 43).eq(traptype[0])    # FP
 150                     comb += field(expected_srr1, 44).eq(traptype[4])    # ILLEG
 151                     comb += field(expected_srr1, 45).eq(traptype[1])    # PRIV
 152                     comb += field(expected_srr1, 46).eq(traptype == 0)  # TRAP
 153                     comb += field(expected_srr1, 47).eq(traptype[3])    # ADDR
 154
 155                     comb += [
 156                         Assert(msr_o.ok),
 157                         Assert(msr_o.data == expected_msr),
 158                         Assert(srr0_o.ok),
 159                         Assert(srr0_o.data == op.cia),
 160                         Assert(srr1_o.ok),
 161                         Assert(srr1_o.data == expected_srr1),
 162                         Assert(nia_o.ok),
 163                         Assert(nia_o.data == op.trapaddr << 4),
 164                     ]
 165
 166             ###################
 167             # MTMSR
 168             ###################
 169
 170             ###################
 171             # MFMSR
 172             ###################
 173
 174             with m.Case(MicrOp.OP_MFMSR):
 175                 comb += [
 176                     Assert(dut.o.o.ok),
 177                     Assert(dut.o.o.data == msr_i),
 178                 ]
 179
 180             ###################
 181             # RFID.  v3.0B p955
 182             ###################
 183             with m.Case(MicrOp.OP_RFID):
 184                 comb += [
 185                     Assert(msr_o.ok),
 186                     Assert(nia_o.ok),
 187                 ]
 188
 189                 # Note: going through the spec pseudo-code, line-by-line,
 190                 # in order, with these assertions.  idea is: compare
 191                 # *directly* against the pseudo-code.  therefore, leave
 192                 # numbering in (from pseudo-code) and add *comments* about
 193                 # which field it is (3 == HV etc.)
 194
 195                 # spec: MSR[51] <- (MSR[3] & SRR1[51]) | ((¬MSR[3] & MSR[51]))
 196                 with m.If(field(msr_i, 3)): # HV
 197                     comb += Assert(field(msr_o, 51) == field(srr1_i, 51)) # ME
 198                 with m.Else():
 199                     comb += Assert(field(msr_o, 51) == field(msr_i, 51)) # ME
 200
 201                 # if (MSR[29:31] != 0b010) | (SRR1[29:31] != 0b000) then
 202                 #     MSR[29:31] <- SRR1[29:31]
 203                 with m.If((field(msr_i , 29, 31) != 0b010) |
 204                           (field(srr1_i, 29, 31) != 0b000)):
 205                     comb += Assert(field(msr_o.data, 29, 31) ==
 206                                    field(srr1_i, 29, 31))
 207                 with m.Else():
 208                     comb += Assert(field(msr_o.data, 29, 31) ==
 209                                    field(msr_i, 29, 31))
 210
 211                 # check EE (48) IR (58), DR (59): PR (49) will over-ride
 212                 PR = field(srr1_i, 49) # alias/copy of SRR1 PR field
 213                 comb += [
 214                     Assert(field(msr_o, 48) == field(srr1_i, 48) | PR), # EE
 215                     Assert(field(msr_o, 58) == field(srr1_i, 58) | PR), # IR
 216                     Assert(field(msr_o, 59) == field(srr1_i, 59) | PR), # DR
 217                 ]
 218
 219                 # remaining bits: straight copy.  don't know what these are:
 220                 # just trust the v3.0B spec is correct.
 221                 comb += [
 222                     Assert(field(msr_o, 0, 2) == field(srr1_i, 0, 2)),
 223                     Assert(field(msr_o, 4, 28) == field(srr1_i, 4, 28)),
 224                     Assert(field(msr_o, 32) == field(srr1_i, 32)),
 225                     Assert(field(msr_o, 37, 41) == field(srr1_i, 37, 41)),
 226                     Assert(field(msr_o, 49, 50) == field(srr1_i, 49, 50)),
 227                     Assert(field(msr_o, 52, 57) == field(srr1_i, 52, 57)),
 228                     Assert(field(msr_o, 60, 63) == field(srr1_i, 60, 63)),
 229                 ]
 230
 231                 # check NIA against SRR0.  2 LSBs are set to zero (word-align)
 232                 comb += Assert(nia_o.data == Cat(Const(0, 2), dut.i.srr0[2:]))
 233
 234             #################
 235             # SC.  v3.0B p952
 236             #################
 237             with m.Case(MicrOp.OP_SC):
 238                 expected_msr = Signal(len(msr_o.data))
 239                 comb += expected_msr.eq(op.msr)
 240                 # Unless otherwise documented, these exceptions to the MSR bits
 241                 # are documented in Power ISA V3.0B, page 1063 or 1064.
 242                 # We are not supporting hypervisor or transactional semantics,
 243                 # so we skip enforcing those fields' properties.
 244                 comb += field(expected_msr, MSRb.IR).eq(0)
 245                 comb += field(expected_msr, MSRb.DR).eq(0)
 246                 comb += field(expected_msr, MSRb.FE0).eq(0)
 247                 comb += field(expected_msr, MSRb.FE1).eq(0)
 248                 comb += field(expected_msr, MSRb.EE).eq(0)
 249                 comb += field(expected_msr, MSRb.RI).eq(0)
 250                 comb += field(expected_msr, MSRb.SF).eq(1)
 251                 comb += field(expected_msr, MSRb.TM).eq(0)
 252                 comb += field(expected_msr, MSRb.VEC).eq(0)
 253                 comb += field(expected_msr, MSRb.VSX).eq(0)
 254                 comb += field(expected_msr, MSRb.PR).eq(0)
 255                 comb += field(expected_msr, MSRb.FP).eq(0)
 256                 comb += field(expected_msr, MSRb.PMM).eq(0)
 257                 comb += field(expected_msr, MSRb.TEs, MSRb.TEe).eq(0)
 258                 comb += field(expected_msr, MSRb.UND).eq(0)
 259                 comb += field(expected_msr, MSRb.LE).eq(1)
 260
 261                 comb += [
 262                     Assert(dut.o.srr0.ok),
 263                     Assert(srr1_o.ok),
 264                     Assert(msr_o.ok),
 265
 266                     Assert(dut.o.srr0.data == (op.cia + 4)[0:64]),
 267                     Assert(field(srr1_o, 33, 36) == 0),
 268                     Assert(field(srr1_o, 42, 47) == 0),
 269                     Assert(field(srr1_o, 0, 32) == field(msr_i, 0, 32)),
 270                     Assert(field(srr1_o, 37, 41) == field(msr_i, 37, 41)),
 271                     Assert(field(srr1_o, 48, 63) == field(msr_i, 48, 63)),
 272
 273                     Assert(msr_o.data == expected_msr),
 274                 ]
 275
 276         comb += dut.i.ctx.matches(dut.o.ctx)
 277
 278         return m
 279
 280
 281 class TrapMainStageTestCase(FHDLTestCase):
 282     def test_formal(self):
 283         self.assertFormal(Driver(), mode="bmc", depth=10)
 284         self.assertFormal(Driver(), mode="cover", depth=10)
 285
 286     def test_ilang(self):
 287         vl = rtlil.convert(Driver(), ports=[])
 288         with open("trap_main_stage.il", "w") as f:
 289             f.write(vl)
 290
 291
 292 if __name__ == '__main__':
 293     unittest.main()
 294