switch to using nmutil's FHDLTestCase
[ieee754fpu.git] / src / ieee754 / fsgnj / formal / proof_fsgnj_mod.py
1 # Proof of correctness for FSGNJ module
2 # Copyright (C) 2020 Michael Nolan <mtnolan2640@gmail.com>
3
4 from nmigen import Module, Signal, Elaboratable
5 from nmigen.asserts import Assert, Assume
6 from nmigen.test.utils import FHDLTestCase
7
8 from ieee754.fpcommon.fpbase import FPNumDecode, FPNumBaseRecord
9 from ieee754.fsgnj.fsgnj import FSGNJPipeMod
10 from ieee754.pipeline import PipelineSpec
11 import unittest
12
13 # This defines a module to drive the device under test and assert
14 # properties about its outputs
15 class FSGNJDriver(Elaboratable):
16 def __init__(self, pspec):
17 # inputs and outputs
18 self.pspec = pspec
19 self.a = Signal(pspec.width)
20 self.b = Signal(pspec.width)
21 self.z = Signal(pspec.width)
22 self.opc = Signal(pspec.op_wid)
23 self.muxid = Signal(pspec.id_wid)
24
25 def elaborate(self, platform):
26 m = Module()
27
28 m.submodules.dut = dut = FSGNJPipeMod(self.pspec)
29
30 a1 = FPNumBaseRecord(self.pspec.width, False)
31 b1 = FPNumBaseRecord(self.pspec.width, False)
32 z1 = FPNumBaseRecord(self.pspec.width, False)
33 m.submodules.sc_decode_a = a1 = FPNumDecode(None, a1)
34 m.submodules.sc_decode_b = b1 = FPNumDecode(None, b1)
35 m.submodules.sc_decode_z = z1 = FPNumDecode(None, z1)
36
37 m.d.comb += [a1.v.eq(self.a),
38 b1.v.eq(self.b),
39 z1.v.eq(self.z)]
40
41 # connect up the inputs and outputs. I think these could
42 # theoretically be $anyconst/$anysync but I'm not sure nmigen
43 # has support for that
44 m.d.comb += dut.i.a.eq(self.a)
45 m.d.comb += dut.i.b.eq(self.b)
46 m.d.comb += dut.i.ctx.op.eq(self.opc)
47 m.d.comb += dut.i.muxid.eq(self.muxid)
48 m.d.comb += self.z.eq(dut.o.z)
49
50 # Since the RISCV spec doesn't define what FSGNJ with a funct3
51 # field of 0b011 throug 0b111 does, they should be ignored.
52 m.d.comb += Assume(self.opc != 0b11)
53
54 # The RISCV spec (page 70) says FSGNJ "produces a result that
55 # takes all buts except the sign bit from [operand 1]". This
56 # asserts that that holds true
57 m.d.comb += Assert(z1.e == a1.e)
58 m.d.comb += Assert(z1.m == a1.m)
59
60 with m.Switch(self.opc):
61
62 # The RISCV Spec (page 70) states that for FSGNJ (opcode
63 # 0b00 in this case) "the result's sign bit is [operand
64 # 2's] sign bit"
65 with m.Case(0b00):
66 m.d.comb += Assert(z1.s == b1.s)
67
68 # The RISCV Spec (page 70) states that for FSGNJN (opcode
69 # 0b01 in this case) "the result's sign bit is the opposite
70 # of [operand 2's] sign bit"
71 with m.Case(0b01):
72 m.d.comb += Assert(z1.s == ~b1.s)
73 # The RISCV Spec (page 70) states that for FSGNJX (opcode
74 # 0b10 in this case) "the result's sign bit is the XOR of
75 # the sign bits of [operand 1] and [operand 2]"
76 with m.Case(0b10):
77 m.d.comb += Assert(z1.s == (a1.s ^ b1.s))
78
79 return m
80
81 def ports(self):
82 return [self.a, self.b, self.z, self.opc, self.muxid]
83
84
85 class FPMAXTestCase(FHDLTestCase):
86 def test_max(self):
87 for bits in [16, 32, 64]:
88 module = FSGNJDriver(PipelineSpec(bits, 2, 2))
89 self.assertFormal(module, mode="bmc", depth=4)
90
91
92 if __name__ == '__main__':
93 unittest.main()