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.

As the need for efficient digital circuits is ever growing in the industry, the design of such systems remains daunting, requiring both expertise and time. In an attempt to close the gap between software development and hardware design, powerful features such as functional and object-oriented programming have been used to define new languages, known as Hardware Construction Languages. In this article, we investigate the usage of such languages—more precisely, of Chisel—in the context of Design Space Exploration, and propose a novel design methodology to build custom and adaptable design flows. We apply an innovative functional approach to define flexible strategies for design space exploration, based on the composition of basic exploration steps, and provide a library of basic strategies along with a proof-of-concept framework—which we believe to be the first Chisel-based DSE framework. This framework fully integrates within the ecosystem of Chisel to allow users to define their DSE processes in the same framework (and language) they use to describe their designs. We demonstrate our methodology through several use cases, illustrating how our functional approach makes it possible to consider various metrics of interest when building exploration processes—in particular, we provide a quality of service -driven exploration example. The methodology presented in this work makes use of designers’ expertise to reduce the time required for hardware design, in particular for Design Space Exploration, and its application should ease digital design and enhance hardware developers’ productivity.

Hardware design processes often come with time-consuming iteration loops, as feedbacks generally result of long synthesis runs. It is even more true when multiple different implementations need to be compared to perform Design Space Exploration (DSE). In order to accelerate such flows and increase agility of developers — closing the gap with software development methodologies — we propose to use quick feedback generating transforms based on RTL circuit analysis for quicker convergence of exploration. We also introduce an Hardware Construction Language (HCL) based methodology to build explorable circuit generators, and demonstrate such usage over a General Matrix Multiply (GEMM) Chisel implementation. We demonstrates that using RTL estimation early in the exploration process results in ×7 less synthesis runs and ×4.1 faster convergence than an exhaustive synthesis process, and still achieves state of the art performances when targetting a Xilinx VC709 FPGA.