is the formalisation of a reasonable subset of SystemC based on classical process algebras. During the last few years, has been successfully used to give formal specifications of SystemC designs. For formal analysis purposes, so far, users have been required to transform manually their SystemC codes into corresponding specifications. To verify some desired properties of specifications using existing formal verification tools (e.g. NuSMV and SPIN), similarly, manual translations have been needed for turning specifications into corresponding terms of the input language (e.g. SMV and PROMELA) of the selected formal verification tool. Since manual transformation and translations between SystemC codes, specifications, and various formalisms are quite laborious and therefore error-prone, these translations have to be made as much automatic as possible. The first step of the research in these directions is to automate the transformation from SystemC codes to specifications. In this paper, we present SC2SCFL (an automatic translation tool), which converts SystemC codes into corresponding specifications.