DocumentCode
1880996
Title
Formal verification of state-machines using higher-order logic
Author
Loewenstein, Paul N.
Author_Institution
Nat. Semicond. Corp., Santa Clara, CA, USA
fYear
1989
fDate
2-4 Oct 1989
Firstpage
204
Lastpage
207
Abstract
A description is given of the formalization of some state-machine theory in a higher-order logic (HOL) theorem prover and the results obtained applying that theory. It is shown that by building state-machine theory in HOL, the verification of state-machines is rendered much more tractable. This is illustrated using a family of redundantly encoded serial-parallel multipliers
Keywords
formal logic; logic testing; theorem proving; formal verification; higher-order logic; redundantly encoded serial-parallel multipliers; state-machines; theorem prover; Costs; Design engineering; Formal verification; Hardware; Logic design; Microprocessors; Power engineering and energy; Semiconductor device reliability; Sequential circuits; Switching circuits;
fLanguage
English
Publisher
ieee
Conference_Titel
Computer Design: VLSI in Computers and Processors, 1989. ICCD '89. Proceedings., 1989 IEEE International Conference on
Conference_Location
Cambridge, MA
Print_ISBN
0-8186-1971-6
Type
conf
DOI
10.1109/ICCD.1989.63356
Filename
63356
Link To Document