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