Design Modification for Polynomial Formal Verification
Rolf Drechsler, Alireza Mahzoon · 2022
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.