Technical Reports

The ICICS/CS Reading Room

UBC CS TR-95-21 Summary

Verification of Benchmarks 17 and 22 of the IFIP WG10.5 Benchmark Circuit Suite, October 1995 Scott Hazelhurst and Carl J. H. Seger, 32 pages

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 by 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.

If you have any questions or comments regarding this page please send mail to