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             ###################
 175             # RFID.  v3.0B p955
 176             ###################
 177             with m.Case(MicrOp.OP_RFID):
 178                 comb += [
 179                     Assert(msr_o.ok),
 180                     Assert(nia_o.ok),
 181                 ]
 182
 183                 # Note: going through the spec pseudo-code, line-by-line,
 184                 # in order, with these assertions.  idea is: compare
 185                 # *directly* against the pseudo-code.  therefore, leave
 186                 # numbering in (from pseudo-code) and add *comments* about
 187                 # which field it is (3 == HV etc.)
 188
 189                 # spec: MSR[51] <- (MSR[3] & SRR1[51]) | ((¬MSR[3] & MSR[51]))
 190                 with m.If(field(msr_i, 3)): # HV
 191                     comb += Assert(field(msr_o, 51) == field(srr1_i, 51)) # ME
 192                 with m.Else():
 193                     comb += Assert(field(msr_o, 51) == field(msr_i, 51)) # ME
 194
 195                 # if (MSR[29:31] != 0b010) | (SRR1[29:31] != 0b000) then
 196                 #     MSR[29:31] <- SRR1[29:31]
 197                 with m.If((field(msr_i , 29, 31) != 0b010) |
 198                           (field(srr1_i, 29, 31) != 0b000)):
 199                     comb += Assert(field(msr_o.data, 29, 31) ==
 200                                    field(srr1_i, 29, 31))
 201                 with m.Else():
 202                     comb += Assert(field(msr_o.data, 29, 31) ==
 203                                    field(msr_i, 29, 31))
 204
 205                 # check EE (48) IR (58), DR (59): PR (49) will over-ride
 206                 comb += [
 207                     Assert(
 208                         field(msr_o, 48) ==
 209                         field(srr1_i, 48) | field(srr1_i, 49)
 210                     ),
 211                     Assert(
 212                         field(msr_o, 58) ==
 213                         field(srr1_i, 58) | field(srr1_i, 49)
 214                     ),
 215                     Assert(
 216                         field(msr_o, 59) ==
 217                         field(srr1_i, 59) | field(srr1_i, 49)
 218                     ),
 219                 ]
 220
 221                 # remaining bits: straight copy.  don't know what these are:
 222                 # just trust the v3.0B spec is correct.
 223                 comb += [
 224                     Assert(field(msr_o, 0, 2) == field(srr1_i, 0, 2)),
 225                     Assert(field(msr_o, 4, 28) == field(srr1_i, 4, 28)),
 226                     Assert(field(msr_o, 32) == field(srr1_i, 32)),
 227                     Assert(field(msr_o, 37, 41) == field(srr1_i, 37, 41)),
 228                     Assert(field(msr_o, 49, 50) == field(srr1_i, 49, 50)),
 229                     Assert(field(msr_o, 52, 57) == field(srr1_i, 52, 57)),
 230                     Assert(field(msr_o, 60, 63) == field(srr1_i, 60, 63)),
 231                 ]
 232
 233                 # check NIA against SRR0.  2 LSBs are set to zero (word-align)
 234                 comb += Assert(nia_o.data == Cat(Const(0, 2), dut.i.srr0[2:]))
 235
 236             #################
 237             # SC.  v3.0B p952
 238             #################
 239             with m.Case(MicrOp.OP_SC):
 240                 expected_msr = Signal(len(msr_o.data))
 241                 comb += expected_msr.eq(op.msr)
 242                 # Unless otherwise documented, these exceptions to the MSR bits
 243                 # are documented in Power ISA V3.0B, page 1063 or 1064.
 244                 # We are not supporting hypervisor or transactional semantics,
 245                 # so we skip enforcing those fields' properties.
 246                 comb += field(expected_msr, MSRb.IR).eq(0)
 247                 comb += field(expected_msr, MSRb.DR).eq(0)
 248                 comb += field(expected_msr, MSRb.FE0).eq(0)
 249                 comb += field(expected_msr, MSRb.FE1).eq(0)
 250                 comb += field(expected_msr, MSRb.EE).eq(0)
 251                 comb += field(expected_msr, MSRb.RI).eq(0)
 252                 comb += field(expected_msr, MSRb.SF).eq(1)
 253                 comb += field(expected_msr, MSRb.TM).eq(0)
 254                 comb += field(expected_msr, MSRb.VEC).eq(0)
 255                 comb += field(expected_msr, MSRb.VSX).eq(0)
 256                 comb += field(expected_msr, MSRb.PR).eq(0)
 257                 comb += field(expected_msr, MSRb.FP).eq(0)
 258                 comb += field(expected_msr, MSRb.PMM).eq(0)
 259                 comb += field(expected_msr, MSRb.TEs, MSRb.TEe).eq(0)
 260                 comb += field(expected_msr, MSRb.UND).eq(0)
 261                 comb += field(expected_msr, MSRb.LE).eq(1)
 262
 263                 comb += [
 264                     Assert(dut.o.srr0.ok),
 265                     Assert(srr1_o.ok),
 266                     Assert(msr_o.ok),
 267
 268                     Assert(dut.o.srr0.data == (op.cia + 4)[0:64]),
 269                     Assert(field(srr1_o, 33, 36) == 0),
 270                     Assert(field(srr1_o, 42, 47) == 0),
 271                     Assert(field(srr1_o, 0, 32) == field(msr_i, 0, 32)),
 272                     Assert(field(srr1_o, 37, 41) == field(msr_i, 37, 41)),
 273                     Assert(field(srr1_o, 48, 63) == field(msr_i, 48, 63)),
 274
 275                     Assert(msr_o.data == expected_msr),
 276                 ]
 277
 278         comb += dut.i.ctx.matches(dut.o.ctx)
 279
 280         return m
 281
 282
 283 class TrapMainStageTestCase(FHDLTestCase):
 284     def test_formal(self):
 285         self.assertFormal(Driver(), mode="bmc", depth=10)
 286         self.assertFormal(Driver(), mode="cover", depth=10)
 287
 288     def test_ilang(self):
 289         vl = rtlil.convert(Driver(), ports=[])
 290         with open("trap_main_stage.il", "w") as f:
 291             f.write(vl)
 292
 293
 294 if __name__ == '__main__':
 295     unittest.main()
 296