DocumentCode
3474360
Title
Exploiting state encoding for invariant generation in induction-based property checking
Author
Wedler, Markus ; Stoffel, Dominik ; Kunz, Wolfgang
Author_Institution
Dept. of Electr. & Comput. Eng., Kaiserslautern Univ., Germany
fYear
2004
fDate
27-30 Jan. 2004
Firstpage
424
Lastpage
429
Abstract
We focus 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.
Keywords
finite state machines; logic CAD; safety; sequential circuits; gate-level circuit representation; induction-based property checking; sequential circuit safety property checking; state encoding; Automata; Counting circuits; Design automation; Electrical safety; Encoding; Explosions; Induction generators; Sequential circuits; Sufficient conditions; Upper bound;
fLanguage
English
Publisher
ieee
Conference_Titel
Design Automation Conference, 2004. Proceedings of the ASP-DAC 2004. Asia and South Pacific
Print_ISBN
0-7803-8175-0
Type
conf
DOI
10.1109/ASPDAC.2004.1337612
Filename
1337612
Link To Document