SystemC～(FL) Modeling Verification Of Hardware Design System Using The SPIN Model Checker

As the complexity of system design increases, disign verification has become the bottle-neck of the system design;the traditional verification technology has not been satisfied with the need, however, formalization verification technology is a new technology to suit this need. Formalization verification methods include arithmetic verification, attribute verification, and equivalence verification etc. Our research field is attribute verification, including theorem provement, language inclusion and symbol model checker etc. The common symbol model checkers are CTL model checkers, such as SMV verification implemention, and LTL model checkers such as SPIN verification implemention.SPIN, which is a software verification implemention, is developed by J.Holzmann in Bell Laboratory in 1989. It's used for distributed software and the verification of protocol system. SPIN makes use of PROMELA as the verification model language, LTL formula to describe attributes, and automatism theory to realize the systemic simulation and correctness verification.In the process of system verification with SPIN, the first is building system state machine model in PROMELA language, then abstract the formalizatoin description decribed by LTL formula. The system correctness demand attributes also can be described by special signs of PROMELA. The target of verification is to judge that sytem model whether matches up to the abstract attributes or not.The formal language SystemC^FL is the formalization of a reasonable subset of SystemC based on classical process algebra ACP. It express both SystemC modeling semantics and the process analysis of behaviors in SystemC modeling . SystemC^FL may modeling to kinds of system( finite state system, real-time system).For verification of concurrent systems and hardware designs modeled in SystemC^FL, in this paper, we present an approach to use the SPIN model checker as a verification engine for SystemC^FL designs (modeling concurrent systems and hardware designs), by translating them to PROMELA that is the input language of SPIN. We illustrate the practical interest of our approach with a case studies: a hazardous circuit.