Automated Polynomial Formal Verification: Human-Readable Proof Generation
Rolf Drechsler, Martha Schnieber · 2023
The importance of verification of digital circuits has increased significantly, as their complexity has grown. Simulation based techniques cannot fully guarantee their correctness, as the correctness has to be shown for every possible input assignment. Thus, formal verification has to be applied. However, formal verification methods may require exponential time and space in the worst case. Therefore, Polynomial Formal Verification (PFV) has been researched in the past years, where polynomial upper bounds have been proven for the complete formal verification process. By this efficient run times of the tools are guaranteed. Polynomial bounds have been proven successfully for the verification of several types of circuits, like e.g. adders and multipliers. However, due to the lack of automation techniques, all previous proofs were conducted manually. A tool enabling the automatic proof generation has recently been introduced, which demonstrates the concept of automatic proofs on the example of Binary Decision Diagrams (BDDs). We enhance the tool to automatically generate an extended human-readable proof, detailing the automatic reasoning, such that the produced proof is fully comprehensible.