Preserving and Improving Verifiability of Circuits Based on Local Transformations

The concept of testability preserving or even testability improving circuit transformations has been studied intensively. It has been demonstrated for various fault models, that circuits can be optimized with respect to area and/or delay, while considering testability at the same time. Recently, Polynomial Formal Verification (PFV) has been introduced, where upper bounds on run time and space complexity of the algorithms - ensuring 100% correctness - are given. While the testability aspects were properties of the underlying circuits, here we propose a similar approach in the context of verification algorithms: verification preserving transformations and verification improving transformations. This is discussed for PFV, while the concept can be considered for formal verification techniques in general and also for simulation-based approaches.