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 gate-level descriptions, and the specification is given using the temporal logic TLn, a quaternary-valued temporal logic. A practical, integrated theorem-proving/model checking system based on the compositional theory for TLn and symbolic trajectory evaluation is used to verify the circuits. A 64-bit version of multiplier circuit (Benchmark 17) containing approximately 28 000 gates takes about 18 minutes of computation time to verify. A 4 ? 4, 32-bit 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 self-contained 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.