Date: Wednesday 27 March 2019
Time: 17:00 - 18:30
Location / Room: Room 2

Organisers:
Subhasish Mitra, Stanford, US
Georges Gielen, KU Leuven, BE

Chair:
Ulf Schlichtmann, TU Munich, DE

Co-Chair:
Giovanni De Micheli, EPFL, CH

Modern-day integrated circuits can contain several billions of transistors, multiple cores and memories, several analog and mixed-signal blocks, etc. While designing such chips is a huge effort, their verification is a true nightmare. Traditional techniques require extremely long computation times and may fail to capture all bugs in the system. These problems are exacerbated by even more difficult challenges: hardware security (e.g. the recent Spectre/Meltdown attacks stemming from hardware designs), system safety (e.g. for automotive applications), and software complexity (firmware and software form a significant component of complex Systems-on-Chip). This special session focuses on novel approaches from industry and academia to overcome these seemingly insurmountable outstanding challenges Most importantly, this session will discuss not only design bugs but also the new challenges (stated above) that design verification must address - major directions for the DATE research community.

Time	Label	Presentation Title Authors
17:00	8.2.1	HARDWARE AND FIRMWARE VERIFICATION AND VALIDATION: AN ALGORITHM-TO-FIRMWARE DEVELOPMENT METHODOLOGY Speaker: Henry Cox, MediaTek, US Authors: Henry Cox and Harry Chen, MediaTek, US Abstract System-level verification of a modem product involves ensuring both the hardware and firmware work correctly and that the product meets signal performance requirements at low cost. In many ways, the firmware problem is harder - or at least more open-ended. We discuss a development methodology based on automatic generation and reusable components that has been used to implement several generations of software-defined radio (SDR) modem SOCs. Automation both ensures consistency between models and tools and enables fast turnaround when something changes. Download Paper (PDF; Only available from the DATE venue WiFi)
17:30	8.2.2	PROCESSOR HARDWARE SECURITY VULNERABILITIES AND THEIR DETECTION BY UNIQUE PROGRAM EXECUTION CHECKING Speaker: Wolfgang Kunz, University of Kaiserslautern, DE Authors: Mohammad Rahmani Fadiheh1, Dominik Stoffel1, Clark Barrett2, Subhasish Mitra2 and Wolfgang Kunz1 1TU Kaiserslautern, DE; 2Stanford University, US Abstract Recent discovery of security attacks in advanced processors, known as Spectre and Meltdown, has resulted in high public alertness about security of hardware. The root cause of these attacks is information leakage across covert channels that reveal secret data without any explicit information flow between the secret and the attacker. Many sources believe that such covert channels are intrinsic to highly advanced processor architectures based on speculation and out-of-order execution, suggesting that such security risks can be avoided by staying away from high- end processors. This paper, however, shows that the problem is of wider scope: we present new classes of covert channel attacks which are possible in average-complexity processors with in-order pipelining, as they are mainstream in applications ranging from Internet-of-Things to Autonomous Systems. We present a new approach as a foundation for remedy against covert channels: while all previous attacks were found by clever thinking of human attackers, this paper presents a formal method called Unique Program Execution Checking which detects and locates vulnerabilities to covert channels systematically, including those to covert channels unknown so far. Download Paper (PDF; Only available from the DATE venue WiFi)
18:00	8.2.3	SYMBOLIC QED PRE-SILICON VERIFICATION FOR AUTOMOTIVE MICROCONTROLLER CORES: INDUSTRIAL CASE STUDY Speaker: Subhasish Mitra, Stanford University, US Authors: Eshan Singh1, Keerthikumara Devarajegowda2, Sebastian Simon3, Ralf Schnieder3, Karthik Ganesan1, Mohammad Fadiheh4, Dominik Stoffel4, Wolfgang Kunz4, Clark Barrett1, Wolfgang Ecker5 and Subhasish Mitra1 1Stanford University, US; 2Infineon Technologies AG/Technische Universität Kaiserslautern, DE; 3Infineon Technologies AG, DE; 4Technische Universität Kaiserslautern, DE; 5Infineon Technologies AG/Technische Universität München, DE Abstract We present an industrial case study that demonstrates the practicality and effectiveness of Symbolic Quick Error Detection (Symbolic QED) in detecting logic design flaws (logic bugs) during pre-silicon verification. Our study focuses on several microcontroller core designs (~1,800 flip-flops, ~70,000 logic gates) that have been extensively verified using an industrial verification flow and used for various commercial automotive products. The results of our study are as follows: 1. Symbolic QED detected all logic bugs in the designs that were detected by the industrial verification flow (which includes various flavors of simulation-based verification and formal verification). 2. Symbolic QED detected additional logic bugs that were not recorded as detected by the industrial verification flow. (These additional bugs were also perhaps detected by the industrial verification flow.) 3. Symbolic QED enables significant design productivity improvements: (a) 8X improved (i.e., reduced) verification effort for a new design (8 person-weeks for Symbolic QED vs. 17 person-months using the industrial verification flow). (b) 60X improved verification effort for subsequent designs (2 person-days for Symbolic QED vs. 4-7 person-months using the industrial verification flow). (c) Quick bug detection (runtime of 20 seconds or less), together with short counterexamples (10 or fewer instructions) for quick debug, using Symbolic QED. Download Paper (PDF; Only available from the DATE venue WiFi)
18:15	8.2.4	REVIEW OF METHODOLOGIES FOR PRE- AND POST-SILICON ANALOG VERIFICATION IN MIXED-SIGNAL SOCS Speaker: Georges Gielen, KU Leuven, BE Authors: Georges Gielen1, Nektar Xama1, Karthik Ganesan2 and Subhasish Mitra2 1KU Leuven, BE; 2Stanford University, US Abstract The integration of increasingly more complex and heterogeneous SOCs results in ever more complicated demands for the verification of the system and its underlying subsystems. Pre-silicon design validation as well as post-silicon test generation of the analog and mixed-signal (AMS) subsystems within SOCs proves extremely challenging as these subsystems do not share the formal description potential of their digital counterparts. Several methods have been developed to cope with this lack of formalization during AMS pre-silicon validation, including model checkers, affine arithmetic formalisms and equivalence checkers. However, contrary to the industrial practice for digital circuits of using formal verification and ATPG tools, common industry practice for analog circuits still largely defaults to simulation-based validation and test generation. A new formal digital-inspired technique, called AMS-QED, can potentially solve these issues in analog and mixed-signal verification. Download Paper (PDF; Only available from the DATE venue WiFi)
18:30		End of session