@inproceedings{299c56e877e347a8b28a2e05436c7fea,
title = "Formal verification of serial pipeline multipliers",
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.",
author = "Kim, {Jang Dae} and Chin, {Shiu Kai}",
note = "Publisher Copyright: {\textcopyright} 1995, Springer-Verlag. All rights reserved.; 8th International Workshop on Higher Order Logic Theorem Proving and its Applications, 1995 ; Conference date: 11-09-1995 Through 14-09-1995",
year = "1995",
doi = "10.1007/3-540-60275-5_68",
language = "English (US)",
isbn = "3540602755",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "229--244",
editor = "Schubert, {E. Thomas} and Windley, {Phillip J.} and James Alves-Foss",
booktitle = "Higher Order Logic Theorem Proving and Its Applications - 8th International Workshop, Proceedings",
}