Optimized Hardware/Software Co-Verification using the UCLID Satisfiability Modulo Theory Solver
Simon Schwan, Paula Herber · 2020
Embedded systems are often used in safety-critical applications like cars or airplanes. This makes it crucial to verify their hardware and software under all circumstances. In previous work, we have presented an approach for the formal verification of integrated hardware/software systems using the satisfiability modulo theory solving based verification system UCLID. However, the transformation of integrated hardware/software systems into the input language of the UCLID verification system causes a considerable overhead in the number of symbolic simulation steps necessary for k-inductive verification. In this paper, we overcome this problem by presenting two optimizations for the symbolic simulation of cooperatively scheduled concurrent processes: First, we realize a reduction of redundant states in individual functions that respects all data, control and inter-process dependencies. To capture these dependencies precisely, we present the novel concept of a cooperative dominator tree, which extends the classical concept of a dominator tree to cooperatively scheduled concurrent processes. Second, we present a process parallelization for cooperatively scheduled concurrent processes based on a SystemC dependence graph. In our evaluation based on a set of 21 synthetic case studies, we reach an average reduction of the inductive verification times by 40 %.