On Self-Verifying DSL Generation for Embedded Systems Automation

Abstract:
As various domain knowledge is prerequired, the embedded systems development is difficult. In the development process, multiple programming languages are used to develop different aspects such as hardware, firmware and formal verification. The semantic gap and inconsistent syntax among these languages escalate further the design efforts. We propose to generate Python-embedded Self-Verifying Domain-Specific Languages (DSLs) from metamodels. Domainspecific semantics are captured in metamodels. With additional configurations, domain-specific functionalities are included in DSLs. Further, tests are generated to assure the DSL quality. To demonstrate the applicability, the proposed approach is applied on an embedded system automation framework that generates hardware, firmware and formal properties for verification. An SoC was generated and verified with the automation framework. Minimal efforts were observed to achieve high code coverage for DSLs. Furthermore, our approach scales well with increasing domain complexity, i.e., the generation took less than 10 seconds for the most complex DSL (129.9k Lines of Code).