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]
  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) |
  88                           (field(msr_i, 29, 31) != 0b000)):
  89                     comb += Assert(field(msr_o.data, 29, 31) == field(srr1_i, 29, 31))
  90
  91         comb += dut.i.ctx.matches(dut.o.ctx)
  92
  93         return m
  94
  95
  96 class TrapMainStageTestCase(FHDLTestCase):
  97     def test_formal(self):
  98         self.assertFormal(Driver(), mode="bmc", depth=10)
  99         self.assertFormal(Driver(), mode="cover", depth=10)
 100
 101     def test_ilang(self):
 102         vl = rtlil.convert(Driver(), ports=[])
 103         with open("trap_main_stage.il", "w") as f:
 104             f.write(vl)
 105
 106
 107 if __name__ == '__main__':
 108     unittest.main()
 109