Advanced Techniques for Bit-Level Model Checking

With increasing design complexity, verification becomes a more and more important aspect of the design flow: modern circuits contain up to several million transistors, causing verification to be the major bottleneck and the most expensive stage. This is one of the reasons why Formal Verification techniques are gaining large attention, since they allow to prove correctness of a circuit (ensuring a total functional correctness) compared to classical simulation, which cannot guarantee sufficient coverage of the design, due to its intrinsic not complete nature. Being Formal Verification a complete technique, its natural application can be found in all those critical systems where the absence of bugs is mandatory. In particular, hardware design can be considered as one of the most critical areas, due to the difficulties (and costs) involved in solving a fault introduced at the design stage, but exposed only after its manufacturing. On the other hand, generally speaking, a software system could be patched easily, just releasing a newer version of the software itself. Nevertheless recently also software applications are becoming a relevant area of application for Formal Verification techniques, especially concerning safety critical applications, software security aspects and firmware of embedded systems. Nowadays the most widely used approach to Formal Verification is Model Checking, which consists of a systematically exhaustive exploration of the mathematical model of the system under analysis. The great advantage of Model Checking is that, provided the model of the system and the property to check, it is fully automatic; while its primary disadvantage relies on the difficulty to scale to large systems. The main goal of this Ph.D. dissertation is to present improvements to Model Checking algorithms for hardware design, focused on scalability and efficiency aspects. Every contribution is provided with exhaustive experimental data, performed on industrial test-cases. This dissertation studies also a recent but equally relevant (and critical) area of application for Model Checking algorithms: the verification of security properties in embedded systems. In this context, due to the novelty of this topic, efforts were oriented to study the applicability of the Model Checking approach, leaving the scalability aspects to further works.