DocumentCode
2412952
Title
Using RTL statespace information and state encoding for induction based property checking
Author
Wedler, Markus ; Stoffel, Dominik ; Kunz, Wolfgang
Author_Institution
Dept. of Electr. Eng. & IT, Kaiserslautern Univ., Germany
fYear
2003
fDate
2003
Firstpage
1156
Lastpage
1157
Abstract
This paper focuses on checking safety properties of 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.
Keywords
finite state machines; formal verification; invariance; logic design; logic testing; sequential circuits; state-space methods; RTL state space information; circuit gate-level representation; effective invariants computation; finite state machine; induction based property checking; safety properties checking; sequential circuits; state encoding; verification; Automata; Automatic control; Design automation; Encoding; Hardware design languages; Induction generators; Safety; Sequential circuits; Upper bound;
fLanguage
English
Publisher
ieee
Conference_Titel
Design, Automation and Test in Europe Conference and Exhibition, 2003
ISSN
1530-1591
Print_ISBN
0-7695-1870-2
Type
conf
DOI
10.1109/DATE.2003.1253779
Filename
1253779
Link To Document