FDL 2018

Forum on specification & Design Languages

@Munich, Germany
September 10-12, 2018

@Munich, Germany


Rainer Domer
University of California, Irvine

1st Keynote: On the Limits of Standard-compliant Parallel Simulation of the IEEE SystemC Language

The IEEE standard 1666 [1] defines SystemC as a C++ class library for system and hardware design. Unfortunately SystemC simulation is based on sequential co-routine semantics, despite the explicit parallelism available in its design models. This imposes strict limits on standard-compliant parallel simulation which obstruct designers’ efforts to increase execution speed by utilizing multi- and many-core host platforms. In this keynote, we discuss seven obstacles [2] identified in the SystemC standard that stand in the way of efficient parallel simulation, including the co-operative multitasking semantics, the weak role of channels, TLM-2.0, and an overall sequential modeling mindset. Thus, truly parallel SystemC appears elusive given the current IEEE standard. Accepting this fact, we can only make the best of it and design parallel SystemC approaches in maximum compliance with the standard.
As an example, we present the Recoding Infrastructure for SystemC (RISC) [3]. RISC is an open source CAD software package that provides a dedicated compiler and simulator for SystemC with out- of-order parallel execution engine, yet maintains the classic transaction level modeling semantics. Experimental results show that RISC can efficiently exploit thread- and data-level parallelism in SystemC models resulting in several hundred times higher simulation speed [4]. We also highlight recent advances in scaling the RISC approach to support large design models with 3rd party library code.

[1] IEEE Computer Society. “IEEE Standard 1666-2011 for Standard SystemC Language Reference Manual”, IEEE, New York, USA, 2011.
[2] R. Dömer: "Seven Obstacles in the Way of Standard-Compliant Parallel SystemC Simulation", IEEE Embedded Systems Letters, vol. 8, no. 4, pp. 81-84, December 2016.
[3] RISC project web site: http://www.cecs.uci.edu/~doemer/risc.html
[4] T. Schmidt, G. Liu, R. Dömer: "Exploiting Thread and Data Level Parallelism for Ultimate Parallel SystemC Simulation", Proceedings of the Design Automation Conference (DAC) 2017, Austin, TX, June 2017.
[5] T. Schmidt, Z. Cheng, R. Dömer: "Port Call Path Sensitive Conflict Analysis for Instance-Aware Parallel SystemC Simulation", Proceedings of the Design, Automation and Test in Europe (DATE) Conference 2018, Dresden, Germany, March 2018.

Rainer Dömer received his Ph.D. degree in Information and Computer Science from the University of Dortmund, Germany, in 2000. He is currently a full Professor in Electrical Engineering and Computer Science at the University of California, Irvine (UCI). He is also a member of the Center for Embedded and Cyber-physical Systems (CECS) at UCI. His research interests include system-level design and methodologies, embedded computer systems, specification and modeling languages, advanced parallel simulation, and the integration of hard- and software systems. Rainer Dömer received the prestigious NSF CAREER Award for his research on efficient modeling of embedded computer systems in 2008, the EECS Faculty of the Year award in 2013, the Best Paper award at the Design, Automation and Test in Europe (DATE) conference in 2014, and the Faculty Innovation in Teaching Mid-Career Award in 2016.

- Web page: http://www.cecs.uci.edu/~doemer/

Jean-Pierre Talpin
INRIA, France

2st Keynote: Refinement types for system design

"Clean-slate" programming environments are now invading territories of general-purpose software development: F*, Liquid Haskell, TypeScript, and to different extends CompCert, Cogent, or even Frama-C, are open-source projects offering one to combine the programming or specification of an application with the proof of its correctness, up to logical requirements specified as dependent types or assertions.
Yet, "shallow" verification with the former languages, as some name it, does not come close to theorem-prover-mechanized certified development with the latter provers, as some advocate. However, the emergence of Cogent (co-generation of program and proof from specification) in SeL4 and, similarly, layered abstractions in CertikOS, manifest the need for modularity and proof abstraction to make verified programming tenable for scalable developments: the SeL4 project revealed the barrier of a quadratic growth of proof obligations w.r.t. the size of code to verify.
And yet, again, modular proof abstraction doesn't seem so different than matured practices of interface-based design, contract-based design, correctness-by-construction, that are most known to the system design community and have been advocated for a decade. Unsurprisingly, this infatuation faced similar quadratic barriers, resulting from the use of automata-based formalisms, and most scaled applications of these methods instead use logical modulo-theory assume-guarantee reasoning.
Clean-state languages are the tools that combine both specification, abstraction and proof capacities by the notion of refinement type {v:Int| v>0} to, e.g., denote the values v of type Int that are strictly positive, and *assume* a function to be called with such numbers and give the opposite *guarantee* on its result: x:{v:Int| v>0} -> {w:Int| w<0}, ergo for arrays, pointers, streams, threads, exceptions, the TLS protocol.
The aim of this keynote is to give the (system) design language community a gentle introduction to the notion of refinement types, at the core of these general-purpose environment, and to demonstrate the potential benefits of such tools in system design by a highlight of orchestrated works in progress in my group: team TEA, and in collaborations with UC San Diego, University of Maryland, IETR, MERCE, the Chinese Academy of Science and Beihang University.

