Exploiting state encoding for invariant generation in induction-based property checking

— This paper focuses on checking safety properties for sequential circuits specified on the RTlevel. 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: 2004
• Where: ASPDAC
• Authors: Markus Wedler, Dominik Stoffel, Wolfgang Kunz
• Keywords: ASPDAC 2004, Different State Encodings, Induction-based Property Checking, State Encoding