A Model Driven Framework with Assertion Based Verification Support for Embedded Systems Design Automation

Abstract

Over the past decade, due to significant technological advancements, the complexity and demand of embedded systems is growing exponentially. Consequently, industries dealing with the development of embedded systems are under continual pressure to achieve improved productivity and reduced time-to-market. Therefore, a comprehensive and just-in-time design & verification becomes critical. To tackle this requirement, Assertion Based Verification (ABV) has emerged as a promising paradigm, which allows verification in optimum timespan. Although, ABV improves the design verification time, it usually suffers from the low level implementation complexities and tend to delay overall design automation process. In this regard, Model Based System Engineering (MBSE) plays a vital role by providing higher abstraction layer for low level complex implementations. However, existing MBSE approaches for ABV, do not provide full verification coverage. Particularly, MBSE solutions for renowned low level ABV technologies like SystemVerilog are hard to find in the literature and industrial solutions. Furthermore, most of the existing MBSE approaches deal with either static ABV or dynamic ABV in isolation, whereas complex designs usually require the application of both static & dynamic ABV simultaneously. In order to resolve these design verification issues, this study proposes a novel and comprehensive MBSE framework for embedded systems to simplify and expedite the execution of ABV. Precisely, a unified MODEVES (MOdel-based DEsign Verification for Embedded Systems) framework has been developed to simultaneously support Static and Dynamic ABV through well-known Timed Automata formalism and SystemVerilog, respectively. Moreover, a complete end-to-end MODEVES Modeling Methodology (MMM) has been proposed, which includes, UMLSV (UML profile for SystemVerilog) and standard UML / SysML notations to model design requirements. Besides that, SVOCL (SystemVerilog in Object Constraint Language) and NLCTL (Natural Language for Computation Tree Logic) have been proposed to model the verification requirements for dynamic & static ABV, respectively. Finally, all these technologies are integrated in an open source MODEVES Transformation Engine (MTE) to automatically generate: 1) SystemVerilog Register Transfer Level (RTL) code, 2) Timed Automata model, 3) SVAs (SystemVerilog Assertions) and 4) CTL (Computation Tree Logic) assertions from the high level MMM-compliant models. v | P a g e Viability of MODEVES framework has been demonstrated through eight (8) benchmark case studies: Traffic Lights Controller, Car Collison Avoidance System, Arbiter, Elevator, Unmanned Aerial Vehicle, Automated Teller Machine (ATM), Train Gate and Bridge Crossing system. Subsequently, the quantitative analysis is performed to demonstrate that MODEVES has achieved on average 92% productivity gain, while executing both static and dynamic ABV, as compared to the conventional low-level implementations. To summarize, the results indicate that the MMM effectively enables the concurrent modeling of design & verification requirements for both static and dynamic ABV approaches. On the other hand, MTE is capable of generating low level target models from MMM-compliant source models automatically, allowing rapid static and / or dynamic ABV using the state-of-the-art tools like UPPAAL and QUESTASIM, respectively. Consequently, MODEVES significantly simplifies and speeds up the simultaneous execution of both static and dynamic ABV in early development phases without involving low level implementation complexities and improves the design productivity that eventually reduces timeto-market of embedded system products.