The behavior of any electronic system can be traced back to how its constituting components physically interact with each other. Such low-level interactions explain how specific states of a given circuit are physically possible. Some circuit states can be erroneous, e.g., applying a voltage stress greater than what some device can tolerate. It is of particular importance to know whether such errors can happen on a given circuit, so that required corrections can be made. Identifying errors requires some circuit modeling technique, and a way to explore the state space of the circuit model (which may be very large if at all finite). In this work, we show the limitations of classical verification techniques, and propose a new approach based on formal methods to overcome them. We propose new circuit semantics for transistor-level descriptions from (1) recalling and improving existing semantics, and (2) introducing novel alternate ones. We then demonstrate their usage in our verification framework—which makes use of a satisfiability modulo theories (SMT) solver—to verify specific electric properties of circuits. Specifically, we address the problem of the search for circuit transistors that are subject to electrical overstress (EOS). We draw interesting conclusions by comparing the presented circuit semantics, both formally and via experimental benchmarks.

Hardware verification is crucial to ensure the quality of Integrated Circuits, and prevent costly bugs down the manufacturing flow. Electrical Rule Checking (ERC) is a verification step used to assert that a circuit complies with some electrical rules, from the absence of short-circuits to dedicated constructor rules. In this survey, we provide a global overview of existing ERC techniques at transistor-level, where voltage values are explicit. We propose a new classification method to compare the existing approaches based on their semantic modeling of circuits. This survey precisely describes transistor-level ERC research challenges and existing solutions. We believe it will help structure this research domain by positioning existing approaches with respect to each other. Obviously, a survey should also facilitate technological transfer and this one should help CAD vendors identify the most relevant approaches to integrate in their tools. Finally, we highlight several promising directions to improve the existing solutions.

We present a novel technique for Electrical Rule Checking (ERC) based on formal methods. We define a relational semantics of Integrated Circuits (IC) as a means to model circuits' behavior at transistor-level. We use Z3, a Satisfiability Modulo Theory (SMT) solver, to verify electrical properties on circuits – thanks to the defined semantics. We demonstrate the usability of the approach to detect current leakage due to missing level-shifter on large industrial circuits, and we conduct experiments to study the scalability of the approach.

We consider the verification of electrical properties of circuits to identify potential violations of electrical design rules, also called Electrical Rule Checking (ERC). We present a general approach based on Satisfiability Modulo Theory (SMT) to verify that these errors cannot occur in a given circuit. We claim that our approach is scalable and more precise than existing analyses, like voltage propagation. We applied these techniques to a specific type of errors, the missing level shifters. On an industrial case-study, our technique is able to flag 31 % of the warnings raised by the voltage propagation analysis as being false alarms.

We study the approximability of the NP-complete Maximum Minimal Feedback Vertex Set problem. Informally, this natural problem seems to lie in an intermediate space between two more well-studied problems of this type: Maximum Minimal Vertex Cover, for which the best achievable approximation ratio is n, and Upper Dominating Set, which does not admit any n1−ϵ approximation. We confirm and quantify this intuition by showing the first non-trivial polynomial time approximation for Maximum Minimal Feedback Vertex Set with a ratio of O(n2/3), as well as a matching hardness of approximation bound of n2/3−ϵ, improving the previously known hardness of n1/2−ϵ. Having settled the problem's approximability in polynomial time, we move to the context of super-polynomial time. We devise a generalization of our approximation algorithm which, for any desired approximation ratio r, produces an r-approximate solution in time nO(n/r3/2). This time-approximation trade-off is essentially tight under the ETH.

Optimization problems consist of either maximizing or minimizing an objective function. Instead of looking for a maximum solution (resp. minimum solution), one can find a minimum maximal solution (resp. maximum minimal solution). Such "flipping" of the objective function was done for many classical optimization problems. For example, ${\rm M{\small INIMUM}}$ ${\rm V{\small ERTEX}}$ ${\rm C{\small OVER}}$ becomes ${\rm M{\small AXIMUM}}$ ${\rm M{\small INIMAL}}$ ${\rm V{\small ERTEX}}$ ${\rm C{\small OVER}}$, ${\rm M{\small AXIMUM}}$ ${\rm I{\small NDEPENDENT}}$ ${\rm S{\small ET}}$ becomes ${\rm M{\small INIMUM}}$ ${\rm M{\small AXIMAL}}$ ${\rm I{\small NDEPENDENT}}$ ${\rm S{\small ET}}$ and so on. In this paper, we propose to study the weighted version of Maximum Minimal Edge Cover called ${\rm U{\small PPER}}$ ${\rm E{\small DGE}}$ ${\rm C{\small OVER}}$, a problem having application in genomic sequence alignment. It is well-known that ${\rm M{\small INIMUM}}$ ${\rm E{\small DGE}}$ ${\rm C{\small OVER}}$ is polynomial-time solvable and the "flipped" version is NP-hard, but constant approximable. We show that the weighted ${\rm U{\small PPER}}$ ${\rm E{\small DGE}}$ ${\rm C{\small OVER}}$ is much more difficult than ${\rm U{\small PPER}}$ ${\rm E{\small DGE}}$ ${\rm C{\small OVER}}$ because it is not $O(\frac{1}{n^{1/2-\varepsilon}})$ approximable, nor $O(\frac{1}{\Delta^{1-\varepsilon}})$ in edge-weighted graphs of size $n$ and maximum degree $\Delta$ respectively. Indeed, we give some hardness of approximation results for some special restricted graph classes such as bipartite graphs, split graphs and $k$-trees. We counter-balance these negative results by giving some positive approximation results in specific graph classes.