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
  13 from nmigen.asserts import Assert, AnyConst
  14 from nmigen.cli import rtlil
  15
  16 from nmutil.formaltest import FHDLTestCase
  17
  18 from soc.decoder.power_enums import MicrOp
  19
  20 from soc.fu.trap.main_stage import TrapMainStage
  21 from soc.fu.trap.pipe_data import TrapPipeSpec
  22 from soc.fu.trap.trap_input_record import CompTrapOpSubset
  23
  24
  25 def is_ok(sig, value):
  26     """
  27     Answers with a list of assertions that checks for valid data on
  28     a pipeline stage output.  sig.data must have the anticipated value,
  29     and sig.ok must be asserted.  The `value` is constrained to the width
  30     of the sig.data field it's verified against, so it's safe to add, etc.
  31     offsets to Nmigen signals without having to worry about inequalities from
  32     differing signal widths.
  33     """
  34     return [
  35         Assert(sig.data == value[0:len(sig.data)]),
  36         Assert(sig.ok),
  37     ]
  38
  39
  40 def full_function_bits(msr):
  41     """
  42     Answers with a numeric constant signal with all "full functional"
  43     bits filled in, but all partial functional bits zeroed out.
  44
  45     See src/soc/fu/trap/main_stage.py:msr_copy commentary for details.
  46     """
  47     zeros16_21 = Const(0, (22 - 16))
  48     zeros27_30 = Const(0, (31 - 27))
  49     return Cat(msr[0:16], zeros16_21, msr[22:27], zeros27_30, msr[31:64])
  50
  51
  52 def is_full_function_ok(out, inp):
  53     """
  54     Answers with a list of assertions that ONLY covers the full function
  55     MSR bits.  It ignores the remaining bits.
  56     """
  57     return [
  58         Assert(out.data[0:16] == inp[0:16]),
  59 #       Assert(out.data[22:27] == inp[22:27]),
  60 #       Assert(out.data[31:64] == inp[31:64]),
  61         Assert(out.ok),
  62     ]
  63
  64
  65 class Driver(Elaboratable):
  66     """
  67     """
  68
  69     def elaborate(self, platform):
  70         m = Module()
  71         comb = m.d.comb
  72
  73         rec = CompTrapOpSubset()
  74         pspec = TrapPipeSpec(id_wid=2)
  75
  76         m.submodules.dut = dut = TrapMainStage(pspec)
  77
  78         # frequently used aliases
  79         op = dut.i.ctx.op
  80
  81         comb += op.eq(rec)
  82
  83         # start of properties
  84         with m.Switch(op.insn_type):
  85             with m.Case(MicrOp.OP_SC):
  86                 comb += [
  87                     is_ok(dut.o.nia, Const(0xC00)),
  88                     is_ok(dut.o.srr0, dut.i.cia + 4),
  89                     is_ok(dut.o.srr1, full_function_bits(dut.i.msr)),
  90                 ]
  91             with m.Case(MicrOp.OP_RFID):
  92                 comb += [
  93                     is_ok(dut.o.nia, Cat(Const(0, 2), dut.i.srr0[2:])),
  94                     is_full_function_ok(dut.o.msr, dut.i.srr1),
  95                 ]
  96
  97         comb += dut.i.ctx.matches(dut.o.ctx)
  98
  99         return m
 100
 101
 102 class TrapMainStageTestCase(FHDLTestCase):
 103     def test_formal(self):
 104         self.assertFormal(Driver(), mode="bmc", depth=10)
 105         self.assertFormal(Driver(), mode="cover", depth=10)
 106
 107     def test_ilang(self):
 108         vl = rtlil.convert(Driver(), ports=[])
 109         with open("trap_main_stage.il", "w") as f:
 110             f.write(vl)
 111
 112
 113 if __name__ == '__main__':
 114     unittest.main()
 115