Abstract :
The paper presents a collection of 20 benchmark suites with a total of 1,132 ISCAS Boolean formulas from formal verification of high-level microprocessors, including pipelined, superscalar, and VLIW models with exceptions, multicycle functional units, branch prediction, instruction queues, and register renaming. These benchmarks can be used in research on testing, logic synthesis and optimization, equivalence verification, decision diagrams, and Boolean satisfiability. The most complex formulas have more than 700,000 logic gates.
Keywords :
Boolean algebra; computability; decision diagrams; formal verification; high level synthesis; instruction sets; logic testing; microprocessor chips; pipeline processing; Boolean satisfiability; ISCAS Boolean formulas; ISCAS benchmarks; VLIW models; branch prediction; decision diagrams; equivalence verification; formal verification; high-level microprocessors; instruction queues; logic gates; logic synthesis; multicycle functional units; pipelined models; register renaming; superscalar models; testing; Benchmark testing; Boolean functions; Computer bugs; Formal verification; Logic gates; Logic testing; Microprocessors; Predictive models; Safety; VLIW;
