src/soc/fu/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, Repl,
   5                     signed)
   6 from nmigen.asserts import Assert, AnyConst, Assume, Cover
   7 from nmigen.test.utils import FHDLTestCase
   8 from nmigen.cli import rtlil
   9
  10 from soc.fu.alu.main_stage import ALUMainStage
  11 from soc.fu.alu.pipe_data import ALUPipeSpec
  12 from soc.fu.alu.alu_input_record import CompALUOpSubset
  13 from soc.decoder.power_enums import InternalOp
  14 import unittest
  15
  16
  17 # This defines a module to drive the device under test and assert
  18 # properties about its outputs
  19 class Driver(Elaboratable):
  20     def __init__(self):
  21         # inputs and outputs
  22         pass
  23
  24     def elaborate(self, platform):
  25         m = Module()
  26         comb = m.d.comb
  27
  28         rec = CompALUOpSubset()
  29         recwidth = 0
  30         # Setup random inputs for dut.op
  31         for p in rec.ports():
  32             width = p.width
  33             recwidth += width
  34             comb += p.eq(AnyConst(width))
  35
  36         pspec = ALUPipeSpec(id_wid=2, op_wid=recwidth)
  37         m.submodules.dut = dut = ALUMainStage(pspec)
  38
  39         # convenience variables
  40         a = dut.i.a
  41         b = dut.i.b
  42         carry_in = dut.i.carry_in
  43         so_in = dut.i.so
  44         carry_out = dut.o.xer_co.data[0]
  45         carry_out32 = dut.o.xer_co.data[1]
  46         o = dut.o.o
  47
  48         # setup random inputs
  49         comb += [a.eq(AnyConst(64)),
  50                  b.eq(AnyConst(64)),
  51                  carry_in.eq(AnyConst(1)),
  52                  so_in.eq(AnyConst(1))]
  53
  54         comb += dut.i.ctx.op.eq(rec)
  55
  56         # Assert that op gets copied from the input to output
  57         for rec_sig in rec.ports():
  58             name = rec_sig.name
  59             dut_sig = getattr(dut.o.ctx.op, name)
  60             comb += Assert(dut_sig == rec_sig)
  61
  62         # signed and signed/32 versions of input a
  63         a_signed = Signal(signed(64))
  64         a_signed_32 = Signal(signed(32))
  65         comb += a_signed.eq(a)
  66         comb += a_signed_32.eq(a[0:32])
  67
  68         comb += Assume(a[32:64] == 0)
  69         comb += Assume(b[32:64] == 0)
  70         # main assertion of arithmetic operations
  71         with m.Switch(rec.insn_type):
  72             with m.Case(InternalOp.OP_ADD):
  73
  74                 comb += Assert(Cat(o, carry_out) == (a + b + carry_in))
  75
  76                 # CA32
  77                 comb += Assert((a[0:32] + b[0:32] + carry_in)[32]
  78                                == carry_out32)
  79             with m.Case(InternalOp.OP_EXTS):
  80                 for i in [1, 2, 4]:
  81                     with m.If(rec.data_len == i):
  82                         comb += Assert(o[0:i*8] == a[0:i*8])
  83                         comb += Assert(o[i*8:64] == Repl(a[i*8-1], 64-(i*8)))
  84
  85         return m
  86
  87
  88 class ALUTestCase(FHDLTestCase):
  89     def test_formal(self):
  90         module = Driver()
  91         self.assertFormal(module, mode="bmc", depth=2)
  92         self.assertFormal(module, mode="cover", depth=2)
  93     def test_ilang(self):
  94         dut = Driver()
  95         vl = rtlil.convert(dut, ports=[])
  96         with open("main_stage.il", "w") as f:
  97             f.write(vl)
  98
  99
 100 if __name__ == '__main__':
 101     unittest.main()