Model Checking, From Hardware To Software And Back Again Seminars/Workshops

Abstract

The first major successes of model checking were in hardware verification. Symbolic model checking with BDDs and later SAT-based bounded model checking made it possible to handle hardware designs of realistic complexity. Combining counterexample-guided abstraction refinement and predicate abstraction with these symbolic techniques, led to a new generation of powerful software model checkers (SLAM, BLAST, MAGIC, CBMC, etc). Recently, we have used software model checking techniques to verify programs in hardware description languages like Verilog. Most model checkers for hardware verification currently compile the design into a gate-level description or netlist before verification. As a result, much of the structure of the design is lost and the state explosion problem is exacerbated. By analyzing the hardware description language using software model checking techniques, we are able to avoid the translation into netlist form and handle even larger designs.