src/soc/alu/formal/proof_input_stage.py

   1 # Proof of correctness for partitioned equal signal combiner
   2 # Copyright (C) 2020 Michael Nolan <mtnolan2640@gmail.com>
   3
   4 from nmigen import Module, Signal, Elaboratable, Mux
   5 from nmigen.asserts import Assert, AnyConst, Assume, Cover
   6 from nmigen.test.utils import FHDLTestCase
   7 from nmigen.cli import rtlil
   8
   9 from soc.alu.input_stage import ALUInputStage
  10 from soc.alu.pipe_data import ALUPipeSpec
  11 from soc.alu.alu_input_record import CompALUOpSubset
  12 import unittest
  13
  14
  15 # This defines a module to drive the device under test and assert
  16 # properties about its outputs
  17 class Driver(Elaboratable):
  18     def __init__(self):
  19         # inputs and outputs
  20         pass
  21
  22     def elaborate(self, platform):
  23         m = Module()
  24         comb = m.d.comb
  25
  26         rec = CompALUOpSubset()
  27         recwidth = 0
  28         # Setup random inputs for dut.op
  29         for p in rec.ports():
  30             width = p.width
  31             recwidth += width
  32             comb += p.eq(AnyConst(width))
  33
  34         pspec = ALUPipeSpec(id_wid=2, op_wid=recwidth)
  35         m.submodules.dut = dut = ALUInputStage(pspec)
  36
  37         a = Signal(64)
  38         b = Signal(64)
  39         comb += [dut.i.a.eq(a),
  40                  dut.i.b.eq(b),
  41                  a.eq(AnyConst(64)),
  42                  b.eq(AnyConst(64))]
  43
  44
  45         comb += dut.i.ctx.op.eq(rec)
  46
  47
  48         # Assert that op gets copied from the input to output
  49         for p in rec.ports():
  50             name = p.name
  51             rec_sig = p
  52             dut_sig = getattr(dut.o.ctx.op, name)
  53             comb += Assert(dut_sig == rec_sig)
  54
  55         with m.If(rec.invert_a):
  56             comb += Assert(dut.o.a == ~a)
  57         with m.Else():
  58             comb += Assert(dut.o.a == a)
  59         comb += Assert(dut.o.b == b)
  60
  61
  62
  63
  64         return m
  65
  66 class GTCombinerTestCase(FHDLTestCase):
  67     def test_formal(self):
  68         module = Driver()
  69         self.assertFormal(module, mode="bmc", depth=4)
  70         self.assertFormal(module, mode="cover", depth=4)
  71     def test_ilang(self):
  72         dut = Driver()
  73         vl = rtlil.convert(dut, ports=[])
  74         with open("input_stage.il", "w") as f:
  75             f.write(vl)
  76
  77
  78 if __name__ == '__main__':
  79     unittest.main()