Logic Synthesis and Verification provides a state-of-the-art view of logic synthesis and verification. It consists of fifteen chapters, each focusing on a distinct aspect. Each chapter presents key developments, outlines future challenges, and lists essential references.
Two-level logic minimization
This chapter presents both exact and heuristic two-level logic minimization algorithms. For exact logic minimization, it shows various techniques to reduce the complexity of covering problems, discusses branching heuristics, and presents several methods ...
Multi-level logic optimization
Three basic methods for multi-level logic optimization, namely algebraic logic optimization, Boolean logic optimization, and decomposition is a fundamental technology for the generation of multi-level logic. The application of BDDs offers an increased ...
Flexibillity in logic
It is possible to synthesize more efficient implementations if we remove the requirement of preserving local functionality. This can be done to some degree by taking into account the environment of the logic targeted by synthesis. The environment ...
Multiple-valued logic synthesis and optimization
Some Boolean logic problems can be solved more efficiently in multiple-valued domain. This chapter covers a part of the theory of multiple-valued logic related to applications in CAD. Basic methods for representation and optimization of multiple-valued ...
Technology mapping
Technology mapping transforms a technology independent logic network into gates implemented in a technology library. This chapter focuses on the three phases of technology mapping: decomposition, pattern matching and covering. Traditionally, a lot of ...
Technology-based transformations
Technology mapping is inherently a difficult problem. The current mapping algorithms cannot provide optimum solutions for minimum delay or area for industrial circuits in the presence of large gate libraries, complex design constraints, realistic & ...
Logical and physical design: a flow perspective
A physical design flow consists of producing a production-worthy layout from a gate-level netlist subject to a set of constraints. This chapter focuses on the problems imposed by shrinking process technologies, and their solutions in the context of ...
Logic synthesis for low power
Energy-efficient design of integrated ciecuits requires specialized tools and technologies. This chapter surveys some of the most important contributions in logic synthesis for achieving low-power consumption, by means of gete-level and register-...
Optimization of synchronous circuits
We study techniques for optimizing synchronous sequential circuits. These techniques use either state-based or structural gate-level models. We survey recent advances in state-based techniques focusing on the computation of the flexibility in ...
Asynchronous control circuits
Asynchronous, or clockless, design is receiving renewed attention, due to its potential benefits of modularity, low power, low electromagnetic interference and average-case performance. This chapter focuses on two styles for asynchronous controller ...
Ordered binary decision diagrams
Ordered Binary Decision Diagrams (OBDDs) play a key role in the automated synthesis and formal verification of digital systems. They are the state-of-the-art data structure for representing switching functions in various branches of electronic design ...
SAT and ATPG: algorithms for Boolean decision problems
The problems of Boolean satisfiability (SAT) and automatic test pattern generation (ATPG) are strongly related - both in terms of application areas (premanufacturing design validation and post-manufacturing testing), as well as in terms of techniques ...
Combinational and sequential equivalence checking
This chapter covers the problem of deciding functional equivalence of two design descriptions. We focus our presentation on the most commonly used form of equivalence checking, which compares the input/output behavior of two deterministic design models. ...
Static timing analysis
Static timing analysis is a technique for estimating the delay of a design without electrical simulation. It is widely adopted in industry for timing verification and optimization. This chapter will overview the basics of static timing analysis.
The future of logic synthesis and verification
Logic synthesis has been worked on for at least 40 years, and much has been accomplished, with many commercial tools developed and used pervasively. However, in light of the continual progress made in technology, more complex designs will be made and ...
Cited By
- Amarú L, Soeken M, Vuillod P, Luo J, Mishchenko A, Gaillardon P, Olson J, Brayton R and De Micheli G Enabling exact delay synthesis Proceedings of the 36th International Conference on Computer-Aided Design, (352-359)
- Huang H and Densmore D (2014). Fluigi, ACM Journal on Emerging Technologies in Computing Systems, 11:3, (1-19), Online publication date: 30-Dec-2015.
- Färm P, Dubrova E and Kuehlmann A Integrated logic synthesis using simulated annealing Proceedings of the 21st edition of the great lakes symposium on Great lakes symposium on VLSI, (407-410)
- Cong J, Liu B, Majumdar R and Zhang Z (2010). Behavior-Level Observability Analysis for Operation Gating in Low-Power Behavioral Synthesis, ACM Transactions on Design Automation of Electronic Systems, 16:1, (1-29), Online publication date: 1-Nov-2010.
- Gershenfeld N, Dalrymple D, Chen K, Knaian A, Green F, Demaine E, Greenwald S and Schmidt-Nielsen P (2010). Reconfigurable asynchronous logic automata, ACM SIGPLAN Notices, 45:1, (1-6), Online publication date: 2-Jan-2010.
- Gershenfeld N, Dalrymple D, Chen K, Knaian A, Green F, Demaine E, Greenwald S and Schmidt-Nielsen P Reconfigurable asynchronous logic automata Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, (1-6)
- Orshansky M and Wang W (2009). Statistical analysis of circuit timing using majorization, Communications of the ACM, 52:8, (95-100), Online publication date: 1-Aug-2009.
- Koes D and Goldstein S Near-optimal instruction selection on dags Proceedings of the 6th annual IEEE/ACM international symposium on Code generation and optimization, (45-54)
- Zafiu A, Stefanescu I, Laurentiu I, Ghita C and Franti E An exact method to compute maximal implicants in a multivalued logic Proceedings of the 5th WSEAS international conference on System science and simulation in engineering, (249-254)
- Babighian P, Benini L and Macii E A Scalable ODC-Based Algorithm for RTL Insertion of Gated Clocks Proceedings of the conference on Design, automation and test in Europe - Volume 1
- Saluja N and Khatri S A robust algorithm for approximate compatible observability don't care (CODC) computation Proceedings of the 41st annual Design Automation Conference, (422-427)
- Bengtsson T, Martinelli A and Dubrova E A BDD-based fast heuristic algorithm for disjoint decomposition Proceedings of the 2003 Asia and South Pacific Design Automation Conference, (191-196)
- Sinha S, Mishchenko A and Brayton R Topologically constrained logic synthesis Proceedings of the 2002 IEEE/ACM international conference on Computer-aided design, (679-686)
- Keutzer K and Orshansky M From blind certainty to informed uncertainty Proceedings of the 8th ACM/IEEE international workshop on Timing issues in the specification and synthesis of digital systems, (37-41)
Index Terms
- Logic Synthesis and Verification
Recommendations
Algorithmic logic-based verification
Turing in his seminal paper "Checking a Large Routine" [Turing 1949] already asked the question whether it was possible to check a routine was right. Among other contributions, he proposed flowcharts as a concise program representation. He also ...