Adders

For adders, BDD-based verification has already been known to produce good results. However, upper bounds for the complexity were not investigated before the PolyVer project. PolyAdd demonstrated that the three basic adder architectures ripple carry adder, conditional sum adder and carry look-ahead adder can be verified in polynomial time and space using BDD-based verification. The results were later extended to general prefix adders and were therefore proven for a class of circuits instead of a specific circuit.

Publications | Adders

Multipliers

The formal verification of multipliers poses a more complicated challenge, as the BDD of the multiplication function has already been proven to have an exponential size. However, the use of Multiplicative Binary Moment Diagrams (*BMDs) results in polynomial upper bounds for Wallace- tree like multipliers. Another state-of-the-art verification method for multipliers is Symbolic Computer Algebra (SCA). Within the PolyVer project, hybrid methods consisting of BDD- and SCA-based verification were explored for the PFV of more complex non-trivial multipliers.

Publications | Mutipliers

Complex Arithmetic Circuits

In addition to basic circuits, such as adders and multipliers, more complex arithmetic circuits exist that contain multiple operations, therefore complicating their verification process. However, it was proven that a simple Arithmetic Logic Unit (ALU) can be verified in polynomial time and space using BDDs. The PFV of processors has been investigated within the PolyVer project at the example of a RISC-V processor, where PFV has been proven to be possible for a RISC-V RV32I and MicroRV32 processor. Furthermore, PFV could be applied to a general arithmetic circuit computing a polynomial. In addition to integer arithmetic circuits, PFV has been applied to floating point arithmetic circuits as well, specifically to floating point adders and floating point multipliers. In this context, exponential lower bounds were also proven for shifted addition using BDDs.

Publications | Complex Arithmetic Circuits

Approximate Circuits

As small errors are acceptable in these applications, exact circuits can be approximated for smaller area or delay, while producing wrong outputs for some inputs. The verification complexity of approximate adders has been researched within the PolyVer project. It was proven that the verification of several state-of-the-art approximate adders is guaranteed to have a polynomial time and space complexity. Apart from approximate adders, the possibility of polynomial formal verification of general approximate circuits has also been investigated.

Publications | Approximate Circuits

Structural Properties

PFV has also been proven to be possible for circuits with some specific functional and structural properties. Thus, circuits can be designed such that an efficient verification is guaranteed. Here, PFV could be applied to tree-like circuits, i.e. circuits without fanouts, as well as BDD circuits and KFDD circuits. PFV has also been proven to be possible for totally symmetric functions, meaning functions where the output does not depend on the order of the input variables, as well as circuits of logarithmic depth. Furthermore, Answer Set Programming (ASP) and Boolean Satisfiability (SAT) were used for PFV, where it was proven that circuits with a constant cutwidth and treewidth can be verified in linear time and space.

Publications | Functional Properties

Hierarchical Information

Complex circuits often consist of multiple components for which PFV is not possible using the same formal verification technique. Furthermore, the boundaries of the components are not available in the gate-level netlist. Thus, PFV might not be possible for complex digital circuits without additional hierarchical information. However, hierarchical information can be preserved, enabling PFV by the separate verification of components using different formal verification techniques.

Publications | Hierarchical Information

Sequential Circuits

Even though the focus of the PolyVer project is the verification of combinational circuits, there are several cases where sequential behavior cannot be ignored. In contrast to combinational circuits, states have to be considered for the verification of sequential circuits. Here, Finite State Machines (FSMs) can be used to observe the state behavior of the circuit. It was shown that some simple sequential circuits can be verified in polynomial time and space, even if the underlying FSM has an exponential sequential depth.

Publications | Sequential Circuits

Automatic Proofs

All previously mentioned proofs were conducted manually. However, within the PolyVer project, possibilities for automatically generating the proofs were investigated as well. A first concept for the automatic generation of proofs for PFV was presented, where the concept was exemplarily shown on BDDs. Using the proposed tool, polynomial upper bounds can automatically be proven while producing a human-readable proof to ensure the understandability of the tool.

