A new generation of ISCAS benchmarks from formal verification of high-level microprocessors

Author

Velev, Miroslav N.

Volume

5

fYear

2004

fDate

23-26 May 2004

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Circuits and Systems, 2004. ISCAS '04. Proceedings of the 2004 International Symposium on

Print_ISBN

0-7803-8251-X

Type

conf

DOI

10.1109/ISCAS.2004.1329500

Filename

1329500