Using RTL Statespace Information and State Encoding for Induction Based Property Checking

This paper focuses 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.

• Type: Conference
• Year: 2003
• Where: DATE
• Authors: Markus Wedler, Dominik Stoffel, Wolfgang Kunz
• Keywords: DATE 2003, Hardware, Induction-based Property Checking, Sequential Circuits, State Encoding