Next-Generation Automatic Human-Readable Proofs Enabling Polynomial Formal Verification

Within the past years, the complexity of digital circuits has grown significantly, resulting in an increased difficulty of their verification. Only based on formal verification techniques, the correctness of a circuit can be fully guaranteed. However, the verification of circuits using formal verification techniques generally requires exponential time and space in the worst case. During the verification process, the formal representations of functions, e.g. BDDs, can have an exponential size, resulting in an exponential verification complexity. Thus, recently the concept of Polynomial Formal Verification (PFV) has been introduced, where polynomial upper bounds are proven for the verification complexity. This has been done successfully e.g. for adders and multipliers. Polynomial upper bounds have been proven manually, but it has not been researched yet, how they can be proven automatically. Here, we propose a tool that automatically proves polynomial upper bounds, providing human-readable proofs by induction. In this paper, the concept of automatic proofs for PFV is shown using BDDs as an example.