报告题目：Formal Methods for ESL Verification
报告人：Daniel Große 博士
主持人：陈铭松 副教授
报告时间：2015年5月13日 周三 13:30—15:00
报告地点：中北校区数学馆201
报告人简介：
Daniel Große received the Dr. degree in Computer Science from the University of Bremen, Germany, in 2008. He remained as postdoctoral researcher in the group of Rolf Drechsler in Bremen. In 2010 he was a substitute professor for computer architecture at Albert-Ludwigs University, Freiburg, Germany. From 2013 to 2014 he was CEO of the EDA start-up solvertec focusing on automated debugging techniques. Currently, he is a senior researcher at the University of Bremen, Germany. He has over 10 years of experience in hardware verification. He published more than 70 peer-reviewed papers and served in several program committees like e.g. DATE, ICCAD, MEMOCODE and FDL. His research interests include verification, debugging, synthesis, and high-level languages like SystemC.
报告摘要：
Although embedded systems have witnessed a reduction of their development time and life time in the past decades, their complexity has been increasing steadily. Hence it has become a necessity to raise the level of abstraction beyond the traditional Register Transfer Level (RTL). This approach has been systematized and the Electronic System Level (ESL) design emerged. A widely accepted language for ESL design is SystemC. As a C++ library SystemC perfectly supports abstract modeling, in particular Transaction Level Modeling (TLM). In TLM the detailed communication of (hardware) components is abstracted into function calls. Based on TLM virtual prototypes of a system can be built and software development can be started in parallel to the hardware development. However, the productivity gain depends mainly on the correctness of ESL/TLM models, which serve as reference for both software and hardware development. Therefore effictive methods for functional verification of these models are inevitable.
In the first part of the talk an approach for property checking of TLM models is presented. Our approach allows a complete and efficient verification of “true” TLM properties. In addition to simple safety properties, users can check the effect of transactions and the causal dependency between events and transactions using the Property Specification Language (PSL). The approach is based on a translation of the original SystemC Model to C code. During the translation, a monitor is generated from the PSL property and embedded into the C model in form of source-code assertions. The verification is performed by a novel Bounded Model Checking (BMC) and k-induction technique at the level of C. This technique uses as the underlying proof engine a C model checker, leveraging the advances in the area of formal verification of sequential software.
In the second part of the talk an automated debugging approach for SystemC TLM designs is introduced. The approach automatically computes all diagnoses based on a given execution trace demonstrating an error. Each of these diagnoses describes one Possibly Faulty Part (PFP) in the design that can be changed based on an associated transformation such that the erroneous execution trace cannot be reproduced. A PFP is a set of TLM specific statements which are typically prone to design errors. For instance, erroneously a blocking transaction is used instead of a non-blocking transaction or the incorrect event is notified or waited for, etc. The computation of diagnoses is built on top of the TLM property checking method.