Abstract
This chapter explains the necessary concepts needed for the sound understanding of the approximate computing techniques and algorithms discussed in the later chapters. Concise and scalable data structures that can represent the logic of a circuit is crucial for the success of Electronic Design Automation (EDA). Several EDA algorithms to be introduced in the subsequent chapters directly benefit from the underlying data structure. Hence, this chapter starts with an overview of the relevant data structures such as Binary Decision Diagrams (BDDs) and And-Inverter Graphs (AIGs). Several algorithms presented in this book rely heavily on Boolean Satisfiability (SAT). The verification, synthesis, and test techniques for approximate computing are based on SAT. The relevant details about the combinatorial satisfiability problem along with the variants of the classical SAT techniques useful for approximate computing are introduced in the second part. Further, important concepts on the post-production test and Automated Test Pattern Generation (ATPG) are outlined in the next section. This is required for Chap. 6 on test for approximate computing. A discussion on the different error metrics used in approximate computing forms the last part of this chapter. Approximate computing applications express their tolerance using these error metrics. Before getting into the relevant details on these topics, the common notations and conventions used in this book are outlined next.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
These rules are the postulates of Boolean algebra. For more details we refer to Knuth [Knu11].
- 2.
The Shannon expansion theorem: \(f = x_i f_{x_i} \vee \bar x_i f_{\bar x_i}\) is alternately called Boole’s expansion theorem [Bro90].
- 3.
Note: Strictly speaking a Boolean formula is different from a Boolean function. In particular, several Boolean formulas can represent the same Boolean function. For example, x1 ∨ x2 and (x2 ∧ !x1) ∨ x1 are two distinct Boolean formulas, but evaluate to the same Boolean function. In this book, this distinction is not always respected. The terms Boolean formula and Boolean function are used interchangeably unless a clear differentiation is needed. Refer [Knu11, HS02] for a detailed treatment of Boolean algebra and related topics.
- 4.
- 5.
Equi-satisfiable means the satisfiability properties of the input and output are the same.
References
L. Amarú, P.E. Gaillardon, G. De Micheli, Majority-inverter graph: a novel data-structure and algorithms for efficient logic optimization, in Design Automation Conference, vol. 194, pp. 1–194:6 (2014)
H. Andersen, An introduction to binary decision diagrams, in Lecture notes for Efficient Algorithms and Programs, The IT University of Copenhagen, 1999
M.L. Bushnell, V. Agrawal, Essentials of Electronic Testing for Digital, Memory and Mixed-Signal VLSI Circuits (Springer, Boston, 2002)
P. Bjesse, A. Boralv, Dag-aware circuit compression for formal verification. International Conference on Computer Aided Design, pp. 42–49 (2004)
A. Biere, A. Cimatti, E. Clarke, Y. ZhuH, Symbolic model checking without BDDs, in Tools and Algorithms for the Construction and Analysis of Systems, pp. 193–207 (1999)
A. Biere, R. Heule, H. van Maaren, T. Walsh, Handbook of Satisfiability (IOS Press, Berlin, 2009)
A.R. Bradley, Incremental, inductive model checking, in International Symposium on Temporal Representation and Reasoning, pp. 5–6 (2013)
M.A. Breuer, Determining error rate in error tolerant VLSI chips, in Electronic Design, Test and Applications, pp. 321–326 (2004)
F.M. Brown, Boolean Reasoning: The Logic of Boolean Equations (Kluwer, Boston, 1990)
R.E. Bryant, Binary decision diagrams and beyond: enabling techniques for formal verification, in International Conference on Computer Aided Design, pp. 236–243 (1995)
B. Bollig, I. Wegener, Improving the variable ordering of OBDDs is NP-complete. IEEE Trans. Comput. 45, 993–1002 (1996)
J. Cong, Y. Ding, Combinational logic synthesis for LUT based field programmable gate arrays. ACM Trans. Des. Autom. Electron. Syst. 1, 145–204 (1996)
A. Chandrasekharan, D. Große, R. Drechsler, Yise – a novel framework for boolean networks using Y-inverter graphs, in International Conference on Formal Methods and Models for Codesign, pp. 114–117 (2017)
K.H. Chang, I.L. Markov, V. Bertacco, Post-placement rewiring and rebuffering by exhaustive search for functional symmetries, in International Conference on Computer Aided Design, pp. 56–63 (2005)
S. Chakraborty, K.S. Meel, M.Y. Vardi, Algorithmic improvements in approximate counting for probabilistic inference: from linear to logarithmic SAT calls, in International Joint Conference on Artificial Intelligence, pp. 3569–3576 (2016)
S.A. Cook, The complexity of theorem-proving procedures, in Proceedings of the Third Annual ACM Symposium on Theory of Computing, pp. 151–158 (1971)
R. Drechsler, B. Becker, Binary Decision Diagrams: Theory and Implementation (Springer, New York, 1998)
N. Een, A. Mishchenko, R.K. Brayton, Efficient implementation of property directed reachability, in International Conference on Formal Methods in CAD, pp. 125–134 (2011)
H. Fujiwara, T. Shimono, On the acceleration of test generation algorithms. IEEE Trans. Comput. 32, 1137–1144 (1983)
G.D. Hachtel, F. Somenzi, Logic Synthesis and Verification Algorithms (Kluwer, Boston, 2002)
O.H. Ibarra, S.K. Sahni, Polynomially complete fault detection problems. IEEE Trans. Comput. C-24, 242–249 (1975)
D.E. Knuth, The Art of Computer Programming, vol. 4A (Addison-Wesley, Upper Saddle River, 2011)
D.E. Knuth, Pre-fascicle to The Art of Computer Programming, Section 7.2.2. Satisfiability, vol. 4 (Addison-Wesley, Upper Saddle River, 2016)
M.W. Krentel, The complexity of optimization problems. J. Comput. Syst. Sci. 25, 743–755 (1988)
T. Larrabee, Test pattern generation using Boolean satisfiability. IEEE Trans. Comput. Aided Des. Circuits Syst. 11, 4–15 (1992)
A. Mishchenko, S. Chatterjee, R.K. Brayton, Dag-aware aig rewriting a fresh look at combinational logic synthesis, in Design Automation Conference, pp. 532–535 (2006)
M.W. Moskewicz, C.F. Madigan, Y. Zhao, L. Zhang, S. Malik, Chaff: engineering an efficient SAT solver, in Design Automation Conference, pp. 530–535 (2001)
A. Mishchenko, J.S. Zhang, S. Sinha, J.R. Burch, R.K. Brayton, M.C. Jeske, Using simulation and satisfiability to compute flexibilities in boolean networks. IEEE Trans. Comput. Aided Des. Circuits Syst. 25, 743–755 (2006)
Z. Navabi, Digital System Test and Testable Design (Springer, New York, 2011)
A. Petkovska, A. Mishchenko, M. Soeken, G. De Micheli, R.K. Brayton, P. Ienne, Fast generation of lexicographic satisfiable assignments: enabling canonicity in SAT-based applications, in International Conference on Computer Aided Design, pp. 1–8 (2016)
J.P. Roth, Diagnosis of automata failures: a calculus and a method. IBM J. Res. Dev. 10, 278–281 (1966)
SAT-Race–2016, International Conference on Theory and Applications of Satisfiability Testing, 2016
R. Drechsler S. Eggersglüß, High Quality Test Pattern Generation and Boolean Satisfiability (Springer, Boston, 2012)
F. Somenzi, Binary decision diagrams, in NATO Science Series F: Computer and Systems Sciences, vol. 173, pp. 303–366 (1999)
G. Tseitin, On the complexity of derivation in propositional calculus, in Studies in Constructive Mathematics and Mathematical Logic, vol. 2, pp. 115–125 (1968)
F. van Harmelen, V. Lifschitz, B. Porter, Handbook of Knowledge Representation (Elsevier Science, San Diego, 2007)
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this chapter
Cite this chapter
Chandrasekharan, A., Große, D., Drechsler, R. (2019). Preliminaries. In: Design Automation Techniques for Approximation Circuits. Springer, Cham. https://doi.org/10.1007/978-3-319-98965-5_2
Download citation
DOI: https://doi.org/10.1007/978-3-319-98965-5_2
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-98964-8
Online ISBN: 978-3-319-98965-5
eBook Packages: EngineeringEngineering (R0)