
Verification of Benchmarks 17 and 22 of the IFIP WG10.5
Benchmark Circuit Suite
S. Hazelhurst and C.J. H. Seger
Integrated Systems Design Laboratory
Department of Computer Science
University of British Columbia
Vancouver, B.C., Canada V6T 1Z4
5 October 1995
Abstract
This paper reports on the verification of two of the IFIP WG10.5 benchmarks  the multiplier
and systolic matrix multiplier. The circuit implementations are timed, detailed gatelevel
descriptions, and the specification is given using the temporal logic TLn, a quaternaryvalued
temporal logic. A practical, integrated theoremproving/model checking system based on the
compositional theory for TLn and symbolic trajectory evaluation is used to verify the circuits. A
64bit version of multiplier circuit (Benchmark 17) containing approximately 28 000 gates takes
about 18 minutes of computation time to verify. A 4 ? 4, 32bit version of the matrix multiplier
(Benchmark 22) containing over 110 000 gates take about 170 minutes of computation time to
verify. A significant timing error was discovered in this benchmark.
Keywords: symbolic trajectory evaluation, benchmarks, compositional verification, temporal
logic, theorem proving.
1 Introduction
The IFIP WG10.5 Benchmark Circuit suite [3] is a suite of circuits designed to allow comparison between different verification sites. Descriptions of the circuits are available [7].
This paper reports on the verification of two circuits of the IFIP WG10.5 suite  one is a multiplier circuit, the other is a systolic matrix multiplier circuit  using a method of verification developed in the ISD Laboratory at the University of British Columbia. As this work is part of a larger project, this is a descriptive report of experiments undertaken. It is not a selfcontained report and readers unfamiliar with symbolic trajectory evaluation will need the fuller account of the theory and discussion of the relationship to other work that can be found in work cited later. Much of the work. reported here forms the basis of the first author's PhD research.
Section 2 briefly describes the theoretical basis of the work. Section 3 describes the verification of Benchmark 17 (the multiplier) and Section 4 describes the verification of Benchmark 22 (the
This research was supported by operating grant OGPO 109688 from the Natural Sciences and Engineering Research Council of Canada, a fellowship from the B.C. Advanced Systems Institute, and by equipment grants from Sun Microsystems Canada Ltd. and Digital Equipment of Canada Ltd.