Formal verification of SystemC FL specifications using SPIN
Ka Lok Man · International Conference on Microelectronics · 2006
The formal language SystemCFL is the formalization of SystemC. The language semantics of SystemCFL was formally defined in a standard structured operational semantics (SOS) style. For verification purposes, in this paper, we present an approach to use the SPIN model checker as a verification engine for SystemCFL specifications, by translating SystemCFL specifications to PROMELA that is the input language of SPIN. We illustrate the practical interest of our approach with a case study: a hazardous circuit.