Kratos - A Software Model Checker for SystemC

Abstract. The growing popularity of SystemC has attracted research aimed at the formal verification of SystemC designs. In this paper we present KRATOS, a software model checker for SystemC. KRATOS verifies safety properties, in the form of program assertions, by allowing users to explore two directions in the verification. First, by relying on the translation from SystemC designs to sequen-tial C programs, KRATOS is capable of model checking the resulting C programs using the symbolic lazy predicate abstraction technique. Second, KRATOS imple-ments a novel algorithm, called ESST, that combines Explicit state techniques to deal with the SystemC Scheduler, with Symbolic techniques to deal with the Threads. KRATOS is built on top of NUSMV and MATHSAT, and uses state-of-the-art SMT-based techniques for program abstractions and refinements. 1 introduction Formal verification of SystemC has recently gained significant interests [19, 13, 18, 23, 16, 22, 10]. Despite its importance, verification of SystemC designs is hard and chal-lenging. A SystemC design is a complex entity comprising a multi-threaded program where scheduling is cooperative, according to a specific set of rules [21], and the exe-cution of threads is mutually exclusive. In this paper we present KRATOS, a new software model checker for SystemC. KRATOS provides two different analyses for verifying safety properties (in the form of program assertions) of SystemC designs. First, KRATOS implements a sequential anal-ysis based on lazy predicate abstraction [15] for verifying sequential C programs. To verify SystemC designs using this analysis, we rely on the translation from SystemC to a sequential C program, such that the resulting C program contains both the mapping of SystemC threads in the form of C functions and the encoding of the SystemC sched-uler. Second, KRATOS implements a novel concurrent analysis, called ESST [10], that combines Explicit state techniques to deal with the SystemC Scheduler, with Symbolic techniques, based on lazy predicate abstraction, to deal with the Threads. KRATOS is available for download a