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
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;
Conference_Titel :
Design, Automation and Test in Europe Conference and Exhibition, 2003
Print_ISBN :
0-7695-1870-2
DOI :
10.1109/DATE.2003.1253779
