Using RTL Statespace Information and State Encoding for Induction Based Property Checking

	This Article
	PDF RSS feed
	Share
	Email this Article to a friend
	Bibliographic References
	ASCII Text BibTex RefWorks Procite/RefMan/Endnote
	Add to:
	Digg Furl Spurl Blink Simpy Google Del.icio.us Y!MyWeb
	Search
	Similar Articles Articles by Markus Wedler Articles by Dominik Stoffel Articles by Wolfgang Kunz

Design, Automation and Test in Europe Conference and Exhibition (DATE'03)

Using RTL Statespace Information and State Encoding for Induction Based Property Checking (PDF)

Munich, Germany

March 03-March 07

ISBN: 0-7695-1870-2

	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

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/DATE.2003.10119

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

Peer Review Notice | Give Us Feedback

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