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()