Formal Verification of SystemC-based Cyber Components
Cyber-Physical Systems (CPS) integrate physical and cyber components, where the latter are responsible for the computation part. Due to their steadily increasing complexity, these cyber components have to be modeled at high level of abstraction when creat
- PDF / 1,028,614 Bytes
- 31 Pages / 439.37 x 666.142 pts Page_size
- 46 Downloads / 205 Views
Introduction Cyber-Physical Systems (CPS) integrate physical and cyber components. These cyber components (e.g. HW/SW implementation of embedded control algorithms) are responsible for the computation part of CPS. Developing such complex components within todays time-to-market constraints requires building abstract models for architectural exploration and early software development. This procedure has been systematized resulting in the Electronic System Level (ESL) design [2]. For ESL design, SystemC [3] has become the standard modeling language and is nowadays being employed in various industries (including consumer electronics, automotive, industrial automation, etc.). SystemC is a C++ class library and provides modules, ports, interfaces and channels as the fundamental modeling components, whereas, the functionality is described by processes. In addition, the SystemC library also includes an event-driven simulation kernel. Essentially, the simulation kernel executes the processes non-preemptive and manages their parallel execution by using delta-cycles. Most crucial for the success of SystemC is the concept of Transaction Level Modeling (TLM) [4–6]. TLM enables the description of communication in terms of This chapter is an extended version of a conference paper appeared at MEMOCODE 2010 [1]. D. Große (✉) ⋅ H.M. Le ⋅ R. Drechsler University of Bremen, Bremen, Germany e-mail: [email protected] H.M. Le e-mail: [email protected] R. Drechsler e-mail: [email protected] D. Große ⋅ R. Drechsler DFKI Bremen, Bremen, Germany © Springer International Publishing Switzerland 2017 S. Jeschke et al. (eds.), Industrial Internet of Things, Springer Series in Wireless Technology, DOI 10.1007/978-3-319-42559-7_6
137
138
D. Große et al.
abstract operations (transactions). The simulation of SystemC TLM models is orders of magnitude faster in comparison to synthesizable HW models, which are implemented at Register Transfer Level (RTL) using e.g. VHDL or Verilog. Furthermore, TLM allows interoperability between models from different IP vendors. Please note that this chapter does not target any particular TLM library (e.g. TLM-2.0 standard) but handles TLM in a more general sense: we focus on SystemC TLM designs where communication is done through transactions (i.e. calling interface functions) and the synchronization is based on events. Clearly, an abstract SystemC TLM model provides the first formalization of the design specification. This first TLM model is usually untimed and is successively refined by adding timing information to a timed TLM model, which in turn is refined down to RTL. Therefore, potential bugs need to be identified already at TLM. However, this functional verification task is difficult [7]. Methods commonly applied at TLM rely on simulation (see e.g. [8–13]) and therefore cannot guarantee the functional correctness, which is of uttermost importance, if the cyber components under development will be integrated in safety-critical CPS. The existing formal verification approaches
Data Loading...
