Recent advances in silicon fabrication technologies, clearly suggest that Moore's law will continue to hold for the next 10-15 years. During this timeframe we will progress from current microprocessors comprising of a couple hundred million transistors towards designs with 1 billion transistors. Consequently, we can safely expect to see tremendously more complicated designs, as we try to exploit the ever-increasing VLSI fabrication capabilities. To make the design of such higher performance microprocessors feasible, CAD tool flows are expected to be drastically changed to allow for more abstraction levels higher in the circuit representation hierarchy. This is necessitated by the fact that Design Validation can be performed faster at a higher level of abstraction. As a result, the microprocessor design process will become an even longer sequence of circuit model transformations.
Hence ascertaining that the microprocessor's functionality is kept unaltered throughout its representation hierarchy will remain a fundamental problem in the design process. Formal equivalence verification techniques have had tremendous success in solving this problem in the last decade. Such techniques are based on mathematical frameworks that conclusively guarantee the equivalence of circuit models, contrary to simulation based approaches. Nevertheless, formal equivalence verification techniques can be limited from space and time complexities that grow exponentially with circuit size in the worst case. The simplest of these formal equivalence approaches require that the corresponding number and placement of memory elements in the circuits under examination are identical. In this case we have an instance of the combinational circuit equivalence problem. This assumption of matching state encodings is applicable only to the comparison of circuit models whose levels of abstraction are not very different. To accommodate the future design methodologies we need to do away with this restriction for enabling the efficient comparison at significantly different levels of abstraction. This requires solving the more general problem of sequential circuit equivalence. In this proposed seminar, the theoretical and practical aspects of the most successful formal equivalence verification techniques will be examined for both the combinational and sequential equivalence checking problems.
The corresponding presentations and discussions will cover the new trends in formal equivalence techniques from many different fields. Equivalence Checking techniques found their way in the mainstream of circuit design CAD tool flows with the maturing of BDD based algorithms. BDDs are canonical representations that allow for extremely efficient comparison of logic functions, but they may suffer from exponential memory requirements. We will review the latest results in this area, including BDD based techniques that exploit structural similarities between circuits under verification to reduce the complexity of combinational equivalence. BDDs as compact representation of transition relations and output functions have enabled Symbolic Model Checking (SMC) techniques for sequential circuit equivalence checking. We will examine the state of the art in Model Checking techniques, where the state space of the product machine is traversed to establish the equivalence of the circuits under comparison. To overcome the worst-case exponential space requirements of BDDs (which also limit the applicability of SMC techniques), researchers have turned to Boolean Satisfiability (SAT) solvers to compare circuit logic functions. SAT solvers completely and exhaustively enumerate the input variable space of circuits to solve the problem of combinational equivalence verification with impressive results lately. In addition, SAT solvers are effectively used in Bounded Model Checking approaches to address the problem of sequential equivalence checking. BDD and SAT based algorithms are fundamentally functional analysis methods and to improve the effectiveness of formal equivalence checking tools researchers have also focused on structural based techniques. So in addition to our focus on SAT and BDD based solutions, we will go over equivalence techniques based on automatic test pattern generation (ATPG). These exhaustive methods operate directly on the circuit structure trying to establish equivalence, in a manner that has evolved from the algorithms used in the manufacturing testing of circuits. Finally, we will focus on integrated approaches that attempt to combine all these techniques. Due to the computational complexities in equivalence checking, no individual technique has been proven completely successful. As a result, researchers have been combining different technologies to make the problem of formal circuit equivalence checking tractable.
Given the above list of topics that will be covered, the goals of the seminar become evident. Initially we wish to review the recent advancements in the core algorithmic solutions for the problem of equivalence verification. Subsequently, we plan to evaluate their scalability in light of the experience accumulated by the design of the complex microprocessors of today. Finally, we would like to motivate further development and integration of formal equivalence techniques according to the emerging trends of future microprocessor designs. The presence of many leading researchers from academia and industry is expected to provide the collaborative framework necessary for capturing the state of the art and clarifying the key technology and methodology challenges that lie ahead in the field of formal circuit equivalence verification.
- Armin Biere (Universität Linz, AT) [dblp]
- Per Bjesse (Prover Technology - Portland, US)
- Kuang-Chien Chen (Verplex Systems Corp. - Milpitas, US)
- Elena Dubrova (KTH Royal Institute of Technology, SE) [dblp]
- Hans Eveking (TU Darmstadt, DE)
- Enrico Giunchiglia (University of Genova, IT) [dblp]
- Ziyad Hanna (Intel Israel - Haifa, IL)
- Geert Janssen (IBM TJ Watson Research Center, US)
- Jie-Hong Roland Jiang (University of California - Berkeley, US)
- Andreas Kühlmann (Cadence Labs - Berkeley, US)
- Wolfgang Kunz (TU Kaiserslautern, DE) [dblp]
- Jörg Lohse (Infineon Technologies Corp. - San Jose, US)
- Joao Marques-Silva (INESC-ID - Lisboa, PT) [dblp]
- Yusuke Matsunaga (Kyushu University - Fukuoka, JP)
- Maher Mneimneh (University of Michigan - Ann Arbor, US)
- In-Ho Moon (Synopsys - Hillsboro, US)
- John Moondanos (University of California - Berkeley, US)
- Prakash Mohan Peranandam (Universität Tübingen, DE)
- Karem A. Sakallah (University of Michigan - Ann Arbor, US) [dblp]
- Christian Stangier (Universität Trier, DE)