Title :
Inductive verification of sequential circuits with a datapath
Author :
Chakrabarti, I. ; Sarkar, D. ; Majumdar, A.K.
Author_Institution :
Dept. of Comput. Sci. & Eng., Indian Inst. of Technol., Kharagpur, India
Abstract :
A backward reasoning approach to verify a digital circuit is described. The proposed proof procedure is an augmentation of inductive reasoning over the states of a finite state machine. The augmentation addresses the issues related to reasoning with both the data and control paths of the circuit. The methodology has been illustrated with a lift controller example. Limitation of this proof approach is also identified
Keywords :
circuit analysis computing; finite state machines; formal verification; inference mechanisms; logic CAD; sequential circuits; theorem proving; backward reasoning approach; datapath; digital circuit verification; finite state machine; inductive verification; sequential circuits; Automata; Automatic control; Computer science; Control systems; Digital circuits; Digital systems; Hardware; Interconnected systems; Mechanical factors; Sequential circuits;
Conference_Titel :
VLSI Design, 1997. Proceedings., Tenth International Conference on
Conference_Location :
Hyderabad
Print_ISBN :
0-8186-7755-4
DOI :
10.1109/ICVD.1997.568080
