# Hardware Model Checking Algorithms and Techniques
## 9 Conclusions  
This paper provides an in-depth overview of the most common SAT-based algorithms usually applied in bit-level hardware model checking scenarios. In the last two decades, SAT-based model checking brought about a leap in the performance and scalability of symbolic model checking algorithms. SAT-based model checking tools have managed to almost supplant BDD-based ones in both industry and academia. Model checking algorithms based on SAT solving, however, still suffer from non-negligible scalability issues when confronted with the complexity of many industrial-scale designs. Improving the performance and scalability of such algorithms is a very challenging, yet very active, research path. This paper strives to provide both a thorough overview of the background required to understand the topics at hand, and a complete description of the aforementioned algorithms and their intricacies. Based on the current state of the art, a selection of the most relevant methods has been identified and described, taking into account both bounded and unbounded model checking, with a focus on safety properties. For the sake of generality, this work provides a description of each algorithm from a theoretical standpoint, trying to avoid details which would turn out to be too implementation oriented in favour of the soundness and comprehensiveness of their description and discussion. As mentioned in the introductory section, as of today, there is no a single winning strategy applicable to the broad range of verification problems one may face. It has thus become almost mandatory to tackle verification tasks using a portfolio of techniques, running in a concurrent/collaborative fashion, in order to maximize the chance of success. Furthermore, additional factors, such as model pre-processing and simplification, property management, engine orchestration, etc., play a role as important as the actual model checking algorithm of choice in determining the success of the verification procedure. This is the main reason why the current research path in this field usually reaches across several different directions, targeting different aspects of the verification chain, rather than focusing on a single specific step. Nevertheless, it is absolutely crucial to develop a firm and sound understanding of the available techniques in order to properly orchestrate verification efforts. For the future, the current path of research is aimed at supporting hierarchical verification for top-down design, embedding support for verification in the whole design chain, starting from specification languages. Currently, there is a need for being able to write a verifiable high-level design, that can then be refined and implemented, while guaranteeing that it is still consistent with its abstraction. The main aim is for properties that have been verified at a given step of the design chain to hold at any other successive level of refinement. Such a desideratum leads to hybrid and top-down/bottom-up design methodologies, with emphasis on verification as grounding for correctness, as well as introducing the need for some sort of certificate, to guarantee the correctness of each step, transformation and refinement involved in the process. Alongside hierarchical verification, the integration of model checking within design becomes even more pressing, where model checkers represent auxiliary tools within the design chain, to support and validate correctness. Despite its potential usefulness, the adoption of model checking in industrial scenarios is still an ongoing process, where funding and methodology changes are the main limiting factors, in conjunction with the absence of a definitively best approach at tackling verification problems. Because of this, we can foresee that for the coming years portfolio-based approaches, exploiting divide-and-conquer strategies among different verification engines, will still be the most consistent way to address such tasks. Conceptualization, P.E.C., G.C., M.P. and P.P. ; methodology, M.P. and P.P. ; software, G.C.