symfpu: Test comparisons

tests/symfpu/edges.sv

@@ -202,6 +202,12 @@ module edges(input clk);
     assign rounded_000 = '0;
 `endif
 
+`ifdef MAX
+    wire choose_max = 1;
+`else
+    wire choose_max = 0;
+`endif
+
     wire rm_RNE = rm[0] == 1'b1;
     wire rm_RNA = rm[1:0] == 2'b10;
     wire rm_RTP = rm[2:0] == 3'b100;
@@ -250,19 +256,21 @@ module edges(input clk);
 
         // all flags are possible
         cover (NV);
-`ifdef DIVS
+`ifndef COMPARES
-// only div can div/zero
+    `ifdef DIVS
+    // only div can div/zero
         cover (DZ);
-`endif
-`ifndef SQRTS
-// sqrt can't overflow or underflow
-        cover (OF);
-    `ifndef ADDSUB
-    // add/sub can't underflow
-        cover (UF);
     `endif
-`endif
+    `ifndef SQRTS
+    // sqrt can't overflow or underflow
+        cover (OF);
+        `ifndef ADDSUB
+        // add/sub can't underflow
+        cover (UF);
+        `endif
+    `endif
         cover (NX);
+`endif
         cover (!NV);
         cover (!DZ);
         cover (!OF);
@@ -282,6 +290,7 @@ module edges(input clk);
         cover (o_ebmin);
 `endif
 
+`ifndef COMPARES
 `ifndef SQRTS
         if (OF) begin
             cover (o_inf);
@@ -324,7 +333,12 @@ module edges(input clk);
             assert (!NX);
         end
 
-        if (a_snan)
+        if (NV)
+            // output = qNaN
+            assert (o_qnan);
+`endif // !COMPARES
+
+        if (a_snan || b_snan)
             // signalling NaN raises invalid exception
             assert (NV);
 
@@ -336,10 +350,6 @@ module edges(input clk);
             // output = +-inf
             assert (o_inf);
 
-        if (NV)
-            // output = qNaN
-            assert (o_qnan);
-
         if (OF)
             // overflow is always inexact
             assert (NX);
@@ -360,6 +370,57 @@ module edges(input clk);
             // a non-underflowing subnormal is exact
             assert (!NX);
 
+`ifdef COMPARES
+        assume (c_zero);
+        assert (!OF);
+        assert (!UF);
+        assert (!NX);
+        assert (!DZ);
+
+        if (!a_nan && b_nan)
+            assert (o == a);
+        else if (a_nan && !b_nan)
+            assert (o == b);
+        else if (a_nan && b_nan)
+            assert (o_nan);
+        else begin
+            assert (o == a || o == b);
+
+            if (a_inf) begin
+                if (a_sign == choose_max)
+                    assert (o == b);
+                else
+                    assert (o == a);
+            end
+
+            if (b_inf) begin
+                if (b_sign == choose_max)
+                    assert (o == a);
+                else
+                    assert (o == b);
+            end
+        end
+
+        if (!a_special && !b_special) begin
+            if (a_sign != b_sign)
+                if (a_sign == choose_max)
+                    assert (o == b);
+                else
+                    assert (o == a);
+            // a_sign == b_sign
+            else if (a_exp != b_exp)
+                if ((a_exp > b_exp) ^ a_sign ^ choose_max)
+                    assert (o == b);
+                else
+                    assert (o == a);
+            // a_exp == b_exp
+            else if ((a_sig > b_sig) ^ a_sign ^ choose_max)
+                assert (o == b);
+            else
+                assert (o == a);
+        end
+`endif
+
 `ifdef DIVS
         assume (c_zero);
         // div/zero only when a is finite

tests/symfpu/run-test.sh

@@ -35,6 +35,14 @@ prove_op() {
     done
 }
 
+prove_op_unrounded() {
+    # DYN is default rounding mode, so this is (currently) equivalent to no rounding mode
+    # but this does skip verifying the built in asserts
+    op=$1
+    defs=$2
+    prove_rm $op "DYN" "$defs"
+}
+
 prove_op sqrt "-DSQRT -DSQRTS"
 prove_op add "-DADD -DADDSUB -DADDS"
 prove_op sub "-DSUB -DADDSUB -DADDS"
@@ -45,4 +53,7 @@ prove_op muladd "-DMULADD -DMULS -DADDS"
 prove_op altdiv "-DALTDIV -DDIVS"
 prove_op altsqrt "-DALTSQRT -DSQRTS"
 
+prove_op_unrounded min "-DMIN -DCOMPARES"
+prove_op_unrounded max "-DMAX -DCOMPARES"
+
 generate_mk --yosys-scripts