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 nmutil.formaltest 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()