switch to using nmutil's FHDLTestCase
[ieee754fpu.git] / src / ieee754 / fpcmp / formal / proof_fpcmp_mod.py
1 # Proof of correctness for FPCMP 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.fpcmp.fpcmp import FPCMPPipeMod
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 FPCMPDriver(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 = FPCMPPipeMod(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 m.d.comb += Assert((z1.v == 0) | (z1.v == 1))
50
51 a_lt_b = Signal()
52
53 with m.If(a1.is_zero & b1.is_zero):
54 m.d.comb += a_lt_b.eq(0)
55 with m.Elif(a1.s != b1.s):
56 m.d.comb += a_lt_b.eq(a1.s > b1.s)
57 with m.Elif(a1.s == 0):
58 m.d.comb += a_lt_b.eq(a1.v[0:width-1] < b1.v[0:width-1])
59 with m.Else():
60 m.d.comb += a_lt_b.eq(a1.v[0:width-1] > b1.v[0:width-1])
61
62 a_eq_b = Signal()
63 m.d.comb += a_eq_b.eq((a1.v == b1.v) | (a1.is_zero & b1.is_zero))
64
65
66 with m.If(a1.is_nan | b1.is_nan):
67 m.d.comb += Assert(z1.v == 0)
68 with m.Else():
69 with m.Switch(opc):
70 with m.Case(0b10):
71 m.d.comb += Assert((z1.v == a_eq_b))
72 with m.Case(0b00):
73 m.d.comb += Assert(z1.v == (a_lt_b))
74 with m.Case(0b01):
75 m.d.comb += Assert(z1.v == (a_lt_b | a_eq_b))
76
77
78
79
80 # connect up the inputs and outputs.
81 m.d.comb += dut.i.a.eq(a)
82 m.d.comb += dut.i.b.eq(b)
83 m.d.comb += dut.i.ctx.op.eq(opc)
84 m.d.comb += dut.i.muxid.eq(muxid)
85 m.d.comb += z.eq(dut.o.z)
86
87 return m
88
89 def ports(self):
90 return []
91
92
93 class FPCMPTestCase(FHDLTestCase):
94 def test_fpcmp(self):
95 for bits in [32, 16, 64]:
96 module = FPCMPDriver(PipelineSpec(bits, 2, 2))
97 self.assertFormal(module, mode="bmc", depth=4)
98
99
100 if __name__ == '__main__':
101 unittest.main()