From 1629c2bd3d410c9fb8df96cc844f13fd5afeb62b Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Fri, 20 Feb 2026 10:09:12 +1300 Subject: [PATCH] tests/symfpu: Add cover checks Include mask/map for abc inputs (and switch to `anyconst` instead of `anyseq`). Add false divide check for mantissa. Covers aren't currently being tested by anything (and have to be removed for `sat`), but I've been using it locally with SBY to confirm that the different edge cases are able to be verified (e.g. when verifying HardFloat against symfpu while using the masked inputs to reduce solver time). --- tests/symfpu/edges.sv | 176 ++++++++++++++++++++++++++++++++++++++- tests/symfpu/run-test.sh | 1 + 2 files changed, 174 insertions(+), 3 deletions(-) diff --git a/tests/symfpu/edges.sv b/tests/symfpu/edges.sv index 90b8b0de7..4b65c18f8 100644 --- a/tests/symfpu/edges.sv +++ b/tests/symfpu/edges.sv @@ -1,5 +1,29 @@ -module edges(); - (* anyseq *) reg [31:0] a, b, c; +module edges(input clk); + +`ifdef MASK + (* anyconst *) reg [31:0] a_in, b_in, c_in; + wire [31:0] a, b, c; + assign a = a_in & 32'hffc42108; + assign b = b_in & 32'hfff80001; + assign c = c_in & 32'hfff80001; +`elsif MAP + (* anyconst *) reg [31:0] a_pre, b_pre, c_pre; + wire [31:0] a_in, b_in, c_in; + // assuming 8/24 + assign a_in[31:22] = a_pre[31:22]; + assign b_in[31:22] = b_pre[31:22]; + assign a_in[21:0] = (a_pre[21:0] & 22'h042100) | (|(a_pre[21:0] & ~22'h042100) << 3); + assign b_in[21:0] = (b_pre[21:0] & 22'h380000) | (|(b_pre[21:0] & ~22'h380000) << 0); + assign c_in = c_pre; + + wire [31:0] a, b, c; + assign a = a_in & 32'hffc42108; + assign b = b_in & 32'hfff80001; + assign c = c_in & 32'hfff80001; +`else + (* anyconst *) reg [31:0] a, b, c; +`endif + (* anyseq *) reg [4:0] rm; reg [31:0] o; reg NV, DZ, OF, UF, NX; @@ -65,9 +89,14 @@ module edges(); wire o_norm = o_exp > 8'h00 && !o_special; wire o_subnorm = o_exp == 8'h00 && o_sig != '0; wire o_finite = o_norm || o_subnorm; - wire o_unclamped = o_finite && o_unsigned != 31'h7f7fffff; + wire o_clamped = o_unsigned == 31'h7f7fffff; + wire o_unclamped = o_finite && !o_clamped; wire o_ebmin = o_exp == 8'h01 && o_sig == '0; + (* keep *) wire [25:0] a_faux = {2'b10, !a_subnorm, a_sig}; + (* keep *) wire [25:0] b_faux = {2'b00, !b_subnorm, b_sig}; + (* keep *) wire [25:0] o_faux = (a_faux - b_faux); + `ifdef MULADD wire muladd_zero = c_zero; wire a_is_1 = a == 32'h3f800000; @@ -180,6 +209,93 @@ module edges(); c_sig == '0; always @* begin + // all classes of input are possible (for all inputs) + cover (a_sign); + cover (!a_sign); + cover (a_zero); + cover (a_norm); + cover (a_subnorm); + cover (a_inf); + cover (a_qnan); + cover (a_snan); + + cover (b_sign); + cover (!b_sign); + cover (b_zero); + cover (b_norm); + cover (b_subnorm); + cover (b_inf); + cover (b_qnan); + cover (b_snan); + +`ifdef MULADD + cover (c_sign); + cover (!c_sign); + cover (c_zero); + cover (c_norm); + cover (c_subnorm); + cover (c_inf); + cover (c_qnan); + cover (c_snan); +`endif + + // all flags are possible + cover (NV); +`ifdef DIV + // only div can div/zero + cover (DZ); +`endif + cover (OF); +`ifndef ADDSUB + // add/sub can't underflow + cover (UF); +`endif + cover (NX); + cover (!NV); + cover (!DZ); + cover (!OF); + cover (!UF); + cover (!NX); + + // all classes of output are possible + cover (o_sign); + cover (!o_sign); + cover (o_zero); + cover (o_norm); + cover (o_subnorm); + cover (o_inf); + cover (o_nan); + cover (o_ebmin); + + if (OF) begin + cover (o_inf); + cover (o_clamped); + end else begin + cover (o_inf); + cover (o_clamped); + end + + if (UF) begin +`ifndef ADDSUB + cover (o_zero); + cover (o_ebmin); + cover (o_subnorm); +`endif + end else begin + cover (o_zero); + cover (o_ebmin); + cover (o_subnorm); + end + + if (NX) begin + cover (o_norm); + cover (o_inf); +`ifndef ADDSUB + cover (o_subnorm); + cover (o_zero); +`endif + end + if (a_nan || b_nan || c_nan) begin // input NaN = output NaN assert (o_nan); @@ -252,6 +368,11 @@ module edges(); // an unrounded result between +-e^bmin is still an underflow when rounded to ebmin if (a_unsigned == 31'h0031b7be && b_unsigned == 31'h3ec6def9) assert (UF); + `ifdef ALT_DIV + if (!NV && !NX && !a_special && b_finite && o_norm) + // if o is subnorm then it can be shifted arbitrarily depending on exponent difference + assert (o_sig == (o_faux[25] ? o_faux[24:2] : o_faux[23:1])); + `endif `endif `ifdef MUL @@ -428,6 +549,55 @@ module edges(); if (a_sign && (a_norm || a_subnorm)) assert (NV); `endif + end + reg skip = 1; + always @(posedge clk) begin + if (skip) begin + skip <= 0; + end else begin + // same input, different rounding mode + if ($stable(a) && $stable(b) && $stable(c)) begin + // inf edge cases + cover ($rose(o_inf)); + if ($rose(o_inf)) begin + cover ($rose(rm_RNE)); + cover ($rose(rm_RNA)); + cover ($rose(rm_RTN)); + cover ($rose(rm_RTP)); + // rm_RTZ can never round to inf + end + +`ifndef ADDSUB + // these aren't applicable to addsub since we they rely on underflow + // ebmin edge cases + cover ($rose(o_ebmin)); + if ($rose(o_ebmin)) begin + cover ($rose(rm_RNE)); + cover ($rose(rm_RNA)); + cover ($rose(rm_RTN)); + cover ($rose(rm_RTP)); + cover ($rose(rm_RTZ)); + end + + // zero edge cases + cover ($rose(o_zero)); + if ($rose(o_zero)) begin + cover ($rose(rm_RNE)); + cover ($rose(rm_RNA)); + cover ($rose(rm_RTN)); + cover ($rose(rm_RTP)); + cover ($rose(rm_RTZ)); + end +`endif + +`ifndef DIV + cover ($rose(OF)); +`endif +`ifdef TININESS_AFTER + cover ($rose(UF)); +`endif + end + end end endmodule \ No newline at end of file diff --git a/tests/symfpu/run-test.sh b/tests/symfpu/run-test.sh index 36db8f395..b262c26af 100755 --- a/tests/symfpu/run-test.sh +++ b/tests/symfpu/run-test.sh @@ -19,6 +19,7 @@ chformal -remove opt read_verilog -sv -formal $defs -D${rm} edges.sv +chformal -remove -cover chformal -lower prep -top edges -flatten sat -set-assumes -prove-asserts -verify