4.2 Timing in System-Level Modeling and Simulation

Time	Label	Presentation Title Authors
17:00	4.2.1	FAST AND ACCURATE DRAM SIMULATION: CAN WE FURTHER ACCELERATE IT? Speaker: Matthias Jung, Fraunhofer IESE, DE Authors: Johannes Feldmann¹, Matthias Jung², Kira Kraft¹, Lukas Steiner¹ and Norbert Wehn¹ ¹TU Kaiserslautern, DE; ²Fraunhofer IESE, DE Abstract Virtual platforms are state-of-the-art for design space exploration and simulation of today's complex System on Chips (SoCs). The challenge of these virtual platforms is to find the right trade-off between speed and accuracy. For the simulation of Dynamic Random Access Memories (DRAMs), that have a complex timing and power behavior, high accuracy models are needed. However, cycle accurate DRAM models require a huge part of the overall simulation time. Therefore, it is important to accelerate the DRAM simulation models while keeping the accuracy. In the literature different approaches to accelerate the DRAM simulation speed in virtual platforms do already exist. This paper proposes two new performance optimized DRAM models that further accelerate the simulation speed with only a negligible degradation in accuracy. The first model is an enhanced Transaction Level Model (TLM), which uses a look-up table to accelerate simulation parts with high bandwidth usage for online scenarios. The other is a neural network based simulator for offline trace analysis. We show a mathematical methodology to generate the inputs for the look-up table and the optimal artificial training set for the neural network. The TLM model is up to 5~times faster compared to a state-of-the-art TLM DRAM simulator. The neural network is able to speed up to~10x, while inferring on a GPU. Both solutions provide only a slight decrease in accuracy of approximately 5%. Download Paper (PDF; Only available from the DATE venue WiFi)
17:30	4.2.2	ACCURATE AND EFFICIENT CONTINUOUS TIME AND DISCRETE EVENTS SIMULATION IN SYSTEMC Speaker: Breytner Fernandez-Mesa, TIMA Laboratory, University Grenoble Alpes, FR Authors: Breytner Fernandez-Mesa, Liliana Andrade and Frédéric Pétrot, TIMA Lab, Université Grenoble Alpes, FR Abstract The AMS extensions of SystemC emerged to aid the virtual prototyping of continuous time and discrete event heterogeneous systems. Although useful for a large set of use cases, synchronization of both domains through a fixed timestep generates inaccuracies that cannot be overcome without penalizing simulation speed. We propose a direct, optimistic, and causal synchronization algorithm on top of the SystemC kernel that explicitly handles the rich set of interactions that occur in the domain interface. We test our algorithm with a complex nonlinear automotive use case and show that it breaks the described accuracy and efficiency trade-off. Our work enlarges the applicability range of SystemC AMS based design frameworks. Download Paper (PDF; Only available from the DATE venue WiFi)
18:00	4.2.3	MODELING AND VERIFYING UNCERTAINTY-AWARE TIMINGBEHAVIORS USING PARAMETRIC LOGICAL TIME CONSTRAINT Speaker: Fei Gao, East China Normal University, CN Authors: Fei Gao¹, Mallet Frederic², Min Zhang¹ and Mingsong Chen³ ¹East China Normal University, CN; ²Universite Cote d'Azur, CNRS, Inria, I3S, Nice, France, FR; ³East China Normal University, FR Abstract The Clock Constraint Specification Language (CCSL) is a logical time based modeling language to formalize timing behaviors of real-time and embedded systems. However, it cannot capture timing behaviors that contain uncertainties, e.g., uncertainty in execution time and period. This limits the application of the language to real-world systems, as uncertainty often exists in practice due to both internal and external factors. To capture uncertainties in timing behaviors, in this paper we extend CCSL by introducing parameters into constraints. We then propose an approach to transform parametric CCSL constraints into SMT formulas for efficient verification. We apply our approach to an industrial case which is proposed as the FMTV (Formal Methods for Timing Verification) Challenge in 2015, which shows that timing behaviors with uncertainties can be effectively modeled and verified using the parametric CCSL. Download Paper (PDF; Only available from the DATE venue WiFi)
18:30	IP2-3, 831	FAST AND ACCURATE PERFORMANCE EVALUATION FOR RISC-V USING VIRTUAL PROTOTYPES Speaker: Vladimir Herdt, University of Bremen, DE Authors: Vladimir Herdt¹, Daniel Grosse² and Rolf Drechsler² ¹University of Bremen, DE; ²University of Bremen / DFKI, DE Abstract RISC-V is gaining huge popularity in particular for embedded systems. Recently, a SystemC-based Virtual Prototype (VP) has been open sourced to lay the foundation for providing support for system-level use cases such as design space exploration, analysis of complex HW/SW interactions and power/timing/performance validation for RISC-V based systems. In this paper, we propose an efficient core timing model and integrate it into the VP core to enable fast and accurate performance evaluation for RISC-V based systems. As a case-study we provide a timing configuration matching the RISC-V HiFive1 board from SiFive. Our experiments demonstrate that our approach allows to obtain very accurate performance evaluation results while still retaining a high simulation performance. Download Paper (PDF; Only available from the DATE venue WiFi)
18:31	IP2-4, 641	AUTOMATED GENERATION OF LTL SPECIFICATIONS FOR SMART HOME IOT USING NATURAL LANGUAGE Speaker: Shiyu Zhang, Nanjing University, CN Authors: Shiyu Zhang¹, Juan Zhai¹, Lei Bu¹, Mingsong Chen², Linzhang Wang¹ and Xuandong Li¹ ¹Nanjing University, CN; ²East China Normal University, CN Abstract Ordinary inexperienced users can build their smart home IoT system easily nowadays, but such user-customized systems could be error-prone. Using formal verification to prove the correctness of such systems is necessary. However, to conduct formal proof, formal specifications such as Linear Temporal Logic (LTL) formulas have to be provided, but ordinary users cannot author LTL formulas but only natural language. To address this problem, this paper presents a novel approach that can automatically generate formal LTL specifications from natural language requirements based on domain knowledge and our proposed ambiguity refining techniques. Experimental results show that our approach can achieve a high correctness rate of 95.4% in converting natural language sentences into LTL formulas from 481 requirements of real examples. Download Paper (PDF; Only available from the DATE venue WiFi)
18:30		End of session

