Date: Thursday 17 March 2016
Time: 16:00 - 17:30
Location / Room: Konferenz 5

Chair:
Mathias Soeken, École Polytechnique Fédérale de Lausanne (EPFL), CH

Co-Chair:
Gianpiero Cabodi, Politecnio di Torino, IT

The session considers verification at the system level. The first paper deals with the combination of protocols and networks. The second paper refines real-time analysis from task level to the level of runnable entities within tasks. The third one focuses on the correctness of synthesis from high level models.

Time	Label	Presentation Title Authors
16:00	12.7.1	ADVOCAT: AUTOMATED DEADLOCK VERIFICATION FOR ON-CHIP CACHE COHERENCE AND INTERCONNECTS Speaker: Freek Verbeek, Open University of The Netherlands, NL Authors: Freek Verbeek1, Pooria Yaghini2, Ashkan Eghbal2 and Nader Bagherzadeh2 1Open University of The Netherlands, NL; 2University of California, Irvine, US Abstract Cache coherence plays a major role in manycore systems. The verification of deadlocks is a challenge in particular, because deadlock freedom is an emergent property. Formal methods often decouple verification of the protocol from verification of the communication interconnect. Modern communication fabrics, however, become more advanced and include a network topology, routing, arbitration, synchronization, and more. In this paper, an integrated approach called ADVOCAT is proposed that allows cross-layer verification of both the cache coherence protocol and the communication fabric all at once. An automated methodology for deriving cross-layer invariants is proposed. These invariants relate the state of the application-layer protocols to en route packets in the communication fabric. We apply this methodology in a case study where cross-layer deadlocks occur if queues are wrongly sized. Our methodology is generally applicable and shows promising scalability. Download Paper (PDF; Only available from the DATE venue WiFi)
16:30	12.7.2	GUARANTEES FOR RUNNABLE ENTITIES WITH HETEROGENEOUS REAL-TIME REQUIREMENTS Speaker: Leonie Ahrendts, Technische Universität Braunschweig, DE Authors: Leonie Ahrendts, Zain A. H. Hammadeh and Rolf Ernst, Technische Universität Braunschweig, DE Abstract Classical real-time (RT) analysis proves temporal properties of tasks. In industrial practice, however, tasks are often composed of runnable entities with heterogeneous RT requirements. If RT guarantees are only available at task granularity, the strictest RT requirement of a runnable entity determines the RT requirement of the entire task. However, by giving RT guarantees for each runnable entity, this over-provisioning can be avoided. We provide an analysis which is fine-grained enough to provide hard and weakly-hard response time guarantees for runnable entities and show the improvement in an industrial case study. Download Paper (PDF; Only available from the DATE venue WiFi)
17:00	12.7.3	VALIDATING SCHEDULING TRANSFORMATION FOR BEHAVIORAL SYNTHESIS Speaker: Sandip Ray, Intel Corporation, US Authors: Zhenkun Yang1, Kecheng Hao2, Kai Cong3, Li Lei1, Sandip Ray3 and Fei Xie1 1Portland State University, US; 2Xilinx Inc., US; 3Intel Corporation, US Abstract Behavioral synthesis automatically compiles an electronic system-level description of a hardware design into an RTL implementation. Scheduling in behavioral synthesis is an important, sophisticated, and error-prone transformation which converts the untimed or partially timed description into a fully timed implementation. We present a scalable equivalence checking algorithm for validating scheduling transformations. The equivalence checking accounts for control/data dependency, scheduling modes, and subtle interface protocols. Our experimental results demonstrate that our approach scales to industrial benchmarks. Furthermore, our checker found bugs in industrial synthesis tool implementations. Download Paper (PDF; Only available from the DATE venue WiFi)
17:30		End of session