Improving bit-level model checking algorithms for scalability through circuit-based reasoning

In the last few years real-life designs have become more and more complex, thus proper circuit management, simplification and transformation proved as important as the actual verification procedure. On the other hand, given the impossibility to determine a priori the best algorithm to use for each benchmark, portfolio approaches have become the de-facto standard in model checking. Tuning parameterization and behavior of the various algorithms in play is nowadays a must. This dissertation describes the activities conducted during the whole PhD course span, concerning model checking algorithms and preprocessing techniques in the context of industrial-derived hardware designs. More in details, some studies addressed during these years focused on appropriate property management, efficient model preprocessing techniques, proper SAT solver management and the introduction of a novel model checking algorithm.