Submit 992-LUT size candidate for voter

[chengxuandi]

This PR submits a size candidate for the EPFL voter benchmark.

File:

• best_results/size/voter_size_2027.blif
  • LUT-6 count: 992
  • depth: 40 levels

Interface:

• .model top
• inputs A[0] through A[1000]
• output maj

Verification:

• ABC successfully reads the submitted BLIF and reports 992 LUT nodes at 40 levels.
• All 992 nontrivial nodes have fan-in at most 6; the network has 1001 inputs, one output, and no latches.
• Functional equivalence to random_control/voter.blif was established by a complete compositional formal proof. ABC CEC proves all 1000 adjacent-input transposition obligations for the official reference; exact evaluation of all 1002 Hamming-weight classes establishes that the reference is the threshold function [sum(A) >= 501]. An independent checker exhaustively verifies the submitted LUT truth tables as an exact counting network implementing the same threshold. Named and positional ABC CEC both pass between the generated parent and the submitted mapped BLIF.

Method:

The implementation reconstructs the proved voter threshold function as a LUT6-oriented counting network. Six-input equal-weight counters compress a weighted bit heap, and the output detects overflow corresponding to the 501-of-1001 threshold. The submitted network is a constructive implementation of the same Boolean function; it was not produced by changing the benchmark specification or using don't-cares.

Environment:

• EPFL benchmark repository commit: 82d8cc6910419298e713a46644ed59fd3df53038
• ABC version: 1.01
• ABC commit: c798fea440d9879a1ae79c3f71936d0bc8103e4d
• LUT mapping flow used to produce the submitted artifact: read_blif raw_candidate.blif; strash; if -K 6; print_stats -c; write_blif voter_992.blif

Submitted by CHENG XUANDI, Lanzhou Jiaotong University.