Formal verification of serial pipeline multipliers

Jang Dae Kim, Shiu Kai Chin

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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 publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
PublisherSpringer Verlag
Pages229-244
Number of pages16
Volume971
ISBN (Print)3540602755, 9783540602750
DOIs
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)
Volume971
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other8th International Workshop on Higher Order Logic Theorem Proving and its Applications, 1995
CountryUnited States
CityAspen Grove
Period9/11/959/14/95

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

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

Cite this