src/soc/fu/spr/formal/proof_main_stage.py

   1 # Proof of correctness for SPR pipeline, main stage
   2
   3
   4 """
   5 Links:
   6 * https://bugs.libre-soc.org/show_bug.cgi?id=418
   7 """
   8
   9 from os import getenv
  10
  11 from unittest import skipUnless
  12
  13 from nmigen import (Elaboratable, Module)
  14 from nmigen.asserts import Assert
  15 from nmigen.cli import rtlil
  16
  17 from nmutil.formaltest import FHDLTestCase
  18
  19 from soc.fu.spr.main_stage import SPRMainStage
  20 from soc.fu.spr.pipe_data import SPRPipeSpec
  21
  22
  23 class Driver(Elaboratable):
  24     """
  25     Defines a module to drive the device under test and assert properties
  26     about its outputs.
  27     """
  28
  29     def elaborate(self, platform):
  30         m = Module()
  31         comb = m.d.comb
  32
  33         dut = SPRMainStage(SPRPipeSpec(id_wid=2))
  34
  35         # Output context is the same as the input context.
  36         comb += Assert(dut.o.ctx != dut.i.ctx)
  37
  38         return m
  39
  40
  41 class SPRMainStageTestCase(FHDLTestCase):
  42     @skipUnless(getenv("FORMAL_SPR"), "Exercise SPR formal tests [WIP]")
  43     def test_formal(self):
  44         self.assertFormal(Driver(), mode="bmc", depth=100)
  45         self.assertFormal(Driver(), mode="cover", depth=100)
  46
  47     def test_ilang(self):
  48         vl = rtlil.convert(Driver(), ports=[])
  49         with open("spr_main_stage.il", "w") as f:
  50             f.write(vl)
  51
  52
  53 if __name__ == '__main__':
  54     unittest.main()