Title :
Formal verification of state-machines using higher-order logic
Author :
Loewenstein, Paul N.
Author_Institution :
Nat. Semicond. Corp., Santa Clara, CA, USA
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;
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
DOI :
10.1109/ICCD.1989.63356
