Formal verification of serial pipeline multipliers

Jang Dae Kim, Shiu Kai Chin

Research output: Chapter in Book/Entry/PoemConference contribution


Serial data-path circuits are often more difficult to analyze than their parallel counterparts. The major reason is data and operations are spread over time. Here the strength of formal verification is demonstrated with verification of classical serial pipeline multipliers. The designer's informal notions of how to interpret the design are formally captured in well-defined functions and standard mathematical notation. A linear-time temporal logic is found to be useful for analyzing such circuits; temporal operators are succinct in expressing certain operating conditions that are otherwise verbose, and temporal laws and operators enable us to work more efficiently in a higher level of reasoning.

Original languageEnglish (US)
Title of host publicationHigher Order Logic Theorem Proving and Its Applications - 8th International Workshop, Proceedings
EditorsE. Thomas Schubert, Phillip J. Windley, James Alves-Foss
PublisherSpringer Verlag
Number of pages16
ISBN (Print)3540602755, 9783540602750
StatePublished - 1995
Event8th International Workshop on Higher Order Logic Theorem Proving and its Applications, 1995 - Aspen Grove, United States
Duration: Sep 11 1995Sep 14 1995

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other8th International Workshop on Higher Order Logic Theorem Proving and its Applications, 1995
Country/TerritoryUnited States
CityAspen Grove

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Formal verification of serial pipeline multipliers'. Together they form a unique fingerprint.

Cite this