DocumentCode
1945071
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
fYear
1997
fDate
4-7 Jan 1997
Firstpage
226
Lastpage
231
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;
fLanguage
English
Publisher
ieee
Conference_Titel
VLSI Design, 1997. Proceedings., Tenth International Conference on
Conference_Location
Hyderabad
ISSN
1063-9667
Print_ISBN
0-8186-7755-4
Type
conf
DOI
10.1109/ICVD.1997.568080
Filename
568080
Link To Document