from nmigen import Module, Signal, Elaboratable
from nmigen.asserts import Assert, Assume
-from nmigen.cli import rtlil
+from nmutil.formaltest import FHDLTestCase
+from ieee754.fpcommon.fpbase import FPNumDecode, FPNumBaseRecord
from ieee754.fsgnj.fsgnj import FSGNJPipeMod
from ieee754.pipeline import PipelineSpec
-import subprocess
-
+import unittest
# This defines a module to drive the device under test and assert
# properties about its outputs
m.submodules.dut = dut = FSGNJPipeMod(self.pspec)
+ a1 = FPNumBaseRecord(self.pspec.width, False)
+ b1 = FPNumBaseRecord(self.pspec.width, False)
+ z1 = FPNumBaseRecord(self.pspec.width, False)
+ m.submodules.sc_decode_a = a1 = FPNumDecode(None, a1)
+ m.submodules.sc_decode_b = b1 = FPNumDecode(None, b1)
+ m.submodules.sc_decode_z = z1 = FPNumDecode(None, z1)
+
+ m.d.comb += [a1.v.eq(self.a),
+ b1.v.eq(self.b),
+ z1.v.eq(self.z)]
+
# connect up the inputs and outputs. I think these could
# theoretically be $anyconst/$anysync but I'm not sure nmigen
# has support for that
# The RISCV spec (page 70) says FSGNJ "produces a result that
# takes all buts except the sign bit from [operand 1]". This
# asserts that that holds true
- m.d.comb += Assert(self.z[0:31] == self.a[0:31])
+ m.d.comb += Assert(z1.e == a1.e)
+ m.d.comb += Assert(z1.m == a1.m)
with m.Switch(self.opc):
# 0b00 in this case) "the result's sign bit is [operand
# 2's] sign bit"
with m.Case(0b00):
- m.d.comb += Assert(self.z[-1] == self.b[-1])
+ m.d.comb += Assert(z1.s == b1.s)
# The RISCV Spec (page 70) states that for FSGNJN (opcode
# 0b01 in this case) "the result's sign bit is the opposite
# of [operand 2's] sign bit"
with m.Case(0b01):
- m.d.comb += Assert(self.z[-1] == ~self.b[-1])
+ m.d.comb += Assert(z1.s == ~b1.s)
# The RISCV Spec (page 70) states that for FSGNJX (opcode
# 0b10 in this case) "the result's sign bit is the XOR of
# the sign bits of [operand 1] and [operand 2]"
with m.Case(0b10):
- m.d.comb += Assert(self.z[-1] == (self.a[-1] ^ self.b[-1]))
+ m.d.comb += Assert(z1.s == (a1.s ^ b1.s))
return m
return [self.a, self.b, self.z, self.opc, self.muxid]
-def run_test():
- m = FSGNJDriver(PipelineSpec(32, 2, 2))
-
- il = rtlil.convert(m, ports=m.ports())
- with open("proof.il", "w") as f:
- f.write(il)
- p = subprocess.Popen(['sby', '-f', 'proof.sby'],
- stdout=subprocess.PIPE,
- stderr=subprocess.PIPE)
- if p.wait() == 0:
- out, err = p.communicate()
- print("Proof successful!")
- print(out.decode('utf-8'))
- else:
- print("Proof failed")
- out, err = p.communicate()
- print(out.decode('utf-8'))
- print(err.decode('utf-8'))
-
-
-if __name__ == "__main__":
- run_test()
+class FPMAXTestCase(FHDLTestCase):
+ def test_max(self):
+ for bits in [16, 32, 64]:
+ module = FSGNJDriver(PipelineSpec(bits, 2, 2))
+ self.assertFormal(module, mode="bmc", depth=4)
+
+
+if __name__ == '__main__':
+ unittest.main()