Time

Label

Presentation Title
Authors

17:00

4.2.1

FAST AND ACCURATE DRAM SIMULATION: CAN WE FURTHER ACCELERATE IT?
Speaker:
Matthias Jung, Fraunhofer IESE, DE
Authors:
Johannes Feldmann¹, Matthias Jung², Kira Kraft¹, Lukas Steiner¹ and Norbert Wehn¹
¹TU Kaiserslautern, DE; ²Fraunhofer IESE, DE
Abstract
Virtual platforms are state-of-the-art for design space exploration and simulation of today's complex System on Chips (SoCs). The challenge of these virtual platforms is to find the right trade-off between speed and accuracy. For the simulation of Dynamic Random Access Memories (DRAMs), that have a complex timing and power behavior, high accuracy models are needed. However, cycle accurate DRAM models require a huge part of the overall simulation time. Therefore, it is important to accelerate the DRAM simulation models while keeping the accuracy. In the literature different approaches to accelerate the DRAM simulation speed in virtual platforms do already exist. This paper proposes two new performance optimized DRAM models that further accelerate the simulation speed with only a negligible degradation in accuracy. The first model is an enhanced Transaction Level Model (TLM), which uses a look-up table to accelerate simulation parts with high bandwidth usage for online scenarios. The other is a neural network based simulator for offline trace analysis. We show a mathematical methodology to generate the inputs for the look-up table and the optimal artificial training set for the neural network. The TLM model is up to 5~times faster compared to a state-of-the-art TLM DRAM simulator. The neural network is able to speed up to~10x, while inferring on a GPU. Both solutions provide only a slight decrease in accuracy of approximately 5%.
Download Paper (PDF; Only available from the DATE venue WiFi)

17:30

4.2.2

