This book presents recent advancements in symbolic simulation-based solutionswhich radically improve scalability. We overview current verificationtechniques, both based on logic simulation and on formal verification methods,and we describe in detail the baseline technique of symbolic simulation.The core of this book focuses on new techniques that narrow the performancegap between the complexity of digital systems and the limited ability to verifythem. In particular we cover a range of solutions that exploit approximationand parametrization methods in order to achieve this goal. In the directionof approximation techniques, we comprehensively cover quasi-symbolic simulation- an aggressive technique aiming at simulating only the portion of thedesign necessary for the verification goal at hand - and cycle-based symbolicsimulation - a unique combination of formal methods and logic simulation thatcan stimulate a circuit with a very large number of input combinations and sequences in parallel. Cycle-based symbolic simulation is a hybrid solution thatuses both approximation and parametrization to attain its scalability goal. Itskey concept is the use of a parametric form to represent the set of states visitedduring simulation. This approach maintains a high degree of scalability, in linewith current logic simulation techniques, while achieving better efficiency.In the realm of parametric solutions, we discuss a range of approaches, includingvarious applications of parametric symbolic simulation to industrialmicroprocessor designs. An in-depth analysis is dedicated to another solutionthat we recently proposed, disjoint-support decomposition-based symbolicsimulation, where the parametrization makes use of the disjoint-support decomposition properties of a Boolean function. This simulation technique isrooted on a novel algorithm that exposes the disjoint decomposition propertiesof a Boolean function by restructuring its BDD representation. The newalgorithm is very efficient in the sense that it has worst-case complexity thatis only quadratic in the size of the initial BDD, compared to that of previoussolutions which had exponential complexity in the number of input variablesof the function. We deploy this algorithm to decompose of the state functionsin symbolic simulation. Then, by restructuring the next-state functions usingtheir disjoint components, it is possible to transform them into a simpler parametric form without sacrificing simulation accuracy. Results show that thistechnique is effective in reducing the memory requirements of symbolic simulationwhile maintaining exact state exploration. When the design complexitybecomes overwhelming, it can trade-off search breadth for performance, andproceed to simulate very large trace sets in parallel, thus maintaining a simulation speed and memory profile that are close to logic simulation.In structuring this book, the hope was to provide an interesting reading for abroad range of readers. Chapters 1,2 and 3 constitute a panoramic flight overthe world of digital systems' design and, in particular, verification. Chapter3 reviews some of the mainstream symbolic techniques in formal verification,dedicating most of the focus to symbolic simulation.We use Chapter 4 to cover the necessary principles of parametric formsand disjoint-support decompositions. In particular, we attempt to keep thematerial at a level that facilitates understanding, but without too many formaldetails. While there is a range of resources discussing parametric formsand parametrizations for Boolean functions, we felt that the topic of disjointsupport decompositions was not as readily available. For that reason Appendix A complements Chapter 4 in providing a more formal presentation of the topic and derivation of the theoretical results.Chapters 5 and 6 focus on a range of recent symbolic simulation techniques,which we grouped in approximate solutions, and exact parametrizations. Finally,Chapter 7 wraps up the presentation and outlines possible future researchdirections.