A New SAT-Based Approach for Equivalence Checking of Hardware-Dependent Low-Level Embedded System Software

Abstract:
This paper presents a novel approach to formally prove the equivalence of low-level hardware-dependent programs. Inspired by hardware verification techniques, a software miter is developed as the computational model to perform the verification task. Taking into account the reactive behavior exposed by the software, two programs are shown to be equivalent if they exhibit the same input/output behavior. The approach relies on a bounded SAT-based paradigm which represents every handled program by a program netlist. Experimental results show the effectiveness of the proposed technique for industrial low-level software in relevant equivalence checking scenarios such as code porting and automated/manual code transformations.