src/soc/fu/logical/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 nmutil.formaltest import FHDLTestCase
   7 from nmigen.cli import rtlil
   8
   9 from soc.fu.alu.input_stage import ALUInputStage
  10 from soc.fu.alu.pipe_data import ALUPipeSpec
  11 from soc.fu.alu.alu_input_record import CompALUOpSubset
  12 from openpower.decoder.power_enums import MicrOp
  13 import unittest
  14
  15
  16 # This defines a module to drive the device under test and assert
  17 # properties about its outputs
  18 class Driver(Elaboratable):
  19     def __init__(self):
  20         # inputs and outputs
  21         pass
  22
  23     def elaborate(self, platform):
  24         m = Module()
  25         comb = m.d.comb
  26
  27         rec = CompALUOpSubset()
  28         recwidth = 0
  29         # Setup random inputs for dut.op
  30         for p in rec.ports():
  31             width = p.width
  32             recwidth += width
  33             comb += p.eq(AnyConst(width))
  34
  35         pspec = ALUPipeSpec(id_wid=2, parent_pspec=None)
  36         m.submodules.dut = dut = ALUInputStage(pspec)
  37
  38         a = Signal(64)
  39         b = Signal(64)
  40         comb += [dut.i.a.eq(a),
  41                  dut.i.b.eq(b),
  42                  a.eq(AnyConst(64)),
  43                  b.eq(AnyConst(64))]
  44
  45         comb += dut.i.ctx.op.eq(rec)
  46
  47         # Assert that op gets copied from the input to output
  48         for p in rec.ports():
  49             name = p.name
  50             rec_sig = p
  51             dut_sig = getattr(dut.o.ctx.op, name)
  52             comb += Assert(dut_sig == rec_sig)
  53
  54         with m.If(rec.invert_in):
  55             comb += Assert(dut.o.a == ~a)
  56         with m.Else():
  57             comb += Assert(dut.o.a == a)
  58
  59         with m.If(rec.imm_data.imm_ok &
  60                   ~(rec.insn_type == MicrOp.OP_RLC)):
  61             comb += Assert(dut.o.b == rec.imm_data.imm)
  62         with m.Else():
  63             comb += Assert(dut.o.b == b)
  64
  65         return m
  66
  67
  68 class GTCombinerTestCase(FHDLTestCase):
  69     def test_formal(self):
  70         module = Driver()
  71         self.assertFormal(module, mode="bmc", depth=4)
  72         self.assertFormal(module, mode="cover", depth=4)
  73
  74     def test_ilang(self):
  75         dut = Driver()
  76         vl = rtlil.convert(dut, ports=[])
  77         with open("input_stage.il", "w") as f:
  78             f.write(vl)
  79
  80
  81 if __name__ == '__main__':
  82     unittest.main()