Verification of systemc components using the method of deduction

Abstract

The verification of the embedded systems would play an important role in its scenario of manufacturing. The SystemC language of the embedded systems material description became the basic language of most of industrial productions companies. This allows several research works to focus on the verification methods of the SystemC designs. The formal verification that bases on mathematical proofs is a powerful method to describe the existence or the absence of the designs errors. It is a combination of two parallel and in collaboration operations; the first one is the specification of the generic and specific properties of the system under a formal language, the second is the description of its behavior under state-transition representations. In spite of its mathematical power, it knows limitations in terms of the systems length. It enters in the type of the state explosion problems that effect on the speed of the check. In this paper, we represent a new approach of verifying the SystemC designs using SPIN Model Checker, based on the deduction method that extract the executions of equivalence “scenarios of equivalence” through which we can deduct the satisfaction or the non-satisfaction of the systems specification.