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
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;
Conference_Titel :
Design Automation Conference, 2004. Proceedings of the ASP-DAC 2004. Asia and South Pacific
Print_ISBN :
0-7803-8175-0
DOI :
10.1109/ASPDAC.2004.1337612