Jean-Pierre Talpin is senior scientist with INRIA and scientific leader of INRIA project TEA. Graduated in Applied Mathematics, he received a Master in Theoretical Computer Science from University Paris VI and did his Ph.D. Thesis at Ecole des Mines de Paris under the supervision of Pierre Jouvelot. He then worked three years as research associate at the European Computer-Industry Research Centre in Munich. He joined INRIA in 1995 and led Inria project ESPRESSO from 2000 to 2012. He is associate editor with the ACM Transaction on Embedded Compter Systems. He edited three books, guest-edited a dozen of scientific journal special issues with ACM and IEEE and authored more than a hundred journal articles, book chapters and conference papers. He received the 2004 ACM Award for the most influential POPL paper, with Mads Tofte, and the 2012 ACM/IEEE LICS Test of Time Award, with Pierre Jouvelot, for his early-carrier work on region inference and region-based memory management. He is the only recipient of both of these awards.

- Web page: http://www.irisa.fr/prive/talpin/

Franz-Josef Grosch
Robert Bosch GmbH

3st Keynote: Blech - a safe synchronous language for embedded real-time programming

Product development at companies such as Bosch requires systems engineering for digital hardware and mechatronic components as well as software engineering for deeply-embedded resource-constrained real-time applications cooperating with distributed cloud applications. While many of the involved engineering disciplines greatly benefit from model-based approaches and from advances in software infrastructures, deeply embedded software is still based on manually written C code, a few components generated from models and glued together with the help of an embedded operating systems like OSEK. Making software safe with the help of tight coding conventions and static analyzers is a time-consuming task. Modern implementation technologies to address software architecture and qualities or to make embedded programming appealing for software professionals are largely missing. We regard synchronous languages to be suitable for solving many of the issues in the integration (causality) and synchronization (clocks) of time-triggered and event-triggered embedded functions that exhibit their behavior over time steps and are coordinated according to their mode-switching in a structured synchronous control flow. Unfortunately, existing synchronous languages do not support modern implementations technologies well such as aggregated data types, object-based programming and separate compilation. Searching for an imperative, strongly-typed, synchronous language (with deterministic concurrent composition, and synchronous control flow), equipped with the aforementioned features for encapsulation and composition (aggregated data types, modules, separate compilation) and supporting programming parallel tasks deployed to separate cores (clock refinement and deterministic inter-task communication), we ended up in designing our own language, suitable for resource-constrained, real-time applications running on multi-core controllers. In this keynote, we will illustrate requirements and features of this language: The realization of synchronous control flow with a focus on separate compilation, a practical way of integrating aggregated data types like arrays, records and references without obstructing causality analysis, and our approach to task-parallel programming. The language design and the compiler implementation is work in progress.

Franz-Josef Grosch is a senior expert at the Bosch Corporate Research campus in Renningen. He studied Computer Science at TU Darmstadt and TU Braunschweig. Franz-Josef worked for several companies as a researcher and software developer. Currently, he works in a department focused on model-based system engineering in the area of software-intensive systems and technologies. The team advances engineering methods for Bosch products that require multi-disciplinary collaboration of engineers and software developers. In this inspiring environment he focuses on improving programming and software engineering for deeply embedded resource-constraint real-time systems. In his current project his team develops a programming language in this area, with the intention to promote modern implementation technologies and to make embedded programming "attractive" for software professionals.

- Web page: https://www.linkedin.com/in/franzjosefg/


Jan Kuper
QBayLogic, Enschede, The Netherlands

Title: FPGA Design with CLaSH

