loading...
Using RTL Statespace Information and State Encoding for Induction Based Property Checking
Munich, Germany March 03-March 07
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/DATE.2003.10119Design, Automation and Test in Europe ...
 This Article 
 
PURCHASE ARTICLE: $0
HTML
IEEE Xplore Subscribers
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
ASCII Text
x 
 
Markus Wedler, Dominik Stoffel, Wolfgang Kunz, "Using RTL Statespace Information and State Encoding for Induction Based Property Checking," Design, Automation and Test in Europe Conference and Exhibition, vol. 1, pp. 11156, Design, Automation and Test in Europe Conference and Exhibition (DATE'03), 2003.
 
 
BibTex
x
 
@article{ 10.1109/DATE.2003.10119,
author = {Markus Wedler and Dominik Stoffel and Wolfgang Kunz},
title = {Using RTL Statespace Information and State Encoding for Induction Based Property Checking},
journal ={Design, Automation and Test in Europe Conference and Exhibition},
volume = {1},
year = {2003},
issn = {1530-1591},
pages = {11156},
doi = {http://doi.ieeecomputersociety.org/10.1109/DATE.2003.10119},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Design, Automation and Test in Europe Conference and Exhibition
TI - Using RTL Statespace Information and State Encoding for Induction Based Property Checking
SN - 1530-1591
SP
EP
A1 - Markus Wedler,
A1 - Dominik Stoffel,
A1 - Wolfgang Kunz,
PY - 2003
KW - null
VL - 1
JA - Design, Automation and Test in Europe Conference and Exhibition
ER -
 
Markus Wedler, University of Kaiserslautern
Dominik Stoffel, University of Kaiserslautern
Wolfgang Kunz, University of Kaiserslautern
This paper focuses on checking safety properties for sequential circuits specified on the RT-level. We study how different state encodings can be used to create a gate-level representation of the circuit that facilitates the computation of effective invariants for induction-based property checking. Our experiments show the strong impact of state encoding on the efficiency of the induction process.
Citation:
Markus Wedler, Dominik Stoffel, Wolfgang Kunz, "Using RTL Statespace Information and State Encoding for Induction Based Property Checking," date, vol. 1, pp.11156, Design, Automation and Test in Europe Conference and Exhibition (DATE'03), 2003
Usage of this product signifies your acceptance of the Terms of Use.