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                     comb += field(expected_msr, MSRb.TEs, MSRb.TEe).eq(0)
 127
 128                     comb += field(expected_msr, MSRb.UND).eq(0)
 129                     comb += field(expected_msr, MSRb.LE).eq(1)
 130
 131                     expected_srr1 = Signal(len(srr1_o.data))
 132                     comb += expected_srr1.eq(op.msr)
 133
 134                     # note here: 36 is ***LESS*** than 32  ***BUT***
 135                     # ***63-36*** is less than 63-32
 136                     # could do with using field_slice here however
 137                     # *get the number order right*.
 138
 139                     # however before doing that: why are these bits
 140                     # initialised to zero then every single one of them
 141                     # is over-ridden?  5 bits, 32-36 (36-32, haha)
 142                     # are set to zero, then 5 bits are set to expressions.
 143
 144                     # redundant comb += expected_srr1[63-36:63-32].eq(0)
 145
 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                 # We are not supporting hypervisor or transactional semantics,
 173                 # so we skip enforcing those fields' properties.
 174                 comb += field(expected_msr, MSRb.IR).eq(0)
 175                 comb += field(expected_msr, MSRb.DR).eq(0)
 176                 comb += field(expected_msr, MSRb.FE0).eq(0)
 177                 comb += field(expected_msr, MSRb.FE1).eq(0)
 178                 comb += field(expected_msr, MSRb.EE).eq(0)
 179                 comb += field(expected_msr, MSRb.RI).eq(0)
 180                 comb += field(expected_msr, MSRb.SF).eq(1)
 181                 comb += field(expected_msr, MSRb.TM).eq(0)
 182                 comb += field(expected_msr, MSRb.VEC).eq(0)
 183                 comb += field(expected_msr, MSRb.VSX).eq(0)
 184                 comb += field(expected_msr, MSRb.PR).eq(0)
 185                 comb += field(expected_msr, MSRb.FP).eq(0)
 186                 comb += field(expected_msr, MSRb.PMM).eq(0)
 187                 # XXX no.  slice quantity still inverted producing an empty list
 188                 # https://bugs.libre-soc.org/show_bug.cgi?id=325#c120
 189                 # also add a comment explaining this very non-obvious
 190                 # behaviour
 191                 comb += field(expected_msr, MSRb.TEs, MSRb.TEe).eq(0)
 192                 comb += field(expected_msr, MSRb.UND).eq(0)
 193                 comb += field(expected_msr, MSRb.LE).eq(1)
 194
 195                 comb += [
 196                     Assert(dut.o.srr0.ok),
 197                     Assert(srr1_o.ok),
 198                     Assert(msr_o.ok),
 199
 200                     Assert(dut.o.srr0.data == (op.cia + 4)[0:64]),
 201                     Assert(field(srr1_o, 33, 36) == 0),
 202                     Assert(field(srr1_o, 42, 47) == 0),
 203                     Assert(field(srr1_o, 0, 32) == field(msr_i, 0, 32)),
 204                     Assert(field(srr1_o, 37, 41) == field(msr_i, 37, 41)),
 205                     Assert(field(srr1_o, 48, 63) == field(msr_i, 48, 63)),
 206
 207                     Assert(msr_o.data == expected_msr),
 208                 ]
 209
 210             ###################
 211             # RFID.  v3.0B p955
 212             ###################
 213             with m.Case(MicrOp.OP_RFID):
 214                 comb += [
 215                     Assert(msr_o.ok),
 216                     Assert(nia_o.ok),
 217                 ]
 218
 219                 # XXX code comment has been removed, which explains
 220                 # why the code is written the way it is written
 221                 # see https://bugs.libre-soc.org/show_bug.cgi?id=325#c127
 222
 223                 # XXX restore HV check
 224                 # https://bugs.libre-soc.org/show_bug.cgi?id=325#c125
 225
 226                 # if (MSR[29:31] != 0b010) | (SRR1[29:31] != 0b000) then
 227                 #     MSR[29:31] <- SRR1[29:31]
 228                 with m.If((field(msr_i , 29, 31) != 0b010) |
 229                           (field(srr1_i, 29, 31) != 0b000)):
 230                     comb += Assert(field(msr_o.data, 29, 31) ==
 231                                    field(srr1_i, 29, 31))
 232                 with m.Else():
 233                     comb += Assert(field(msr_o.data, 29, 31) ==
 234                                    field(msr_i, 29, 31))
 235
 236                 # check EE (48) IR (58), DR (59): PR (49) will over-ride
 237
 238                 # XXX does not look as clear.  revert
 239                 # see https://bugs.libre-soc.org/show_bug.cgi?id=325#c122
 240                 for bit in [48, 58, 59]:
 241                     comb += Assert(
 242                         field(msr_o, bit) ==
 243                         (field(srr1_i, bit) | field(srr1_i, 49))
 244                     )
 245
 246                 # remaining bits: straight copy.  don't know what these are:
 247                 # just trust the v3.0B spec is correct.
 248                 comb += [
 249                     Assert(field(msr_o, 0, 2) == field(srr1_i, 0, 2)),
 250                     Assert(field(msr_o, 4, 28) == field(srr1_i, 4, 28)),
 251                     Assert(field(msr_o, 32) == field(srr1_i, 32)),
 252                     Assert(field(msr_o, 37, 41) == field(srr1_i, 37, 41)),
 253                     Assert(field(msr_o, 49, 50) == field(srr1_i, 49, 50)),
 254                     Assert(field(msr_o, 52, 57) == field(srr1_i, 52, 57)),
 255                     Assert(field(msr_o, 60, 63) == field(srr1_i, 60, 63)),
 256                 ]
 257
 258                 # check NIA against SRR0.  2 LSBs are set to zero (word-align)
 259                 comb += Assert(nia_o.data == Cat(Const(0, 2), dut.i.srr0[2:]))
 260
 261         comb += dut.i.ctx.matches(dut.o.ctx)
 262
 263         return m
 264
 265
 266 class TrapMainStageTestCase(FHDLTestCase):
 267     def test_formal(self):
 268         self.assertFormal(Driver(), mode="bmc", depth=10)
 269         self.assertFormal(Driver(), mode="cover", depth=10)
 270
 271     def test_ilang(self):
 272         vl = rtlil.convert(Driver(), ports=[])
 273         with open("trap_main_stage.il", "w") as f:
 274             f.write(vl)
 275
 276
 277 if __name__ == '__main__':
 278     unittest.main()
 279