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                     comb += field(expected_msr, MSRb.TEs, MSRb.TEe).eq(0)
 124                     comb += field(expected_msr, MSRb.UND).eq(0)
 125                     comb += field(expected_msr, MSRb.LE).eq(1)
 126
 127                     expected_srr1 = Signal(len(srr1_o.data))
 128                     comb += expected_srr1.eq(op.msr)
 129
 130                     comb += expected_srr1[63-36:63-32].eq(0)
 131                     comb += expected_srr1[PI.TRAP].eq(traptype == 0)
 132                     comb += expected_srr1[PI.PRIV].eq(traptype[1])
 133                     comb += expected_srr1[PI.FP].eq(traptype[0])
 134                     comb += expected_srr1[PI.ADR].eq(traptype[3])
 135                     comb += expected_srr1[PI.ILLEG].eq(traptype[4])
 136                     comb += expected_srr1[PI.TM_BAD_THING].eq(0)
 137
 138                     comb += [
 139                         Assert(msr_o.ok),
 140                         Assert(msr_o.data == expected_msr),
 141                         Assert(srr0_o.ok),
 142                         Assert(srr0_o.data == op.cia),
 143                         Assert(srr1_o.ok),
 144                         Assert(srr1_o.data == expected_srr1),
 145                         Assert(nia_o.ok),
 146                         Assert(nia_o.data == op.trapaddr << 4),
 147                     ]
 148
 149             #################
 150             # SC.  v3.0B p952
 151             #################
 152             with m.Case(MicrOp.OP_SC):
 153                 expected_msr = Signal(len(msr_o.data))
 154                 comb += expected_msr.eq(op.msr)
 155                 # Unless otherwise documented, these exceptions to the MSR bits
 156                 # are documented in Power ISA V3.0B, page 1063 or 1064.
 157                 # We are not supporting hypervisor or transactional semantics,
 158                 # so we skip enforcing those fields' properties.
 159                 comb += field(expected_msr, MSRb.IR).eq(0)
 160                 comb += field(expected_msr, MSRb.DR).eq(0)
 161                 comb += field(expected_msr, MSRb.FE0).eq(0)
 162                 comb += field(expected_msr, MSRb.FE1).eq(0)
 163                 comb += field(expected_msr, MSRb.EE).eq(0)
 164                 comb += field(expected_msr, MSRb.RI).eq(0)
 165                 comb += field(expected_msr, MSRb.SF).eq(1)
 166                 comb += field(expected_msr, MSRb.TM).eq(0)
 167                 comb += field(expected_msr, MSRb.VEC).eq(0)
 168                 comb += field(expected_msr, MSRb.VSX).eq(0)
 169                 comb += field(expected_msr, MSRb.PR).eq(0)
 170                 comb += field(expected_msr, MSRb.FP).eq(0)
 171                 comb += field(expected_msr, MSRb.PMM).eq(0)
 172                 comb += field(expected_msr, MSRb.TEs, MSRb.TEe).eq(0)
 173                 comb += field(expected_msr, MSRb.UND).eq(0)
 174                 comb += field(expected_msr, MSRb.LE).eq(1)
 175
 176                 comb += [
 177                     Assert(dut.o.srr0.ok),
 178                     Assert(srr1_o.ok),
 179                     Assert(msr_o.ok),
 180
 181                     Assert(dut.o.srr0.data == (op.cia + 4)[0:64]),
 182                     Assert(field(srr1_o, 33, 36) == 0),
 183                     Assert(field(srr1_o, 42, 47) == 0),
 184                     Assert(field(srr1_o, 0, 32) == field(msr_i, 0, 32)),
 185                     Assert(field(srr1_o, 37, 41) == field(msr_i, 37, 41)),
 186                     Assert(field(srr1_o, 48, 63) == field(msr_i, 48, 63)),
 187
 188                     Assert(msr_o.data == expected_msr),
 189                 ]
 190
 191             ###################
 192             # RFID.  v3.0B p955
 193             ###################
 194             with m.Case(MicrOp.OP_RFID):
 195                 comb += [
 196                     Assert(msr_o.ok),
 197                     Assert(nia_o.ok),
 198                 ]
 199
 200                 # if (MSR[29:31] != 0b010) | (SRR1[29:31] != 0b000) then
 201                 #     MSR[29:31] <- SRR1[29:31]
 202                 with m.If((field(msr_i , 29, 31) != 0b010) |
 203                           (field(srr1_i, 29, 31) != 0b000)):
 204                     comb += Assert(field(msr_o.data, 29, 31) ==
 205                                    field(srr1_i, 29, 31))
 206                 with m.Else():
 207                     comb += Assert(field(msr_o.data, 29, 31) ==
 208                                    field(msr_i, 29, 31))
 209
 210                 # check EE (48) IR (58), DR (59): PR (49) will over-ride
 211                 for bit in [48, 58, 59]:
 212                     comb += Assert(
 213                         field(msr_o, bit) ==
 214                         (field(srr1_i, bit) | field(srr1_i, 49))
 215                     )
 216
 217                 # remaining bits: straight copy.  don't know what these are:
 218                 # just trust the v3.0B spec is correct.
 219                 comb += [
 220                     Assert(field(msr_o, 0, 2) == field(srr1_i, 0, 2)),
 221                     Assert(field(msr_o, 4, 28) == field(srr1_i, 4, 28)),
 222                     Assert(field(msr_o, 32) == field(srr1_i, 32)),
 223                     Assert(field(msr_o, 37, 41) == field(srr1_i, 37, 41)),
 224                     Assert(field(msr_o, 49, 50) == field(srr1_i, 49, 50)),
 225                     Assert(field(msr_o, 52, 57) == field(srr1_i, 52, 57)),
 226                     Assert(field(msr_o, 60, 63) == field(srr1_i, 60, 63)),
 227                 ]
 228
 229                 # check NIA against SRR0.  2 LSBs are set to zero (word-align)
 230                 comb += Assert(nia_o.data == Cat(Const(0, 2), dut.i.srr0[2:]))
 231
 232         comb += dut.i.ctx.matches(dut.o.ctx)
 233
 234         return m
 235
 236
 237 class TrapMainStageTestCase(FHDLTestCase):
 238     def test_formal(self):
 239         self.assertFormal(Driver(), mode="bmc", depth=10)
 240         self.assertFormal(Driver(), mode="cover", depth=10)
 241
 242     def test_ilang(self):
 243         vl = rtlil.convert(Driver(), ports=[])
 244         with open("trap_main_stage.il", "w") as f:
 245             f.write(vl)
 246
 247
 248 if __name__ == '__main__':
 249     unittest.main()
 250