loading...
Inductive Verification of Sequential Circuits with a Datapath
Hyderabad, India January 04-January 07
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ICVD.1997.568080Tenth International Conference on VLS ...
 This Article 
 
Buy PURCHASE ARTICLE: $19
PDF
HTML
Buy IEEE Xplore Subscribers
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
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
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
Usage of this product signifies your acceptance of the Terms of Use.