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                 comb += [
 213                     Assert(
 214                         field(msr_o, 48) ==
 215                         field(srr1_i, 48) | field(srr1_i, 49)
 216                     ),
 217                     Assert(
 218                         field(msr_o, 58) ==
 219                         field(srr1_i, 58) | field(srr1_i, 49)
 220                     ),
 221                     Assert(
 222                         field(msr_o, 59) ==
 223                         field(srr1_i, 59) | field(srr1_i, 49)
 224                     ),
 225                 ]
 226
 227                 # remaining bits: straight copy.  don't know what these are:
 228                 # just trust the v3.0B spec is correct.
 229                 comb += [
 230                     Assert(field(msr_o, 0, 2) == field(srr1_i, 0, 2)),
 231                     Assert(field(msr_o, 4, 28) == field(srr1_i, 4, 28)),
 232                     Assert(field(msr_o, 32) == field(srr1_i, 32)),
 233                     Assert(field(msr_o, 37, 41) == field(srr1_i, 37, 41)),
 234                     Assert(field(msr_o, 49, 50) == field(srr1_i, 49, 50)),
 235                     Assert(field(msr_o, 52, 57) == field(srr1_i, 52, 57)),
 236                     Assert(field(msr_o, 60, 63) == field(srr1_i, 60, 63)),
 237                 ]
 238
 239                 # check NIA against SRR0.  2 LSBs are set to zero (word-align)
 240                 comb += Assert(nia_o.data == Cat(Const(0, 2), dut.i.srr0[2:]))
 241
 242             #################
 243             # SC.  v3.0B p952
 244             #################
 245             with m.Case(MicrOp.OP_SC):
 246                 expected_msr = Signal(len(msr_o.data))
 247                 comb += expected_msr.eq(op.msr)
 248                 # Unless otherwise documented, these exceptions to the MSR bits
 249                 # are documented in Power ISA V3.0B, page 1063 or 1064.
 250                 # We are not supporting hypervisor or transactional semantics,
 251                 # so we skip enforcing those fields' properties.
 252                 comb += field(expected_msr, MSRb.IR).eq(0)
 253                 comb += field(expected_msr, MSRb.DR).eq(0)
 254                 comb += field(expected_msr, MSRb.FE0).eq(0)
 255                 comb += field(expected_msr, MSRb.FE1).eq(0)
 256                 comb += field(expected_msr, MSRb.EE).eq(0)
 257                 comb += field(expected_msr, MSRb.RI).eq(0)
 258                 comb += field(expected_msr, MSRb.SF).eq(1)
 259                 comb += field(expected_msr, MSRb.TM).eq(0)
 260                 comb += field(expected_msr, MSRb.VEC).eq(0)
 261                 comb += field(expected_msr, MSRb.VSX).eq(0)
 262                 comb += field(expected_msr, MSRb.PR).eq(0)
 263                 comb += field(expected_msr, MSRb.FP).eq(0)
 264                 comb += field(expected_msr, MSRb.PMM).eq(0)
 265                 comb += field(expected_msr, MSRb.TEs, MSRb.TEe).eq(0)
 266                 comb += field(expected_msr, MSRb.UND).eq(0)
 267                 comb += field(expected_msr, MSRb.LE).eq(1)
 268
 269                 comb += [
 270                     Assert(dut.o.srr0.ok),
 271                     Assert(srr1_o.ok),
 272                     Assert(msr_o.ok),
 273
 274                     Assert(dut.o.srr0.data == (op.cia + 4)[0:64]),
 275                     Assert(field(srr1_o, 33, 36) == 0),
 276                     Assert(field(srr1_o, 42, 47) == 0),
 277                     Assert(field(srr1_o, 0, 32) == field(msr_i, 0, 32)),
 278                     Assert(field(srr1_o, 37, 41) == field(msr_i, 37, 41)),
 279                     Assert(field(srr1_o, 48, 63) == field(msr_i, 48, 63)),
 280
 281                     Assert(msr_o.data == expected_msr),
 282                 ]
 283
 284         comb += dut.i.ctx.matches(dut.o.ctx)
 285
 286         return m
 287
 288
 289 class TrapMainStageTestCase(FHDLTestCase):
 290     def test_formal(self):
 291         self.assertFormal(Driver(), mode="bmc", depth=10)
 292         self.assertFormal(Driver(), mode="cover", depth=10)
 293
 294     def test_ilang(self):
 295         vl = rtlil.convert(Driver(), ports=[])
 296         with open("trap_main_stage.il", "w") as f:
 297             f.write(vl)
 298
 299
 300 if __name__ == '__main__':
 301     unittest.main()
 302