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 nmigen import (Elaboratable, Module)
  10 from nmigen.asserts import Assert, AnyConst, Assume
  11 from nmigen.cli import rtlil
  12
  13 from nmutil.formaltest import FHDLTestCase
  14
  15 from soc.fu.spr.main_stage import SPRMainStage
  16 from soc.fu.spr.pipe_data import SPRPipeSpec
  17 from soc.fu.spr.spr_input_record import CompSPROpSubset
  18 from soc.decoder.power_enums import MicrOp
  19 import unittest
  20
  21
  22 class Driver(Elaboratable):
  23     """
  24     Defines a module to drive the device under test and assert properties
  25     about its outputs.
  26     """
  27
  28     def elaborate(self, platform):
  29         m = Module()
  30         comb = m.d.comb
  31
  32         # cookie-cutting most of this from alu formal proof_main_stage.py
  33
  34         rec = CompSPROpSubset()
  35         # Setup random inputs for dut.op
  36         for p in rec.ports():
  37             width = p.width
  38             comb += p.eq(AnyConst(width))
  39
  40         pspec = SPRPipeSpec(id_wid=2)
  41         m.submodules.dut = dut = SPRMainStage(pspec)
  42
  43         # convenience variables
  44         a = dut.i.a
  45         ca_in = dut.i.xer_ca[0]   # CA carry in
  46         ca32_in = dut.i.xer_ca[1] # CA32 carry in 32
  47         so_in = dut.i.xer_so      # SO sticky overflow
  48
  49         ca_o = dut.o.xer_ca.data[0]   # CA carry out
  50         ca32_o = dut.o.xer_ca.data[1] # CA32 carry out32
  51         ov_o = dut.o.xer_ov.data[0]   # OV overflow
  52         ov32_o = dut.o.xer_ov.data[1] # OV32 overflow32
  53         o = dut.o.o.data
  54
  55         # setup random inputs
  56         comb += [a.eq(AnyConst(64)),
  57                  ca_in.eq(AnyConst(0b11)),
  58                  so_in.eq(AnyConst(1))]
  59
  60         comb += dut.i.ctx.op.eq(rec)
  61
  62         # Assert that op gets copied from the input to output
  63         for rec_sig in rec.ports():
  64             name = rec_sig.name
  65             dut_sig = getattr(dut.o.ctx.op, name)
  66             comb += Assert(dut_sig == rec_sig)
  67
  68         return m
  69
  70
  71 class SPRMainStageTestCase(FHDLTestCase):
  72     #don't worry about it - tests are run manually anyway.  fail is fine.
  73     #@skipUnless(getenv("FORMAL_SPR"), "Exercise SPR formal tests [WIP]")
  74     def test_formal(self):
  75         self.assertFormal(Driver(), mode="bmc", depth=100)
  76         self.assertFormal(Driver(), mode="cover", depth=100)
  77
  78     def test_ilang(self):
  79         vl = rtlil.convert(Driver(), ports=[])
  80         with open("spr_main_stage.il", "w") as f:
  81             f.write(vl)
  82
  83
  84 if __name__ == '__main__':
  85     unittest.main()