IChecker: An efficient checker for inductive invariants

Feng Lu; K. T. Cheng

doi:10.1109/HLDVT.2006.319987

IChecker: An efficient checker for inductive invariants

Feng Lu^*, K. T. Cheng

^*Corresponding author for this work

Research output: Chapter in Book/Conference Proceeding/Report › Conference Paper published in a book › peer-review

11 Citations (Scopus)

Abstract

Invariants in sequential circuits could be very useful for sequential optimizations and for speeding up functional verification tasks. However, the lack of efficient and scalable invariant identification tools limits their usage. In this paper, we present a new tool, IChecker, for efficient identification of true invariants for any given initial, set of invariant candidates. ICheker uses new circuit simplification techniques to iteratively minimize constrained circuit models, along with a number of heuristics for efficient computation of invariants. Experimental results demonstrate the high efficiency and effectiveness of the proposed approach for identifying sequential invariants.

Original language	English
Title of host publication	Proceedings - 11th Annual IEEE International High-Level Design Validation and Test Workshop, HLDVT'06
Pages	176-180
Number of pages	5
DOIs	https://doi.org/10.1109/HLDVT.2006.319987
Publication status	Published - 2006
Externally published	Yes
Event	11th Annual IEEE International High-Level Design Validation and Test Workshop, HLDVT'06 - Monterey, CA, United States Duration: 8 Nov 2006 → 10 Nov 2006

Publication series

Name	Proceedings - IEEE International High-Level Design Validation and Test Workshop, HLDVT
ISSN (Print)	1552-6674

Conference

Conference	11th Annual IEEE International High-Level Design Validation and Test Workshop, HLDVT'06
Country/Territory	United States
City	Monterey, CA
Period	8/11/06 → 10/11/06

Access to Document

10.1109/HLDVT.2006.319987

Cite this

@inproceedings{6f647ccc9a3149de962a22ffb1aaa4ff,

title = "IChecker: An efficient checker for inductive invariants",

abstract = "Invariants in sequential circuits could be very useful for sequential optimizations and for speeding up functional verification tasks. However, the lack of efficient and scalable invariant identification tools limits their usage. In this paper, we present a new tool, IChecker, for efficient identification of true invariants for any given initial, set of invariant candidates. ICheker uses new circuit simplification techniques to iteratively minimize constrained circuit models, along with a number of heuristics for efficient computation of invariants. Experimental results demonstrate the high efficiency and effectiveness of the proposed approach for identifying sequential invariants.",

author = "Feng Lu and Cheng, \{K. T.\}",

year = "2006",

doi = "10.1109/HLDVT.2006.319987",

language = "English",

isbn = "142440679X",

series = "Proceedings - IEEE International High-Level Design Validation and Test Workshop, HLDVT",

pages = "176--180",

booktitle = "Proceedings - 11th Annual IEEE International High-Level Design Validation and Test Workshop, HLDVT'06",

note = "11th Annual IEEE International High-Level Design Validation and Test Workshop, HLDVT'06 ; Conference date: 08-11-2006 Through 10-11-2006",

}

Lu, F & Cheng, KT 2006, IChecker: An efficient checker for inductive invariants. in Proceedings - 11th Annual IEEE International High-Level Design Validation and Test Workshop, HLDVT'06., 4110086, Proceedings - IEEE International High-Level Design Validation and Test Workshop, HLDVT, pp. 176-180, 11th Annual IEEE International High-Level Design Validation and Test Workshop, HLDVT'06, Monterey, CA, United States, 8/11/06. https://doi.org/10.1109/HLDVT.2006.319987

IChecker: An efficient checker for inductive invariants. / Lu, Feng; Cheng, K. T.
Proceedings - 11th Annual IEEE International High-Level Design Validation and Test Workshop, HLDVT'06. 2006. p. 176-180 4110086 (Proceedings - IEEE International High-Level Design Validation and Test Workshop, HLDVT).

Research output: Chapter in Book/Conference Proceeding/Report › Conference Paper published in a book › peer-review

TY - GEN

T1 - IChecker

T2 - 11th Annual IEEE International High-Level Design Validation and Test Workshop, HLDVT'06

AU - Lu, Feng

AU - Cheng, K. T.

PY - 2006

Y1 - 2006

N2 - Invariants in sequential circuits could be very useful for sequential optimizations and for speeding up functional verification tasks. However, the lack of efficient and scalable invariant identification tools limits their usage. In this paper, we present a new tool, IChecker, for efficient identification of true invariants for any given initial, set of invariant candidates. ICheker uses new circuit simplification techniques to iteratively minimize constrained circuit models, along with a number of heuristics for efficient computation of invariants. Experimental results demonstrate the high efficiency and effectiveness of the proposed approach for identifying sequential invariants.

AB - Invariants in sequential circuits could be very useful for sequential optimizations and for speeding up functional verification tasks. However, the lack of efficient and scalable invariant identification tools limits their usage. In this paper, we present a new tool, IChecker, for efficient identification of true invariants for any given initial, set of invariant candidates. ICheker uses new circuit simplification techniques to iteratively minimize constrained circuit models, along with a number of heuristics for efficient computation of invariants. Experimental results demonstrate the high efficiency and effectiveness of the proposed approach for identifying sequential invariants.

UR - https://openalex.org/W2056597596

UR - https://www.scopus.com/pages/publications/46249114044

U2 - 10.1109/HLDVT.2006.319987

DO - 10.1109/HLDVT.2006.319987

M3 - Conference Paper published in a book

SN - 142440679X

SN - 9781424406791

T3 - Proceedings - IEEE International High-Level Design Validation and Test Workshop, HLDVT

SP - 176

EP - 180

BT - Proceedings - 11th Annual IEEE International High-Level Design Validation and Test Workshop, HLDVT'06

Y2 - 8 November 2006 through 10 November 2006

ER -

IChecker: An efficient checker for inductive invariants

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this