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

Markus Wedler; Dominik Stoffel; Wolfgang Kunz

doi:10.1109/DATE.2003.10119

Design, Automation & Test in Europe Conference & Exhibition

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

Year: 2003, Volume: 2, Pages: 11156

DOI Bookmark: 10.1109/DATE.2003.10119

Authors

Markus Wedler, University of Kaiserslautern
Dominik Stoffel, University of Kaiserslautern
Wolfgang Kunz, University of Kaiserslautern

Abstract

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.

Like what you’re reading?

Already a member?

Get this article FREE with a new membership!

Using RTL statespace information and state encoding for induction based property checking
Design, Automation & Test in Europe Conference & Exhibition
Learning from constraints for formal property checking
2009 IEEE International High Level Design Validation and Test Workshop
Exploiting state encoding for invariant generation in induction-based property checking
Asia and South Pacific Design Automation Conference
Using RTL statespace information and state encoding for induction based property checking
Design, Automation & Test in Europe Conference & Exhibition
Exploiting state encoding for invariant generation in induction-based property checking
ASP-DAC 2004: Asia and South Pacific Design Automation Conference 2004
Exploiting State Encoding for Invariant Generation in Induction-Based Property Checking
Asia and South Pacific Design Automation Conference
Explicit Safety Property Strengthening in SAT-based Induction
2007 20th International Conference on VLSI Design
Using RTL statespace information and state encoding for induction based property checking
Design, Automation & Test in Europe Conference & Exhibition
A K-Induction Method Extended with Value Analysis for C Program Safety Verification
2022 IEEE International Conference on Trust, Security and Privacy in Computing and Communications (TrustCom)
Encoding Induction Proof in Dafny
2021 International Symposium on Theoretical Aspects of Software Engineering (TASE)

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

Authors

Abstract

Related Articles