Recent years have shown an enormous increase in the usage of FPGAs. Unfortunately, the programming methodology for FPGAs has not developed with the same pace, the overwhelming majority of hardware designers still use VHDL or (System) Verilog, where both languages are of a very low level with poor abstraction mechanisms. In practice, many attempts are made for high level synthesis (HLS) tools, to generate VHDL/Verilog from traditional programming languages such as C, C++, Python. However, the essential structure of such languages does not fit an FPGA well and designing an FPGA by means of most HLS systems is a cumbersome task. As an aternative to this, CLaSH is a recently developed tool to design FPGAs based on the programming language Haskell. CLaSH too generates VHDL or Verilog from a Haskell specification, but as a consequence of the fact that Haskell is a functional programming language, it is much closer to hardware architecture than an imperative language. Hence, FPGA design in Haskell is more straightforward than by using an HLS system. In addition, Haskell has powerful abstraction mechanisms such as higher order functions, polymorphism, lambda abstraction, and offers features such as the definability of domain specific embedded languages, and the possibility to apply mathematical transformations on a given design in order to optimize the design. The result is that by using CLaSH FPGA designs can be developed with far less effort than hand-written VHDL/Verilog, and still having the same performance characteristics. An important advantage of CLaSH, in comparison with VHDL/Verilog, is further that a CLaSH specification can be easily simulated. In fact, the development of a design in CLaSH goes hand-in-hand with simulation and testing. During the tutorial we will introduce CLaSH by various examples, ranging from mathematical problems to the specification of small processors. If time allows we will demonstrate the actual usage of an FPGA. It will be practical if participants have some preliminary knowledge of Haskell, but that is by no means necessary.

Dr. Jan Kuper received his M.Sc. degree (with honours) at the University of Twente in the area of Mathematics and Logics in 1985. In 1994, he got his Ph.D. thesis on the foundations of Mathematics and Computer Science under the supervision of Prof.dr. Henk Barendregt. Until 2016 he was a lecturer at the Universities of Leiden and Enschede, performing research in formal methods in computer science. Since 2007 his research concentrated on the mathematical specification of hardware architectures, which -- in co-operation with several PhD-students -- resulted in the hardware specification system CLaSH. In 2016 he, together with Dr. Cristiaan Baaij, started the company QBayLogic to exploit CLaSH.

- Web page: http://www.qbaylogic.com/our-team.html

Karsten Einwich

Title: Heterogeneous System Level Modelling Techniques for Fast Virtual Prototypes

State of the Art semiconductor technologies are the enabler for a cost-effective realization of more and more sophisticated systems. Software in conjunction with analog and digital electronics will directly assist and interact in tight control loops with physical components like mechanics. The better those interactions will be understood and managed the better will those costs for expensive e.g. mechanical components be saved due to their simplification. New innovative features can be realized, and aging as well as wearing can be compensated increasing the overall reliability and safety. This is important for all emerging application areas, where electronics interact directly with the environment like industry 4.0, IoT and automotive including autonomous driving. Virtual prototyping is one of the core technologies to manage the increasing complexity cost-efficiently. Virtual prototypes have many advantages as they are very early available in the design process and therefore especially allow to start the software development even before hardware is available, they are completely introspect able, and they allow to answer what-if questions easily. Verification scenarios created on virtual prototypes are reproducible, and corner cases, which cannot be practically realized in hardware, can be checked. Furthermore, verification runs can be integrated in a continuous integration environment. Due to the emerging applications, virtual prototypes must also include besides digital hard- software components the analog electronics and the physical environment of the system. A practical virtual prototype must be able to simulate complete application scenarios of the complete electronic hard- software system and the relevant physical environment in an acceptable timeframe. To achieve such performance the application of system level modelling techniques is required. For digital components, those are techniques like TLM (transaction level modelling) or just in time compilation. With this tutorial, we will destroy the myth, that when analog components are added to the system, the performance of a virtual prototype will become always slow. Similar to the digital domain also for analog and physical components abstraction techniques are available. When using such techniques, performance of analog components does not slow down the overall system; the computation effort of the analog part even can become negligible compared to the usually dominating digital part. The tutorial will discuss and demonstrate the application and combination of different system level modelling techniques using the IEEE standardized SystemC and SystemC AMS language. Thereby, the tutorial will concentrate on the underlying modelling techniques and principles rather than on the language aspects. Using practical examples the modelling techniques will be explained and the attendees will perform lab exercises to acquire hands-on knowledge. Lab exercises will be performed in the system level-modelling environment COSIDE® to also demonstrate examples that are more complex.

Karsten Einwich is CEO of COSEDA Technologies, a company based in Germany that provides software solutions in the field of system level design for complex electronic hard- & software products. Karsten Einwich has more than 25 years of experience in the field of modelling, simulation and verification of complex heterogeneous systems. During his over 20 years at the Fraunhofer Institute for Integrated Circuits IIS, Division Engineering of Adaptive Systems he managed a research group which developed methods and tools for the design of electronic hard- & software components in the context of the whole system. Karsten Einwich was deeply involved in the development and standardization process (IEEE & Accellera) of the SystemC AMS modelling and simulation technology. His activities in various national and international industrial as well as academic projects over the past 25 years have made him a highly recognized expert in in the field of how to make latest system modeling, simulation, design and verification methodologies efficient, practical and usable.

- Website: https://www.coseda-tech.com/index.php

FDL 2018 is in Munich, Germany