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