ACCURATE AND EFFICIENT CONTINUOUS TIME AND DISCRETE EVENTS SIMULATION IN SYSTEMC
Speaker:
Breytner Fernandez-Mesa, TIMA Laboratory, University Grenoble Alpes, FR
Authors:
Breytner Fernandez-Mesa, Liliana Andrade and Frédéric Pétrot, TIMA Lab, Université Grenoble Alpes, FR
Abstract
The AMS extensions of SystemC emerged to aid the virtual prototyping of continuous time and discrete event heterogeneous systems. Although useful for a large set of use cases, synchronization of both domains through a fixed timestep generates inaccuracies that cannot be overcome without penalizing simulation speed. We propose a direct, optimistic, and causal synchronization algorithm on top of the SystemC kernel that explicitly handles the rich set of interactions that occur in the domain interface. We test our algorithm with a complex nonlinear automotive use case and show that it breaks the described accuracy and efficiency trade-off. Our work enlarges the applicability range of SystemC AMS based design frameworks.
Download Paper (PDF; Only available from the DATE venue WiFi)

18:00

4.2.3

MODELING AND VERIFYING UNCERTAINTY-AWARE TIMINGBEHAVIORS USING PARAMETRIC LOGICAL TIME CONSTRAINT
Speaker:
Fei Gao, East China Normal University, CN
Authors:
Fei Gao¹, Mallet Frederic², Min Zhang¹ and Mingsong Chen³
¹East China Normal University, CN; ²Universite Cote d'Azur, CNRS, Inria, I3S, Nice, France, FR; ³East China Normal University, FR
Abstract
The Clock Constraint Specification Language (CCSL) is a logical time based modeling language to formalize timing behaviors of real-time and embedded systems. However, it cannot capture timing behaviors that contain uncertainties, e.g., uncertainty in execution time and period. This limits the application of the language to real-world systems, as uncertainty often exists in practice due to both internal and external factors. To capture uncertainties in timing behaviors, in this paper we extend CCSL by introducing parameters into constraints. We then propose an approach to transform parametric CCSL constraints into SMT formulas for efficient verification. We apply our approach to an industrial case which is proposed as the FMTV (Formal Methods for Timing Verification) Challenge in 2015, which shows that timing behaviors with uncertainties can be effectively modeled and verified using the parametric CCSL.
Download Paper (PDF; Only available from the DATE venue WiFi)

18:30

IP2-3, 831

FAST AND ACCURATE PERFORMANCE EVALUATION FOR RISC-V USING VIRTUAL PROTOTYPES
Speaker:
Vladimir Herdt, University of Bremen, DE
Authors:
Vladimir Herdt¹, Daniel Grosse² and Rolf Drechsler²
¹University of Bremen, DE; ²University of Bremen / DFKI, DE
Abstract
RISC-V is gaining huge popularity in particular for embedded systems. Recently, a SystemC-based Virtual Prototype (VP) has been open sourced to lay the foundation for providing support for system-level use cases such as design space exploration, analysis of complex HW/SW interactions and power/timing/performance validation for RISC-V based systems. In this paper, we propose an efficient core timing model and integrate it into the VP core to enable fast and accurate performance evaluation for RISC-V based systems. As a case-study we provide a timing configuration matching the RISC-V HiFive1 board from SiFive. Our experiments demonstrate that our approach allows to obtain very accurate performance evaluation results while still retaining a high simulation performance.
Download Paper (PDF; Only available from the DATE venue WiFi)

18:31

IP2-4, 641

AUTOMATED GENERATION OF LTL SPECIFICATIONS FOR SMART HOME IOT USING NATURAL LANGUAGE
Speaker:
Shiyu Zhang, Nanjing University, CN
Authors:
Shiyu Zhang¹, Juan Zhai¹, Lei Bu¹, Mingsong Chen², Linzhang Wang¹ and Xuandong Li¹
¹Nanjing University, CN; ²East China Normal University, CN
Abstract
Ordinary inexperienced users can build their smart home IoT system easily nowadays, but such user-customized systems could be error-prone. Using formal verification to prove the correctness of such systems is necessary. However, to conduct formal proof, formal specifications such as Linear Temporal Logic (LTL) formulas have to be provided, but ordinary users cannot author LTL formulas but only natural language. To address this problem, this paper presents a novel approach that can automatically generate formal LTL specifications from natural language requirements based on domain knowledge and our proposed ambiguity refining techniques. Experimental results show that our approach can achieve a high correctness rate of 95.4% in converting natural language sentences into LTL formulas from 481 requirements of real examples.
Download Paper (PDF; Only available from the DATE venue WiFi)

18:30

End of session