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 ibm(n):
  28     return 63-n
  29
  30
  31 def is_ok(sig, value):
  32     """
  33     Answers with a list of assertions that checks for valid data on
  34     a pipeline stage output.  sig.data must have the anticipated value,
  35     and sig.ok must be asserted.  The `value` is constrained to the width
  36     of the sig.data field it's verified against, so it's safe to add, etc.
  37     offsets to Nmigen signals without having to worry about inequalities from
  38     differing signal widths.
  39     """
  40     return [
  41         Assert(sig.data == value[0:len(sig.data)]),
  42         Assert(sig.ok),
  43     ]
  44
  45
  46 def full_function_bits(msr):
  47     """
  48     Answers with a numeric constant signal with all "full functional"
  49     bits filled in, but all partial functional bits zeroed out.
  50
  51     See src/soc/fu/trap/main_stage.py:msr_copy commentary for details.
  52     """
  53     zeros16_21 = Const(0, (22 - 16))
  54     zeros27_30 = Const(0, (31 - 27))
  55     return Cat(msr[0:16], zeros16_21, msr[22:27], zeros27_30, msr[31:64])
  56
  57
  58 class Driver(Elaboratable):
  59     """
  60     """
  61
  62     def elaborate(self, platform):
  63         m = Module()
  64         comb = m.d.comb
  65
  66         rec = CompTrapOpSubset()
  67         pspec = TrapPipeSpec(id_wid=2)
  68
  69         m.submodules.dut = dut = TrapMainStage(pspec)
  70
  71         # frequently used aliases
  72         op = dut.i.ctx.op
  73         msr_o = dut.o.msr
  74         srr1_i = dut.i.srr1
  75
  76         comb += op.eq(rec)
  77
  78         # start of properties
  79         with m.Switch(op.insn_type):
  80             with m.Case(MicrOp.OP_SC):
  81                 comb += [
  82                     is_ok(dut.o.nia, Const(0xC00)),
  83                     is_ok(dut.o.srr0, dut.i.cia + 4),
  84                     is_ok(dut.o.srr1, full_function_bits(dut.i.msr)),
  85                 ]
  86             with m.Case(MicrOp.OP_RFID):
  87                 def field(r, start, end):
  88                     return r[63-end:63-start]
  89
  90                 comb += [
  91                     Assert(msr_o.ok),
  92                     Assert(dut.o.nia.ok),
  93
  94                     Assert(msr_o[MSR.HV] == (srr1_i[MSR.HV] & dut.i.msr[MSR.HV])),
  95                     Assert(msr_o[MSR.EE] == (srr1_i[MSR.EE] | srr1_i[MSR.PR])),
  96                     Assert(msr_o[MSR.IR] == (srr1_i[MSR.IR] | srr1_i[MSR.PR])),
  97                     Assert(msr_o[MSR.DR] == (srr1_i[MSR.DR] | srr1_i[MSR.PR])),
  98                     Assert(field(msr_o, 0, 2) == field(srr1_i, 0, 2)),
  99                     Assert(field(msr_o, 4, 28) == field(srr1_i, 4, 28)),
 100                     Assert(msr_o[63-32] == srr1_i[63-32]),
 101                     Assert(field(msr_o, 37, 41) == field(srr1_i, 37, 41)),
 102                     Assert(field(msr_o, 49, 50) == field(srr1_i, 49, 50)),
 103                     Assert(field(msr_o, 52, 57) == field(srr1_i, 52, 57)),
 104                     Assert(field(msr_o, 60, 63) == field(srr1_i, 60, 63)),
 105                     Assert(dut.o.nia.data == Cat(Const(0, 2), dut.i.srr0[2:])),
 106                 ]
 107                 with m.If(dut.i.msr[MSR.HV]):
 108                     comb += Assert(msr_o[MSR.ME] == srr1_i[MSR.ME])
 109                 with m.Else():
 110                     comb += Assert(msr_o[MSR.ME] == dut.i.msr[MSR.ME])
 111                 with m.If((field(dut.i.msr, 29, 31) != 0b010) |
 112                           (field(dut.i.msr, 29, 31) != 0b000)):
 113                     comb += Assert(field(msr_o.data, 29, 31) == field(srr1_i, 29, 31))
 114
 115         comb += dut.i.ctx.matches(dut.o.ctx)
 116
 117         return m
 118
 119
 120 class TrapMainStageTestCase(FHDLTestCase):
 121     def test_formal(self):
 122         self.assertFormal(Driver(), mode="bmc", depth=10)
 123         self.assertFormal(Driver(), mode="cover", depth=10)
 124
 125     def test_ilang(self):
 126         vl = rtlil.convert(Driver(), ports=[])
 127         with open("trap_main_stage.il", "w") as f:
 128             f.write(vl)
 129
 130
 131 if __name__ == '__main__':
 132     unittest.main()
 133