Title :
Mechanical identification of inductive properties during verification of finite state machines
Author :
Chakrabarti, I. ; Sarkar, D.
Author_Institution :
Dept. of Comput. Sci. & Eng., Indian Inst. of Technol., Kharagpur, India
Abstract :
This paper describes a method to verify a finite state machine by theorem proving. For some instances, inductive reasoning comes in handy to support the proof of verification. In this work the theorem prover itself tries to find out the properties on which induction needs to be applied. A short account of the proof procedure which is based on goal directed backward reasoning is given. A nontrivial example is presented to illustrate the approach. A proof construction algorithm has been provided
Keywords :
encoding; finite state machines; logic design; sequential circuits; sequential switching; theorem proving; FSM verification; finite state machines; goal directed backward reasoning; inductive properties; mechanical identification; proof construction algorithm; theorem proving; Algorithm design and analysis; Automata; Computer science; Encoding; Hardware; Integrated circuit interconnections; Logic; Mechanical factors; Sequential circuits; Very large scale integration;
Conference_Titel :
VLSI Design, 1994., Proceedings of the Seventh International Conference on
Conference_Location :
Calcutta
Print_ISBN :
0-8186-4990-9
DOI :
10.1109/ICVD.1994.282725
