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 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.fu.trap.main_stage import TrapMainStage
  19 from soc.fu.trap.pipe_data import TrapPipeSpec
  20
  21
  22 class Driver(Elaboratable):
  23     """
  24     """
  25
  26     def elaborate(self, platform):
  27         m = Module()
  28         comb = m.d.comb
  29
  30         pspec = TrapPipeSpec(id_wid=2)
  31
  32         m.submodules.dut = dut = TrapMainStage(pspec)
  33
  34         comb += dut.i.ctx.matches(dut.o.ctx)
  35
  36         return m
  37
  38
  39 class TrapMainStageTestCase(FHDLTestCase):
  40     def test_formal(self):
  41         self.assertFormal(Driver(), mode="bmc", depth=10)
  42         self.assertFormal(Driver(), mode="cover", depth=10)
  43
  44     def test_ilang(self):
  45         vl = rtlil.convert(Driver(), ports=[])
  46         with open("trap_main_stage.il", "w") as f:
  47             f.write(vl)
  48
  49
  50 if __name__ == '__main__':
  51     unittest.main()
  52