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         # and for the context muxid
  61         width = dut.i.ctx.muxid.width
  62         comb += dut.i.ctx.muxid.eq(AnyConst(width))
  63
  64         # assign the PowerDecode2 operation subset
  65         comb += dut.i.ctx.op.eq(rec)
  66
  67         # check that the operation (op) is passed through (and muxid)
  68         comb += Assert(dut.o.ctx.op == dut.i.ctx.op )
  69         comb += Assert(dut.o.ctx.muxid == dut.i.ctx.muxid )
  70
  71         return m
  72
  73
  74 class SPRMainStageTestCase(FHDLTestCase):
  75     #don't worry about it - tests are run manually anyway.  fail is fine.
  76     #@skipUnless(getenv("FORMAL_SPR"), "Exercise SPR formal tests [WIP]")
  77     def test_formal(self):
  78         self.assertFormal(Driver(), mode="bmc", depth=100)
  79         self.assertFormal(Driver(), mode="cover", depth=100)
  80
  81     def test_ilang(self):
  82         vl = rtlil.convert(Driver(), ports=[])
  83         with open("spr_main_stage.il", "w") as f:
  84             f.write(vl)
  85
  86
  87 if __name__ == '__main__':
  88     unittest.main()