Verification of Benchmarks 17 and 22 of the IFIP WG10.5 Benchmark Circuit Suite

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 \Theta 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..