A Unified Model-Based Framework for the Simplified Execution of Static and Dynamic Assertion-Based Verification

Abstract

The improved productivity and reduced time-to-market are essential requirements for the development of modern embedded systems and, therefore, the comprehensive as well as timely design verification is critical. Assertion Based Verification (ABV) is a renowned paradigm to timely achieve an optimum test coverage, either through static or dynamic techniques. However, the major limitation with ABV is its inherited low-level implementation complexity. In order to simplify its execution, various Model Based System Engineering approaches provide a higher abstraction layer. Nevertheless, the complete verification requirements, targeting the static as well as dynamic ABV at the same time in a unified framework, are not being addressed. Furthermore, the dynamic verification support is provided through some traditional languages (like C, Verilog) where the advanced ABV features cannot be exploited. Consequently, this article introduces the MODEVES (MOdel-based DEsign Verification for Embedded Systems) framework to simultaneously support the static and dynamic ABV. Particularly, the UML (Unified Modeling Language) and SysML (Systems Modeling Language) diagrams are used to model the structural and behavioral requirements. Moreover, the NLCTL (Natural Language for Computation Tree Logic) is proposed to include the verification requirements for static ABV while the SVOCL (SystemVerilog in Object Constraint Language) is used to represent the dynamic verification constraints. An open source transformation engine is developed to automatically generate the SystemVerilog Register Transfer Level (RTL) code, Timed Automata model, SystemVerilog assertions and Computation Tree Logic (CTL) assertions with minimum transformation losses. The significance of the MODEVES framework is established through several case studies and the quantitative analysis shows an improvement of almost 100% in design productivity, as compared to the conventional low-level implementations.

Keywords

• Assertion based verification
• computation tree logic
• embedded systems
• model based system engineering
• systemverilog assertions
• timed automata