From 4946e26cba1604172bdcbef2d21b9e9ccc45809e Mon Sep 17 00:00:00 2001 From: Michael Nolan Date: Sun, 2 Feb 2020 14:41:56 -0500 Subject: [PATCH] Handle -0 and +0 equals and < --- src/ieee754/fpcmp/formal/proof_fpcmp_mod.py | 17 +++++++---- src/ieee754/fpcmp/fpcmp.py | 20 +++++++++---- src/ieee754/fpcmp/test/test_fpcmp_pipe.py | 31 ++++++++++++++++++--- 3 files changed, 52 insertions(+), 16 deletions(-) diff --git a/src/ieee754/fpcmp/formal/proof_fpcmp_mod.py b/src/ieee754/fpcmp/formal/proof_fpcmp_mod.py index 45a978d1..4f3d273e 100644 --- a/src/ieee754/fpcmp/formal/proof_fpcmp_mod.py +++ b/src/ieee754/fpcmp/formal/proof_fpcmp_mod.py @@ -50,12 +50,17 @@ class FPCMPDriver(Elaboratable): a_lt_b = Signal() - with m.If(a1.s != b1.s): + with m.If(a1.is_zero & b1.is_zero): + m.d.comb += a_lt_b.eq(0) + with m.Elif(a1.s != b1.s): m.d.comb += a_lt_b.eq(a1.s > b1.s) with m.Elif(a1.s == 0): - m.d.comb += a_lt_b.eq(a1.v[0:31] < b1.v[0:31]) + m.d.comb += a_lt_b.eq(a1.v[0:width-1] < b1.v[0:width-1]) with m.Else(): - m.d.comb += a_lt_b.eq(a1.v[0:31] > b1.v[0:31]) + m.d.comb += a_lt_b.eq(a1.v[0:width-1] > b1.v[0:width-1]) + + a_eq_b = Signal() + m.d.comb += a_eq_b.eq((a1.v == b1.v) | (a1.is_zero & b1.is_zero)) with m.If(a1.is_nan | b1.is_nan): @@ -63,12 +68,12 @@ class FPCMPDriver(Elaboratable): with m.Else(): with m.Switch(opc): with m.Case(0b10): - m.d.comb += Assert(z1.v == (a1.v == b1.v)) + m.d.comb += Assert((z1.v == a_eq_b)) with m.Case(0b00): m.d.comb += Assert(z1.v == (a_lt_b)) with m.Case(0b01): - m.d.comb += Assert(z1.v == (a_lt_b | - (a1.v == b1.v))) + m.d.comb += Assert(z1.v == (a_lt_b | a_eq_b)) + diff --git a/src/ieee754/fpcmp/fpcmp.py b/src/ieee754/fpcmp/fpcmp.py index 16405b55..067642d3 100644 --- a/src/ieee754/fpcmp/fpcmp.py +++ b/src/ieee754/fpcmp/fpcmp.py @@ -46,13 +46,20 @@ class FPCMPPipeMod(PipeModBase): m.d.comb += [a1.v.eq(self.i.a), b1.v.eq(self.i.b)] + both_zero = Signal() + comb += both_zero.eq((a1.v[0:width-1] == 0) & + (b1.v[0:width-1] == 0)) + ab_equal = Signal() - m.d.comb += ab_equal.eq(a1.v == b1.v) + m.d.comb += ab_equal.eq((a1.v == b1.v) | both_zero) + contains_nan = Signal() m.d.comb += contains_nan.eq(a1.is_nan | b1.is_nan) a_lt_b = Signal() - # if(a1.s != b1.s): + # if(a1.is_zero && b1.is_zero): + # a_lt_b = 0 + # elif(a1.s != b1.s): # a_lt_b = a1.s > b1.s (a is more negative than b) signs_same = Signal() comb += signs_same.eq(a1.s > b1.s) @@ -64,12 +71,13 @@ class FPCMPPipeMod(PipeModBase): # a_lt_b = a[0:31] > b[0:31] signs_different = Signal() comb += signs_different.eq(Mux(a1.s, - (a1.v[0:31] > b1.v[0:31]), - (a1.v[0:31] < b1.v[0:31]))) + (a1.v[0:width-1] > b1.v[0:width-1]), + (a1.v[0:width-1] < b1.v[0:width-1]))) - comb += a_lt_b.eq(Mux(a1.s == b1.s, + comb += a_lt_b.eq(Mux(both_zero, 0, + Mux(a1.s == b1.s, signs_different, - signs_same)) + signs_same))) no_nan = Signal() # switch(opcode): diff --git a/src/ieee754/fpcmp/test/test_fpcmp_pipe.py b/src/ieee754/fpcmp/test/test_fpcmp_pipe.py index af0ce953..cff066ef 100644 --- a/src/ieee754/fpcmp/test/test_fpcmp_pipe.py +++ b/src/ieee754/fpcmp/test/test_fpcmp_pipe.py @@ -3,6 +3,8 @@ from ieee754.fpcmp.pipeline import (FPCMPMuxInOut) from ieee754.fpcommon.test.fpmux import runfp +from ieee754.fpcommon.test.case_gen import run_pipe_fp +from ieee754.fpcommon.test import unit_test_single from sfpy import Float16, Float32, Float64 import math @@ -32,9 +34,30 @@ def test_fpcmp_le(): runfp(dut, 32, "test_fpcmp_le", Float32, fpcmp_le, n_vals=100, opcode=0b01) +def cornercases(): + nan = Float32(float('nan')).bits + yield nan, Float32(1.0).bits + yield Float32(1.0).bits, nan + yield nan, nan + yield Float32(0.0).bits, Float32(-0.0).bits + yield Float32(-0.0).bits, Float32(0.0).bits + +def test_fpcmp_cornercases(): + dut = FPCMPMuxInOut(32, 4) + run_pipe_fp(dut, 32, "test_fpcmp_f32_corner_eq", unit_test_single, + Float32, cornercases, fpcmp_eq, 5, + opcode=0b10) + run_pipe_fp(dut, 32, "test_fpcmp_f32_corner_le", unit_test_single, + Float32, cornercases, fpcmp_le, 5, + opcode=0b01) + run_pipe_fp(dut, 32, "test_fpcmp_f32_corner_lt", unit_test_single, + Float32, cornercases, fpcmp_lt, 5, + opcode=0b00) + if __name__ == '__main__': - for i in range(50): - test_fpcmp_lt() - test_fpcmp_eq() - test_fpcmp_le() + test_fpcmp_cornercases() + # for i in range(50): + # test_fpcmp_lt() + # test_fpcmp_eq() + # test_fpcmp_le() -- 2.30.2