Publication
Design Modification for Polynomial Formal Verification
Rolf Drechsler; Alireza Mahzoon
In: Proceedings of the 2022 International Symposium on Electrical, Electronics and Information Engineering. International Symposium on Electrical, Electronics and Information Engineering (ISEEIE-2022), February 25-27, Chiang Mai, Thailand, Pages 187-194, ISBN 978-1-6654-6874-9, IEEE Computer Society, CA; USA, 2/2022.
Abstract
With the rapid increase in the size and the complexity of digital circuits, the error rate in the design process is getting higher. In order to avoid the enormous financial loss due to the production of buggy circuits, using scalable
formal verification methods is essential. The scalability of a verification method for a specific design is proven by showing that the method has polynomial space and time complexities.
Unfortunately, not all verification methods have a polynomial complexity, particularly when it comes to the verification of complex designs. In this paper, we propose a novel design modification method for polynomial formal verification of complex designs. Complex designs consist of several smaller units that can be verified polynomially using a specific verification method. However, there is not a verification technique that verifies the whole
design (including all units) in polynomial space and time. Our novel method first detects the suitable verification method for each design unit and then makes them visible to the verification
process with minor design modifications. Thus, the verification can be carried out polynomially which was not possible with a single verification technique and without design modification before. The experimental results confirm the efficiency of our method for the verification of complex integer multipliers.