Formal Property Checking Using Structural Circuit Transformations

Andreas Kuehlmann

Abstract

In this talk we discuss the application of structural circuit transformations for enhancing formal property checking. In the first part, we present the concept of generalized retiming for improving symbolic reachability analysis. We demonstrate that the classical definition of retiming can be generalized for verification by relaxing the notion of design equivalence and physical implementability. This includes (1) omitting the need for equivalent reset states by using an initialization stump, (2) supporting negative registers, handled by a general functional relation to future time frames, and (3) eliminating peripheral registers by converting them into simple temporal offsets. In the second part of the talk we present implementation details of the retiming approach using an AND/INVERTER/REGISTER graph model. In the last part we discuss a general tool architecture based on re-entrant transformation engines which can potentially decompose and solve verification problems that otherwise would be infeasible. We further give some outlook into current and future research in the area of transformation-based verification methods.