engineering / physical circuits arithmetic rtl / state machines logic / switching / storage power / area / timing communication / dependable control ᑕ. / mathematical operators retained boundary state exact interval composition carry frontiers / affine costs definitions and proofs speedrunpapi / current interfaces math 18 bounded exact operators onnx closed cpu / bit-exact plans r1cs output determinism / v0.7.2 rtl circuit blocks / measured on the target capabilities / json threshold networks / measured epfl voter, 1001 inputs 987 lut-6 / published best 1145 depth build 9 levels / published best 11 epfl arbiter, 128 requests 256 lut-6 / published best 259, equations and check ecp5, 64-input detector 8.76 ns, 139 cells / plain rtl 12.87 ns, 271 source, netlists and proofs arithmetic / measured epfl multiplier, 64 x 64 3420 lut-6 / published best 4282 epfl square, 64-bit 2421 lut-6 / published best 2894 epfl sqrt, 128-bit 2174 lut-6 / published best 2958 epfl hyp, 128-bit sides 24436 lut-6 / published best 36451 epfl div, 64 / 64 2287 lut-6 / published best 3082 epfl sin, 24-bit 685 lut-6 / published best 994, formula and check epfl log2, 32-bit 4099 lut-6 / published best 5986, formula and check multiplier, depth 11 levels / published best 25 square, depth 10 levels, 3358 lut-6 / published best 10, 3690 div, depth 58 levels, 20232 lut-6 / published best 170, 30849 log2, depth 23 levels, 7978 lut-6 / published best 51, 9391 log2, ecp5 placed 47.8 ns, 21171 cells / published best 105.9 ns, 24254 independent proof 0.3 s to 6 s per circuit source, netlists and proofs epfl mtm / measured sixteen, 16.2 million gates 12691 lut-6 / published best 3282958 twenty, 20.7 million gates 12719 lut-6 / published best 4166467 twentythree, 23.3 million gates 12744 lut-6 / published best 470892 sixteen, depth 9 levels, 407332 lut-6 / published best 14 levels, 3387001 one fibonacci loop in 64-bit integers, written out as a truth table proof of equivalence no solver, 9 minutes for the three netlists, rule and proof iwls contest / measured ex290, 12 inputs 519 and nodes / best of twelve teams 2868 ex292, 14 inputs 605 and nodes / best of twelve teams 5557 ex294, 16 inputs 683 and nodes / best of twelve teams 8383 ex296, 13 inputs 1067 and nodes / best of twelve teams 6217 ex298, 15 inputs 1459 and nodes / best of twelve teams 21553 ex299, 16 inputs 2056 and nodes / best of twelve teams 15410 functions given as truth tables only; the rule recovered, the circuit built from it rules and circuits for twenty functions 2025 contest, ex161, 8-bit float multiply 303 and nodes / best of four teams 2327 2025 contest, ex162, 8-bit float divide 554 and nodes / best of four teams 2850 2025 contest, ex183, half-precision square 686 and nodes / best of four teams 2245 2025 contest, ex185, half-precision root 642 and nodes / best of four teams 2277 rules for twenty-six functions, eleven circuits secure computation / and gates, xor free ieee double square root 2013 / bristol fashion 91504 ieee double divide 4559 / bristol fashion 82269 ieee double multiply 5218 / bristol fashion 19626 ieee double add 1447 / bristol fashion 5385 ten float circuits 15704 / bristol fashion 204664 64 x 64 multiply 5272 / bristol fashion 8128 nine proved equivalent with abc; add, multiply, divide, root on 1,000,000,000 operands against the processor sixteen circuits in the same file format, and the check linear logic / measured crc-32, 512-bit bus 701 lut-6, 4 levels / yosys 2344 crc-32, 1024-bit bus 1214 lut-6, 5 levels / yosys 4662 crc-32, 64 bytes, any length 1172 lut-6 rs(544,514) encoder, 4 symbols 783 lut-6 / yosys 2576 ecp5, 64-bit bus, placed 227 cells, 5.70 ns / xor equations 531, 5.64 ns source, netlists and proofs crc-32 frame check, 8 / 32 / 64 bits per clock 41 / 100 / 151 lut-6, each proved on every input verification evidence for do-254 and iso 26262 applicants crc-32 frame check with a fault detector, 64 bits per clock 173 lut-6 / duplicate and compare 323 no single fault in the block changes its output without the alarm / two proofs divider module / measured ecp5, 64-bit, placed 4889 cells, 292 ns / yosys operators 12246, 394 ns xilinx 7, 64-bit, synth 2352 lut / yosys operators 4215 ecp5, 64-bit, udivf 181 ns, 5161 cells, 49 mult / yosys operators 394 ns cyclone v, 64-bit, quartus 160 ns, 1866 alms, 35 dsp / quartus operators 248 ns, 5094 alms rtl module and sat proof arithmetic audit / open cores dawsonjon/fpu, double divide 2^29 times the quotient, subnormal band / fix filed dawsonjon/fpu, double to float 1 - 2^-53 converts to 0.5 / fix filed or1200 fpu, multiply twice the product, subnormal operand opencores fpu inf * -inf returns nan basejump stl fpu, add 0 + 0 returns the smallest normal number / fix filed lowrisc muntjac fpu, fma the 106-bit product loses its last bit / reported neorv32 fpu, float to integer 0.5 + 2^-24 converts to 0 / fix merged upstream mor1kx, marocchino fpu overflow returns inf in the directed rounding modes / reported marocchino fpu 1/0, then 1+1 returns inf / reported openhw cvfpu, bfloat16 divide a quotient below 2^-134 returns zero, no flags / cause and fix filed openhw cvfpu, narrowing add 0 + 2^-129 returns 2^127 / reported openhw cva5 fpu, divide 0.0 / 2.0 right after another divide never returns / cause and fix filed openhw cva5 fpu, square root inexact roots returned as exact, 29-bit roots / cause and fix filed gaisler noel-v fpu, multiply 3.0 * 5.0 - 15.0 returns 1.65e-24 after a mispredicted branch / cause and fix sent gaisler noel-v fpu, fma 16 - (1 + 2^-52)(1 - 2^-52) rounds up to exactly 15 / cause and fix sent ieee vhdl float_pkg, sqrt sqrt(2.0) in double precision is one unit off / cause and patch sent ieee vhdl float_pkg, mac (-6)(-1) + (-5) returns -15 / cause and patch sent ieee vhdl float_pkg, resize the double 2^-512 converts to 1.0 in single / cause and patch sent blackparrot, integer to float a 64-bit integer converted to single is rounded twice / fix filed microwatt fpu, enabled underflow a result that rounds up is classed as denormalized / cause and fix filed siemens ac_std_float, fma with ties to odd, a tie under a power of two returns twice the result / cause and fix filed siemens ac_std_float, add 1.0 minus a far smaller number is one unit low at four fraction widths / cause and fix filed siemens ac_std_float, ceil ceil(-0.5) returns +0 where the c library returns -0 / cause and fix filed siemens ac_std_float, convert the largest subnormal of binary32 becomes zero in bfloat16's layout / cause and fix filed siemens ac_std_float, from int 4294967295 with ties to odd converts to zero / cause and fix filed siemens ac_math, fixed divide 0.5 / 3 into an integer type leaves the output unwritten / cause and fix filed llvm apfloat, multiply (1 - 2^-53) * 2^-1022 rounds up to the smallest normal number with no underflow status / reported, patch published google xls apfloat, fma a nan operand returns infinity on the e4m3 and e5m2 layouts / cause and fix filed google xls apfloat, from int 100000 to half precision, rounding toward zero, returns infinity / reported t-head e906, c906, c910 0 wrong values in 1.1 million vectors per operation results and reproducers one arithmetic block / 1,800 usd crc, divider, voter, correlator, popcount-threshold, squarer compiled for your fpga family, measured in your flow against your rtl delivered: lut netlist (.v), proof files with an independent checker, comparison sheet full refund if it does not beat your reference on lut count or logic depth evidence package for one block / 1,800 usd the block proved on every input, a second proof by an unrelated tool, simulation, known answers one page in the terms of do-254 or iso 26262: what the evidence covers, what stays with the applicant example: crc-32 frame check block with a fault detector and its proof / 4,800 usd the detector beside your block: check bits predicted from the inputs, computed again from the output, an alarm when they differ proved by two unrelated methods: no single fault in the block changes its output without the alarm example: crc-32 with a detector, 173 lut-6 against 323 for duplicate and compare larger work / by contract a block is accepted on reference source / target library independent functional check synthesis / placement / activity measured physical result proofs results colony