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