Preserving Design Hierarchy Information for Polynomial Formal Verification
Rolf Drechsler, Alireza Mahzoon · 2022
With the growing complexity of digital circuits, formal verification has become a crucial task after the design in order to ensure the correctness of a circuit. Many existing verification methods suffer from unpredictability in their performance. It is not clear whether they have to be run for seconds, hours, or days to return the verification results or whether they fail in the end. The unpredictability can only be resolved by ensuring complexity bounds. To guarantee scalability we are in particular interested in Polynomial Formal Verification (PFV), where the space and time complexities have polynomial bounds with respect to the size of the circuit.The information about the design hierarchy is usually vital for PFV. Complex digital circuits consist of several components that cannot be verified with an individual verification technique in polynomial space and time. However, with additional knowledge about the boundaries of components, PFV becomes possible through the step-wise verification of sub-components and the use of different formal proof engines. In this paper, we first introduce PFV and clarify its importance. We consider the verification of several flattened gate-level arithmetic circuits and illustrate the challenges of PFV when no design hierarchy is available. Then, we show how these challenges can be overcome by preserving design hierarchy information including the boundaries of the components.