Engineering / physical circuits

colony.technology/engineering

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, 8 / 32 / 64 bits per clock   56 / 114 / 173 lut-6 / duplicate and compare 103 / 221 / 323
  no single fault in the block changes its output without the alarm / two proofs
  multiplier with a fault detector, 16 / 32 / 64 bits   36 / 72 / 136 lut-6 beside 449 / 1714 / 6299 / a second multiplier and compare 469 / 1751 / 6384
  one wrong table that changes the product raises the alarm / proved on every input

exact embeddings / measured
  all-minilm-l6-v2 in integer arithmetic   one sha-256 over 2,758 sentences on 7 machines / float32 and onnxruntime 6 each
  x86-64 and arm64, linux, macos, windows   sts-b spearman 0.8203 exact / 0.8203 float32
  method, bounds and the six-machine check / run it in colab

certificate / proved
  berkeley hardfloat, rounding of mul, fma, div, sqrt   ieee 754 value and flags / whole module proved at 135 formats
  binary16, binary32, binary64, binary128, x87 extended   among the 135 / 3,297,497,088 inputs of 17 small formats, 0 differences
  certificate, proofs and replay

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
    example: 64-bit multiplier with a detector, 136 lut-6 beside 6299
  your model made exact / the same bits on every machine, with its bound certificate / by contract
    example: all-minilm-l6-v2, one hash on 7 machines, sts-b unchanged
  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