Abstract
The UML and its associated profiles like MARTE and SysML provide a general framework to model and analyze embedded systems. Though mostly used for modeling, MARTE is equally capable of design verification techniques. The Clock Constraint Specification Language (CCSL) annexed to the MARTE provides the notion of logical time to model heterogeneous and concurrent systems and to address their time-related semantic issues. This paper advocates the use of CCSL to express the safety properties of UML/MARTE/SysML models and presents an automatic transformation of selected CCSL operators into equivalent SystemVerilog assertions. This contribution bridges the gap between the abstract CCSL specifications modeling causality relations and the RTL-based SystemVerilog assertions, hence achieving early design validation. SystemVerilog being a popular hardware description and verification language allows us to integrate the verification features in a classical design flow. In the end, the utility of the presented approach is demonstrated with the help of a case study.