# Hardware Model Checking Algorithms and Techniques
## 1 Introduction  
Ranging from commodity devices to business or safety critical environments, digital systems have proliferated into most aspects of our daily lives. Moreover, thanks to Moore's law and the advent of high-level synthesis, contemporary hardware designs often comprise an extremely high level of complexity. As a direct consequence, design verification has become one of the most relevant aspects of the design and production flow. In such a scenario, guaranteeing the correct behavior of digital systems, with respect to their specification, is becoming an ever more pressing need for manufacturers [1]. The increasing complexity of hardware designs, together with the demand for short development cycles imposed by ever evolving markets, makes the delivery of defect-free systems an extremely challenging task. This is particularly true when considering sequential designs, in which the behavior of the system depends not only on the inputs applied at a given time but also on the state the system finds itself in. Modern systems are characterized by the presence of several million elements, those being transistors, logic gates, memory elements or other things. In such a scenario, design verification can represent one of the most time consuming, yet necessary, activities to be performed, with reports supporting it in the range between 40% and 70% of the entire cycle's endeavor [2]. Oftentimes, the usual testing techniques are not enough to prove the correctness of a whole system in a timely fashion, and further problems arise when taking into account the issue of transferring theoretical results to industrial practice [3]. Traditionally, hardware designs are verified through _simulation_. In simulation, a model of the system is solicited by a set of stimuli while the resulting behavior is checked against the expected behavior. Simulation is scalable, being applicable to designs of virtually any size, but is also costly and incomplete. In fact, it is often unfeasible to completely cover the behaviors of a realistic design through simulation. The incompleteness of simulation is often aggravated by the increasing complexity of hardware designs, which not only increases the number of behaviors to check but may also introduce corner cases difficult to cover. Starting from the late 1980s, _formal hardware verification_ has become an attractive approach to overcome the coverage limitations of simulation. Formal verification is the useof the formal methods of mathematics and logic to prove (or disprove) the correctness of a design with respect to a given formal specification of its expected behavior. During the last two decades, research in the field of formal verification has led to the development of many techniques. Such techniques can be subdivided into three main approaches to formal verification: _theorem proving_[4; 5], _equivalence checking_[6] and _model checking_[7; 8]. Model checking is the most widely used formal verification approach for sequential hardware designs. In model checking, a _model_ of the design and a formalized representation of its specification are formulated using some mathematically precise and unambiguous language. Then, an algorithmic procedure automatically checks whether or not the model meets the formal specification. Such a procedure exhaustively traverses the modeled behaviors of the system and either confirms that the system behaves correctly or produces a trace that demonstrates a violating behavior (called a _counterexample_). The main advantages of model checking are its fully automated nature and its ability to produce counterexamples. Usually, the design to be verified is modeled as a _transition system_, comprising states and transitions between states, and the specification is formalized by writing _temporal logic properties_. Invariant verification is a particular model checking task in which the system specification is described as an invariant property that must hold true in every reachable state of the model.