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.
['Markus Wedler', 'Dominik Stoffel', 'Wolfgang Kunz']
Using RTL Statespace Information and State Encoding for Induction Based Property Checking