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 """
   8
   9
  10 import unittest
  11
  12 from nmigen import Cat, Const, Elaboratable, Module, Signal
  13 from nmigen.asserts import Assert, AnyConst
  14 from nmigen.cli import rtlil
  15
  16 from nmutil.formaltest import FHDLTestCase
  17
  18 from soc.consts import MSR
  19
  20 from soc.decoder.power_enums import MicrOp
  21
  22 from soc.fu.trap.main_stage import TrapMainStage
  23 from soc.fu.trap.pipe_data import TrapPipeSpec
  24 from soc.fu.trap.trap_input_record import CompTrapOpSubset
  25
  26
  27 def field(r, start, end):
  28     return r[63-end:63-start+1] # slices ends are +1, POWER spec is not
  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, dut.i.msr
  47         srr1_i = dut.i.srr1
  48
  49         comb += op.eq(rec)
  50
  51         # start of properties
  52         with m.Switch(op.insn_type):
  53             with m.Case(MicrOp.OP_SC):
  54                 comb += [
  55                     Assert(dut.o.srr0.ok),
  56                     Assert(dut.o.srr1.ok),
  57
  58                     Assert(dut.o.srr0.data == (dut.i.cia + 4)[0:64]),
  59                     Assert(field(dut.o.srr1, 33, 36) == 0),
  60                     Assert(field(dut.o.srr1, 42, 47) == 0),
  61                     Assert(field(dut.o.srr1, 0, 32) == field(msr_i, 0, 32)),
  62                     Assert(field(dut.o.srr1, 37, 41) == field(msr_i, 37, 41)),
  63                     Assert(field(dut.o.srr1, 48, 63) == field(msr_i, 48, 63)),
  64                 ]
  65             with m.Case(MicrOp.OP_RFID):
  66                 comb += [
  67                     Assert(msr_o.ok),
  68                     Assert(dut.o.nia.ok),
  69
  70                     Assert(msr_o[MSR.HV] == (srr1_i[MSR.HV] & msr_i[MSR.HV])),
  71                     Assert(msr_o[MSR.EE] == (srr1_i[MSR.EE] | srr1_i[MSR.PR])),
  72                     Assert(msr_o[MSR.IR] == (srr1_i[MSR.IR] | srr1_i[MSR.PR])),
  73                     Assert(msr_o[MSR.DR] == (srr1_i[MSR.DR] | srr1_i[MSR.PR])),
  74                     Assert(field(msr_o, 0, 2) == field(srr1_i, 0, 2)),
  75                     Assert(field(msr_o, 4, 28) == field(srr1_i, 4, 28)),
  76                     Assert(msr_o[63-32] == srr1_i[63-32]),
  77                     Assert(field(msr_o, 37, 41) == field(srr1_i, 37, 41)),
  78                     Assert(field(msr_o, 49, 50) == field(srr1_i, 49, 50)),
  79                     Assert(field(msr_o, 52, 57) == field(srr1_i, 52, 57)),
  80                     Assert(field(msr_o, 60, 63) == field(srr1_i, 60, 63)),
  81                     Assert(dut.o.nia.data == Cat(Const(0, 2), dut.i.srr0[2:])),
  82                 ]
  83                 with m.If(msr_i[MSR.HV]):
  84                     comb += Assert(msr_o[MSR.ME] == srr1_i[MSR.ME])
  85                 with m.Else():
  86                     comb += Assert(msr_o[MSR.ME] == msr_i[MSR.ME])
  87                 with m.If((field(msr_i , 29, 31) != 0b010) | # MSR
  88                           (field(srr1_i, 29, 31) != 0b000)): # SRR1
  89                     comb += Assert(field(msr_o.data, 29, 31) ==
  90                                    field(srr1_i, 29, 31))
  91                 with m.Else():
  92                     comb += Assert(field(msr_o.data, 29, 31) ==
  93                                    field(msr_i, 29, 31))
  94
  95         comb += dut.i.ctx.matches(dut.o.ctx)
  96
  97         return m
  98
  99
 100 class TrapMainStageTestCase(FHDLTestCase):
 101     def test_formal(self):
 102         self.assertFormal(Driver(), mode="bmc", depth=10)
 103         self.assertFormal(Driver(), mode="cover", depth=10)
 104
 105     def test_ilang(self):
 106         vl = rtlil.convert(Driver(), ports=[])
 107         with open("trap_main_stage.il", "w") as f:
 108             f.write(vl)
 109
 110
 111 if __name__ == '__main__':
 112     unittest.main()
 113