src/soc/alu/formal/proof_main_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, Cat
   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.main_stage import ALUMainStage
  10 from soc.alu.pipe_data import ALUPipeSpec
  11 from soc.alu.alu_input_record import CompALUOpSubset
  12 from soc.decoder.power_enums import InternalOp
  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, op_wid=recwidth)
  36         m.submodules.dut = dut = ALUMainStage(pspec)
  37
  38         a = Signal(64)
  39         b = Signal(64)
  40         carry_in = Signal()
  41         so_in = Signal()
  42         comb += [dut.i.a.eq(a),
  43                  dut.i.b.eq(b),
  44                  dut.i.carry_in.eq(carry_in),
  45                  dut.i.so.eq(so_in),
  46                  a.eq(AnyConst(64)),
  47                  b.eq(AnyConst(64)),
  48                  carry_in.eq(AnyConst(1)),
  49                  so_in.eq(AnyConst(1))]
  50
  51
  52         comb += dut.i.ctx.op.eq(rec)
  53
  54
  55         # Assert that op gets copied from the input to output
  56         for p in rec.ports():
  57             name = p.name
  58             rec_sig = p
  59             dut_sig = getattr(dut.o.ctx.op, name)
  60             comb += Assert(dut_sig == rec_sig)
  61
  62         with m.Switch(rec.insn_type):
  63             with m.Case(InternalOp.OP_ADD):
  64                 comb += Assert(Cat(dut.o.o, dut.o.carry_out) ==
  65                                (a + b + carry_in))
  66             with m.Case(InternalOp.OP_AND):
  67                 comb += Assert(dut.o.o == a & b)
  68             with m.Case(InternalOp.OP_OR):
  69                 comb += Assert(dut.o.o == a | b)
  70             with m.Case(InternalOp.OP_XOR):
  71                 comb += Assert(dut.o.o == a ^ b)
  72
  73
  74         return m
  75
  76 class GTCombinerTestCase(FHDLTestCase):
  77     def test_formal(self):
  78         module = Driver()
  79         self.assertFormal(module, mode="bmc", depth=4)
  80         self.assertFormal(module, mode="cover", depth=4)
  81     def test_ilang(self):
  82         dut = Driver()
  83         vl = rtlil.convert(dut, ports=[])
  84         with open("main_stage.il", "w") as f:
  85             f.write(vl)
  86
  87
  88 if __name__ == '__main__':
  89     unittest.main()