Inductive Verification of Sequential Circuits with a Datapath

V
VLSID
1997
Tenth International Conference on VLSI Design: VLSI in Multimedia Applications
Abstract - Inductive Verification of Sequential Circuits with a Datapath

	This Article
	Subscribers, please Login Purchase article: $19 PDF IEEE Xplore Subscribers RSS feed
	Share
	Email this Article to a friend
	Bibliographic References
	ASCII Text BibTex RefWorks Procite/RefMan
	Add to:
	Digg Furl Spurl Blink Simpy Google Del.icio.us Y!MyWeb
	Search
	Similar Articles Articles by I. Chakrabarti Articles by D. Sarkar Articles by A. K. Majumdar

Tenth International Conference on VLSI Design: VLSI in Multimedia Applications

Hyderabad, India

January 04-January 07

ISBN: 0-8186-7755-4

	ASCII Text	x
	I. Chakrabarti, D. Sarkar, A. K. Majumdar, "Inductive Verification of Sequential Circuits with a Datapath," VLSI Design, International Conference on, pp. 226, Tenth International Conference on VLSI Design: VLSI in Multimedia Applications, 1997.

	BibTex	x
	@article{ 10.1109/ICVD.1997.568080, author = {I. Chakrabarti and D. Sarkar and A. K. Majumdar}, title = {Inductive Verification of Sequential Circuits with a Datapath}, journal ={VLSI Design, International Conference on}, volume = {0}, year = {1997}, issn = {1063-9667}, pages = {226}, doi = {http://doi.ieeecomputersociety.org/10.1109/ICVD.1997.568080}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }

	RefWorks Procite/RefMan/Endnote	x
	TY - CONF JO - VLSI Design, International Conference on TI - Inductive Verification of Sequential Circuits with a Datapath SN - 1063-9667 SP EP A1 - I. Chakrabarti, A1 - D. Sarkar, A1 - A. K. Majumdar, PY - 1997 KW - finite state machine KW - theorem proving KW - hardware verification KW - backward reasoning KW - inductive reasoning KW - data and control paths KW - data invariant. VL - 0 JA - VLSI Design, International Conference on ER -

I. Chakrabarti, Indian Institute of Technology

D. Sarkar, Indian Institute of Technology

A. K. Majumdar, Indian Institute of Technology

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ICVD.1997.568080

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.

Index Terms:

finite state machine, theorem proving, hardware verification, backward reasoning, inductive reasoning, data and control paths, data invariant.

Citation:

I. Chakrabarti, D. Sarkar, A. K. Majumdar, "Inductive Verification of Sequential Circuits with a Datapath," vlsid, pp.226, Tenth International Conference on VLSI Design: VLSI in Multimedia Applications, 1997

Peer Review Notice | Give Us Feedback

Usage of this product signifies your acceptance of the Terms of Use.