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