Digital circuits are extensively used in computers and digital systems and it is of high importance to guarantee that these circuits are correct in order to prevent issues like the famous Pentium FDIV bug. Formal verification can be used to derive the correctness of a given circuit with respect to a certain specification. However arithmetic circuits, and most prominently gate-level multipliers, impose a challenge for existing verification techniques. Approaches which purely rely on SAT solving or on decision diagrams seem to be unable to solve this problem in a reasonable amount of time. Currently one of the most effective techniques is based on algebraic reasoning. In this approach the circuit is modeled as a set of pseudo-Boolean polynomials and the word-level specification is reduced by a Grübner basis which is implied by the polynomial representation of the circuit. However parts of the multiplier, i.e., final stage adders, are hard to verify using computer algebra. In our approach we combine SAT and computer algebra to substantially improve automated verification of integer multipliers. Complex final stage adders are detected and replaced by simple adders. The correctness of the replacement is verified by SAT solvers and the simplified multiplier is verified by computer algebra techniques. Nonetheless the verification process might not be error-free. Generating and automatically checking proofs independently increases confidence in the results of automated reasoning tools. In order to validate verification results we show how proof certificates can be obtained as a by-product of verifying multiplier circuits in our reduction engine, which can be checked with our independent proof checker tool.

The inability of transistors to switch faster than 60mV/decade is the fundamental limit in physics for technology scaling, which prevents the continuation of Dennard's scaling. As a result, on-chip power densities continuously increase with every new generation leading to excessive temperatures that seriously degrade the reliability of chips. In addition, technology scaling is reaching limits in which displacing few atoms within transistors, due to aging phenomena, provokes uncertainty that may cause catastrophic errors during operation. Due to the inevitable need to include wider and wider guardbands towards sustaining reliability for the entire projected lifetime, the customary trend in which performance is gained with technology scaling becomes profound, if not impossible.

In this talk, we will demonstrate how reliability degradations can be investigated from physics, where they do originate, all the way up to the system level, where they ultimately cause errors. We will show how we can bring reliability awareness to existing commercial EDA tool flows in order to contain guardbands. We will also demonstrate how nondeterministic aging-induced errors can be translated into deterministic and controlled approximations instead, allowing designers to narrow or even remove their guardbands.

Finally, we will discuss how Negative Capacitance Field-Effect Transistor (NCFET), which is a recent emerging technology that suppresses the fundamental limit of 60mV/decade, can reshape the future trends in processor design and rescue technology scaling.