Formal Models of Integrated Circuits for Transistor Level Electrical Verification

Abstract

Chip design is a highly complex task. It involves large teams of engineers with a wide range of skills. Their collective goal is to build chips that conform to their respective specifications, and that are bug-free. Despite the efforts made, it is not uncommon for manufactured chips to contain design errors that went unnoticed. Such scenario is a nightmare for semiconductor companies, for the cost of post-fabrication bug fixing is enormous. Companies hence tend to put even more resources toward test and verification than is spent on other design stages. One can clearly see the importance of early error detection in a circuit design project; the earlier an error is discovered, the less it would cost to fix it. This thesis investigates the problem of error verification in integrated circuits (ICs). The design errors of interest are the so-called electrical errors, which are caused by violations of design rules specific to electrical properties. We study existing circuit verification techniques, to understand their limitations. We then introduce our own approaches and demonstrate their use to detect electrical properties violations in industrial circuits. This is achieved by first defining circuit semantics at transistor level, which can be dealt with as satisfiability modulo theories (SMT) problems. Properties (e.g., absence of an error) are then formalized and checked against the circuit formula using an SMT solver, namely Z3. In addition to detecting electrical errors, we address the problem of the analysis of circuits reliability, and more specifically, that of finding the greatest lower bound for reliability of a circuit and the associated electrical state. In fact, the conditions in which a circuit is used determine its degradation rate. To each circuit state is associated a reliability as a function of age, for a given failure mechanism and related model parameters. Hence, finding the greatest lower bound for reliability boils down to identifying the least reliable circuit state at a given age. Such goal is reached by solving the corresponding optimization modulo theories (OMT) problem. The resulting information gives circuit designers solid guarantees on the lifetime of their circuits. These guarantees must be safe. Yet, the more realistic such information is, the better. The approaches introduced in this work use circuit semantics that are derived from the actual circuit behavior. Different semantics, based on different levels of detail in modeling, are explored, implemented, validated against simulation (which is industry-standard in verifying the properties of interest), and compared with each other. The experimental evaluations conducted provide valuable insights on analysis precision-versus-performance tradeoffs.