Polynomial Formal Verification of General Tree-Like Circuits
Alireza Mahzoon, Rolf Drechsler · 2022 China Semiconductor Technology International Conference (CSTIC) · 2022
In recent years, the size and complexity of digital circuits have grown drastically. Consequently, bugs may appear in a circuit in different phases of design and synthesis. If they remain undetected, they propagate to the physical chip and cause huge financial loss for the designers and manufacturers. Formal verification is an important task after design to ensure the correctness of a circuit. Recently, polynomial formal verification has gained special attention. If we prove that the space and time complexity of a verification method is polynomial, we can ensure that it is always scalable. Many digital circuits which are used in different applications have a tree-like structure. It has been proven that if a tree-like circuit is made of basic logic gates (AND, OR, NOT, NAND, and NOR), it can be verified polynomially using BDDs. However, these proofs cannot be extended to the general tree-like circuits containing XOR gates. In this paper, we propose a method to prove the correctness of a general tree-like circuit in polynomial time.