Formally verifying divider circuits is complex, and multiple effective methods have been developed. However, none of these methods provides an upper bound on the verification time, which limits their scalability for large divider circuits. Recently, Polynomial Formal Verification (PFV) based approaches have been investigated to ensure circuit correctness in polynomial time and space. However, there is no PFV based approach for the formal verification of dividers. In this paper, we introduce for the first time a two-level partitioning strategy and present PolyRAD, a novel PFV approach for verifying Restoring Array Divider (RAD). Finally, we prove that verification of RAD can be achieved in polynomial time, and conduct experimental evaluation on RAD of different sizes to validate our theoretical findings.

Formal Verification (FV) is a widely used technique for verifying whether a gate-level design is functionally equivalent to its specification. However, when verification fails due to the presence of faults, Debugging and Fault Correction (DFC) becomes essential to localize bugs and correct them. Despite the success of various automatic DFC approaches, existing methods often lack theoretical guarantees on the computational resources required, making them unpredictable in terms of time and space complexity. Therefore, it is essential to establish upper bounds on the time and space complexity of the DFC process to ensure its practical feasibility. In this paper, we rely on the CutWidth (CW) property to introduce Polynomial Debugging and Fault Correction (PDFC) as a subclass of DFC for combinational circuits, where the time and space complexities of DFC are characterized by CW. Specifically, we show that for circuits with bounded CW, the entire DFC process can be polynomially bounded, unlike Yosys SAT, which has exponential complexity. Moreover, we prove that for circuits with constant CW, the entire DFC process can be carried out in linear time and space. Finally, we evaluate several architectures of adders with small constant cutwidth, considering various numbers and locations of faulty gates in terms of time and space required for the DFC process to confirm our theoretical findings and also compare it with Yosys SAT. To demonstrate that our PDFC approach is not limited to adders and can be applied to any design with bounded cutwidth, we also evaluate benchmark circuits fromITC’99andIWLS’93in terms of time and space of the DFC process.

Ensuring the functional correctness of a digital system is achievable through formal verification. Despite the increased complexity of modern systems, formal verification still needs to be done in a reasonable time. Hence, Polynomial Formal Verification (PFV) techniques are being explored, as they provide guaranteed polynomial upper bounds on the time and space required for the verification process. Recently, it was shown that circuits characterized by a constant cutwidth can be verified in linear time using Answer Set Programming (ASP) . However, these results are limited to combinational circuits, whereas most designs used in digital systems are sequential. In this article, we introduce Linear Formal Verification (LFV) as a subclass of PFV for sequential circuits with constant cutwidth, which are verifiable in linear time and space using ASP. We achieve this by proposing a new data structure called Weighted And-Inverter Graph (W-AIG) . Unlike existing formal verification methods, we prove that our approach can verify any sequential circuit with a constant cutwidth in linear time and space. Finally, we implement our approach and experimentally show that a variety of sequential circuits, such as pipelined adders, serial adders, and shift registers, can be verified in linear time and space, while ring counters can be verified in polynomial time and space, confirming our theoretical findings.

In the field of Electronic Design Automation (EDA), managing circuit complexity is a crucial task for efficient circuit verification, testing, and optimization. Increasing design complexity presents challenges for tasks such as formal verification, fault detection, and circuit optimization. Therefore, reducing circuit complexity becomes crucial in improving the efficiency and scalability of these tasks. These circuits are typically represented as graphs. In the field of parameterized complexity, CutWidth (CW) and TreeWidth (TW) are well-studied decomposition techniques that have been used in analyzing graph algorithms. In this paper, we introduce the TW decomposition technique to the field of EDA for the first time and demonstrate its impact on reducing the circuit complexity of circuits. Additionally, we present a new decomposition technique that combines both decompositions, resulting in a further reduction in circuit complexity. Furthermore, we present experimental results comparing complexity upper bounds from various decompositions to highlight the efficacy of our approach on the ISCAS’85 and EPFL benchmark circuits. Our results show that our decomposition technique outperforms the complexity upper bounds of CW by 90.16× and the complexity upper bounds of TW by 9.34× for the ISCAS’85 benchmarks. Additionally, it outperforms the complexity upper bounds of CW by 1986.37× and the complexity upper bounds of TW by 94.13× for the EPFL benchmarks. Finally, to demonstrate the applicability of the decomposition techniques in solving various EDA problems, we propose a new Formal Verification (FV) approach that leverages these techniques to provide an upper bound for the verification process. We also conduct an experimental evaluation on the ITC’99 , MCNC’91 , and VHDL Library of Arithmetic Units ( ELAU ) benchmark circuits, adder circuits of various sizes (up to 3072-bit width), and Genmul multipliers of different sizes (up to 10×10), to demonstrate the scalability of our approach.

