SystemC^FL: Formal specification and analysis of hardware /software co-designs

SystemC^FL is a formal language for hardware/software co-design. Principally, SystemC^FL is the formalization of SystemC based on classical process algebra ACP. The language is aimed to give formal specification of SystemC designs and perform formal analysis of SystemC processes. Furthermore, SystemC^FL is a single-formalism that can be specifically used for specifying concurrent systems, finite state systems and real-time systems. Desired properties of these systems modeled in SystemC^FL can be verified with existing formal verification tools by translating them formally into different formalisms that are the input languages of the formal verification tools. This paper provides an overview of SystemC^FL and shows some practical applications of SystemC^FL.