• The LGSynth93 benchmark set. Includes circuits from LGSynth91, ISCAS89 and ISCAS85.

  • The archives of benchmark descriptions and posted solutions to NP-hard problems.
    Includes BDD benchmarks

  • The Texas-97 Verification Benchmarks for VIS.

  • Miroslav N. Velev provides several challenging CNF benchmark sets. The suites were generated in the formal verification of superscalar and VLIW microprocessors.

  • Here Miroslav N. Velev provides new significantly more complex benchmarks. The instances were generated in the formal verification of liveness of single-issue pipelined and dual-issue superscalar processors.

  • Here you find an evaluation study of the LGSynth93 benchmark set. The evaluation consists of combinatorial and sequential experiments.


If you know of material that should be linked here or publish such material yourself, please contact the maintainer of these pages.