Ensuring the functional correctness of a digital system is achievable through formal verification. Despite the increased complexity of modern systems, formal verification still needs to be done in a reasonable time. Hence, Polynomial Formal Verification (PFV) techniques are being explored as they provide a guaranteed upper bound on the run time for verification. Recently, it was shown that combinational circuits characterized by a constant cutwidth can be verified in linear time using Answer Set Programming (ASP). However, most of the designs used in digital systems are sequential. Hence, in this paper, we propose a linear time formal verification approach using ASP for sequential circuits with constant cutwidth. We achieve this by proposing a new data structure called Weighted-And Inverter Graph (W-AIG). Unlike existing formal verification methods, we prove that our approach can verify any sequential circuit with a constant cutwidth in a linear time. Finally, we also implement our approach and experimentally show the results on a variety of sequential circuits like pipelined adders, serial adders, and shift registers to confirm our theoretical findings.

Ensuring functional correctness is achieved through formal verification. As circuit complexity increases, limiting the upper bounds for time and space required for verification becomes crucial. Polynomial Formal Verification (PFV) has been introduced to tackle this problem. In modern digital system designs, approximate circuits are widely employed in error resilient applications. Therefore, ensuring the functional correctness of these circuits becomes essential. In prior works, it has been proven that approximate circuits with constant cutwidth can be verified in linear time. However, extending binary logic verification to Multi-Valued Logic (MVL) introduces challenges, particularly regarding the encoding of MVL operators. It has been shown that MVL circuits with constant cutwidth can be verified in linear time using Answer Set Programming (ASP), due to the ASP encoding capabilities of MVL operators. In this paper, we present a PFV approach of MVL approximate circuits with constant cutwidth using ASP. We then demonstrate that the verification of MVL approximate circuits with constant cutwidth can be achieved in linear time. Finally, we evaluate various MVL approximate circuits with constant cutwidth across different logic levels to show the efficacy of our approach.

In the context of digital circuits, formal verification methods have been well-studied to ensure their functional correctness. However, several verification methods fail to provide an upper bound for the time and space complexity. Therefore, Polynomial Formal Verification (PFV) has been introduced to address this problem. Unlike prior works, which have shown that approximate circuits can be verified in polynomial time, we show that approximate circuits with a constant cutwidth can be verified even in linear time. Since approximate circuits have become ubiquitous in error-resilient applications, it becomes essential to guarantee their correctness. While prior works have been limited to formal error analysis, we use Answer Set Programming (ASP) based formal verification to guarantee that the approximate circuit matches its functional specification. In this paper, we first show that several approximate adder circuits exhibit a constant cutwidth. We then provide a PFV approach that relies on this cutwidth as a structural property of the circuits to guarantee a linear-time verification w.r.t. the bitwidth using ASP. Finally, we evaluate several approximate adders in terms of the upper bound of the cutwidth, and verification time.

Only formal methods can guarantee the correctness of a circuit, but are usually very time and memory consuming. Therefore, efficient formal verification is key in the design of complex circuits. Many verification techniques have been introduced, which mostly fail to give bounds for the time complexity of the verification process. To overcome this issue, Polynomial Formal Verification (PFV) was introduced. This paper introduces a novel approach to PFV of circuits, by leveraging the concept of constant cutwidth. We divide the circuit into subgraphs, one for every output. This makes the verification of every subgraph only dependent on the cutwidth of the circuit and independent of the bitwidth. One main problem we solve is the passing of information between those subgraphs. The approach enables formal verification in linear time for circuits with constant cutwidth.

Answer set programming is a form of declarative programming widely used to solve difficult search problems. Probabilistic applications however require to go beyond simple search for one solution and need counting. One such application is plausibility reasoning, which provides more fine-grained reasoning mode between simple brave and cautious reasoning. When modeling with ASP, we oftentimes introduce auxiliary atoms in the program. If these atoms are functionally independent of the atoms of interest, we need to hide the auxiliary atoms and project the count to the atoms of interest resulting in the problem projected answer set counting. In practice, counting becomes quickly infeasible with standard systems such as clasp. In this paper, we present a novel hybrid approach for plausibility reasoning under projections, thereby relying on projected answer set counting as basis. Our approach combines existing systems with fast dynamic programming, which in our experiments shows advantages over existing ASP systems.