Publications | Automatic Proofs

2026

Mohamed Nadeem, Luca Müller, Chandan Kumar Jha, Rolf Drechsler. Advanced And-Inverter Graph Decomposition Technique for Reducing Circuit Complexity. In Transactions on Design Automation of Electronic Systems, DOI:10.1145/3771280, 2026.

Mohamed Nadeem, Chandan Kumar Jha and Rolf Drechsler. PolyEMAC: Polynomial Error Metrics Analysis in Approximate Computing. In International Conference On VLSI Desig (VLSID), 2026.

2025

Mohamed Nadeem, Chandan Kumar Jha, Rolf Drechsler. Polynomial Formal Verification of Sequential Circuits using Weighted-AIGs. In Design, Automation and Test in Europe Conference (DATE), DOI:10.23919/DATE64628.2025.10992799, 2025.

Lennart Weingarten, Kamalika Datta, Rolf Drechsler. Late Breaking Results: Towards Efficient Formal Verification of Dot Product. In Design, Automation and Test in Europe Conference (DATE), DOI:10.23919/DATE64628.2025.10992946 2025.

Rolf Drechsler. Preserving and Improving Verifiability of Circuits Based on Local Transformations. In Latin-American Test Symposium (LATS), DOI:10.1109/LATS65346.2025.10963945, 2025.

Jan Kleinekathöfer, Rolf Drechsler. Automatic Polynomial Formal Verification of a Floating Point Multiplier. In Euromicro Conference Series on Digital System Design (DSD), 2025.

Martha Schnieber, Rolf Drechsler. Synthesis for Testability: Polynomial Test Pattern Generation for KFDD Circuits. In Euromicro Conference Series on Digital System Design (DSD), 2025.

Mohamed Nadeem, Rolf Drechsler. Linear Formal Verification of Multi-Valued Logic Circuits within Constant Cutwidth Architectures. In Multiple-Valued Logic and Soft Computing, 2025.

Martha Schnieber, Rolf Drechsler. Automated polynomial formal verification using generalized binary decision diagram patterns. In Philosophical Transactions of the Royal Society A, DOI:10.1098/rsta.2023.0390, 2025.

Mohamed Nadeem, Chandan Kumar Jha, Rolf Drechsler. Polynomial Formal Verification of Multi-Valued Approximate Circuits within Constant Cutwidth. In IEEE Transactions on Circuits and Systems I: Regular Papers, DOI:10.1109/TCSI.2025.3531008, 2025.

Lennart Weingarten, Kamalika Datta, Rolf Drechsler. Polynomial Formal Verification of a RISC-V Processor. In Transactions on Nanotechnology (TNANO), DOI:10.1109/TNANO.2025.3548265, 2025.

Jan Kleinekathöfer, Alireza Mahzoon, Rolf Drechsler. Lower bound proof for the size of BDDs representing a shifted addition. In Information Processing Letters, DOI:10.1016/j.ipl.2025.106571, 2025.

Lennart Weingarten, Kamalika Datta, Sallar Ahmadi-Pour, Abhoy Kole, Rolf Drechsler. Ensuring Correctness Efficiently for RISC-V Processors with Customised Multiplier Designs. In Design and Verification of Cyber-Physical Systems: From Theory to Applications, 2025.

Mohamed Nadeem, Chandan Kumar Jha, Rolf Drechsler. Polynomial Debugging and Fault Correction of Combinational Circuits With Constant Cutwidth. In Transactions on Circuits and Systems I: Regular Papers, DOI:10.1109/TCSI.2025.3633991, 2025.

Luca Müller, Rolf Drechsler. Polynomial formal verification parameterized by cutwidth properties of a circuit using Boolean satisfiability. In Microprocessors and Microsystems (MICPRO), DOI:10.1016/j.micpro.2025.105199, 2025.