| Title | Evaluation of Runtime Monitoring Methods for Real-Time Event Streams |
| Author | *Biao Hu, Kai Huang, Gang Chen, Alois Knoll (Technical University of Muenchen, Germany) |
| Page | pp. 582 - 587 |
| Keyword | Runtime Monitor, dynamic counter, l-repetitive function, FPGA |
| Abstract | Runtime monitoring is of great importance as a safe guard to
guarantee the correctness of system runtime behaviors. Two new
methods, i.e., dynamic counters and l-repetitive function, are
recently developed to tackle the runtime monitoring for hard
real-time systems. This paper investigates in depth these two newly developed runtime monitoring methods, trying to evaluate and
identify their strengths and weaknesses. Representative scenarios are used as our case studies to quantitatively demonstrate our
comparisons. We also provide FPGA implementations and resource usages of both methods. |
| Slides |
| Title | Automatic Timing-Coherent Transactor Generation for Mixed-Level Simulations |
| Author | *Li-chun Chen, Hsin-I Wu, Ren-Song Tsay (National Tsing Hua University, Taiwan) |
| Page | pp. 588 - 593 |
| Keyword | Mixed-level simulations, ESL, system simulators, transactor, timing coherent |
| Abstract | In this paper we extend the concept of the traditional transactor, which focuses on correct content transfer, to a new timing-coherent transactor that also accurately aligns the timing of each transaction boundary so that designers can perform precise concurrent system behavior analysis in mixed-abstraction-level system simulations which are essential to increasingly complex system designs. To streamline the process, we also develop an automatic approach for timing-coherent transactor generation. Our approach is actually applied in mixed-level simulations and the results show that it achieves 100% timing accuracy while the conventional approach produces results of 25% to 44% error rate. |
| Slides |
| Title | Hybrid Coverage Assertions for Efficient Coverage Analysis Across Simulation and Emulation Environments |
| Author | Hsuan-Ming Chou, Hong-Chang Wu, Yi-Chiao Chen, *Jean Tsao, Shih-Chieh Chang (National Tsing Hua University, Taiwan) |
| Page | pp. 594 - 599 |
| Keyword | coverage analysis, assertion, hardware-accelerated environment |
| Abstract | Coverage metrics are used to measure the completeness of the verification tests. However, in a modern hardware-accelerated environment, coverage may be analyzed across a simulator and an emulator. Hence, conventional coverage techniques can be directly applied. To resolve the above problem, we propose using coverage assertions to detect coverage events across a simulator and an emulator. In addition, an Assertion Operation Graph and graph-based algorithms are proposed to minimize the hardware and performance overheads of coverage assertions. |
| Slides |
| Title | SWAT: Assertion-Based Debugging of Concurrency Issues at System Level |
| Author | *Luis Gabriel Murillo, Róbert Lajos Bücs, Daniel Hincapie, Rainer Leupers, Gerd Ascheid (RWTH Aachen University, Germany) |
| Page | pp. 600 - 605 |
| Keyword | Many-core, Concurrency, Debug, HW/SW, Virtual Platforms |
| Abstract | Modern multi- and many-core systems are prone to concurrency-related bugs which surface only at system level. Detecting these bugs might require dealing with low-level hardware (HW) protocols and/or software (SW) inter-task interactions. Virtual platforms (VPs) offer a viable vehicle to conveniently debug HW/SW functionality, yet developers are mostly limited to manually break-point, step and interact with the system. To ease debugging during integration at system level, this paper introduces SWAT, an assertion-based debugging framework that checks and correlates system-wide interactions among HW and SW components. SWAT is used together with VPs to enable detecting HW and/or SW concurrency bugs with lower effort than existing techniques. Our proposed approach is evaluated in two state-of-the-art platforms running real-world SW stacks. |
| Title | Communication Protocol Analysis of Transaction-Level Models Using Satisfiability Modulo Theories |
| Author | *Che-Wei Chang, Rainer Doemer (University of California, Irvine, U.S.A.) |
| Page | pp. 606 - 611 |
| Keyword | TLM, SMT, Verfication, AMBA bus, CAN bus |
| Abstract | A critical aspect in SoC design is the correctness of
communication between system blocks. In this work, we present
a novel approach to formally verify various aspects of communication
models, including timing constraints and liveness. Our
approach automatically extracts timing relations and constraints
from the design and builds a Satisfiability Modulo Theories (SMT)
model whose assertions are then formally verified along with
properties of interest input by the designer. Our method also addresses
the complexity growth with a hierarchical approach. We
demonstrate our approach on models communicating over industry
standard bus protocol AMBA AHB and CAN bus. Our results
show that the generated assertions can be solved within resonable
time. |
| Slides |