src/ieee754/fpmax/formal/proof_fmax_mod.py

   1 # Proof of correctness for FPMAX module
   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
   6 from nmutil.formaltest import FHDLTestCase
   7
   8 from ieee754.fpcommon.fpbase import FPNumDecode, FPNumBaseRecord
   9 from ieee754.fpmax.fpmax import FPMAXPipeMod
  10 from ieee754.pipeline import PipelineSpec
  11 import unittest
  12
  13
  14 # This defines a module to drive the device under test and assert
  15 # properties about its outputs
  16 class FPMAXDriver(Elaboratable):
  17     def __init__(self, pspec):
  18         # inputs and outputs
  19         self.pspec = pspec
  20
  21     def elaborate(self, platform):
  22         m = Module()
  23         width = self.pspec.width
  24
  25         # setup the inputs and outputs of the DUT as anyconst
  26         a = Signal(width)
  27         b = Signal(width)
  28         z = Signal(width)
  29         opc = Signal(self.pspec.op_wid)
  30         muxid = Signal(self.pspec.id_wid)
  31         m.d.comb += [a.eq(AnyConst(width)),
  32                      b.eq(AnyConst(width)),
  33                      opc.eq(AnyConst(self.pspec.op_wid)),
  34                      muxid.eq(AnyConst(self.pspec.id_wid))]
  35
  36         m.submodules.dut = dut = FPMAXPipeMod(self.pspec)
  37
  38         # Decode the inputs and outputs so they're easier to work with
  39         a1 = FPNumBaseRecord(width, False)
  40         b1 = FPNumBaseRecord(width, False)
  41         z1 = FPNumBaseRecord(width, False)
  42         m.submodules.sc_decode_a = a1 = FPNumDecode(None, a1)
  43         m.submodules.sc_decode_b = b1 = FPNumDecode(None, b1)
  44         m.submodules.sc_decode_z = z1 = FPNumDecode(None, z1)
  45         m.d.comb += [a1.v.eq(a),
  46                      b1.v.eq(b),
  47                      z1.v.eq(z)]
  48
  49         # Since this calculates the min/max of two values, the value
  50         # it returns should either be one of the two values, or NaN
  51         m.d.comb += Assert((z1.v == a1.v) | (z1.v == b1.v) |
  52                            (z1.v == a1.fp.nan2(0)))
  53
  54         # If both the operands are NaN, max/min should return NaN
  55         with m.If(a1.is_nan & b1.is_nan):
  56             m.d.comb += Assert(z1.is_nan)
  57         # If only one of the operands is NaN, fmax and fmin should
  58         # return the other operand
  59         with m.Elif(a1.is_nan & ~b1.is_nan):
  60             m.d.comb += Assert(z1.v == b1.v)
  61         with m.Elif(b1.is_nan & ~a1.is_nan):
  62             m.d.comb += Assert(z1.v == a1.v)
  63         # If none of the operands are NaN, then compare the values and
  64         # determine the largest or smallest
  65         with m.Else():
  66             # Selects whether the result should be the left hand side
  67             # (a) or right hand side (b)
  68             isrhs = Signal()
  69             # if a1 is negative and b1 isn't, then we should return b1
  70             with m.If(a1.s != b1.s):
  71                 m.d.comb += isrhs.eq(a1.s > b1.s)
  72             with m.Else():
  73                 # if they both have the same sign, compare the
  74                 # exponent/mantissa as an integer
  75                 gt = Signal()
  76                 m.d.comb += gt.eq(a[0:width-1] < b[0:width-1])
  77                 # Invert the result we got if both sign bits are set
  78                 # (A bigger exponent/mantissa with a set sign bit
  79                 # means a smaller value)
  80                 m.d.comb += isrhs.eq(gt ^ a1.s)
  81
  82             with m.If(opc == 0):
  83                 m.d.comb += Assert(z1.v ==
  84                                    Mux(opc[0] ^ isrhs,
  85                                        b1.v, a1.v))
  86
  87         # connect up the inputs and outputs.
  88         m.d.comb += dut.i.a.eq(a)
  89         m.d.comb += dut.i.b.eq(b)
  90         m.d.comb += dut.i.ctx.op.eq(opc)
  91         m.d.comb += dut.i.muxid.eq(muxid)
  92         m.d.comb += z.eq(dut.o.z)
  93
  94         return m
  95
  96     def ports(self):
  97         return []
  98
  99
 100 class FPMAXTestCase(FHDLTestCase):
 101     def test_max(self):
 102         for bits in [16, 32, 64]:
 103             module = FPMAXDriver(PipelineSpec(bits, 2, 1))
 104             self.assertFormal(module, mode="bmc", depth=4)
 105
 106
 107 if __name__ == '__main__':
 108     unittest.main()