switch to using nmutil's FHDLTestCase
[ieee754fpu.git] / 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 nmigen.test.utils 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()