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 firstname.lastname@example.org.