2.5 Power of Assertions
Date: Tuesday 10 March 2015
Time: 11:30 - 13:00
Location / Room: Meije
Chair:
Franco Fummi, University of Verona, IT
Co-Chair:
Pablo Sanchez, University of Cantabria, ES
Assertions play a critical role in verification of hardware systems. This session is focusing on new applications of assertions in a wide variety of validation scenarios such as faster bug localization and post-silicon validation as well as reusing properties across abstraction levels.
| Time | Label | Presentation Title Authors |
|---|---|---|
| 11:30 | 2.5.1 | AUTOMATIC EXTRACTION OF ASSERTIONS FROM EXECUTION TRACES OF BEHAVIOURAL MODELS Speakers: Alessandro Danese, Tara Ghasempouri and Graziano Pravadelli, University of Verona, IT Abstract Several approaches exist for specification mining of hardware designs. Most of them work at RTL and they extract assertions in the form of temporal relations between Boolean variables. Other approaches work at system level (e.g., TLM) to mine assertions that specify the behaviour of the communication protocol. However, these techniques do not generate assertions addressing the design functionality. Thus, there is a lack of studies related to the automatic mining of assertions for capturing the functionality of behavioural models, where logic expressions among more abstracted (e.g., numeric) variables than bits and bit vectors are necessary. This paper is intended to fill in the gap, by proposing a tool for automatic extraction of temporal assertions from execution traces of behavioural models by adopting a mix of static and dynamic techniques. Download Paper (PDF; Only available from the DATE venue WiFi) |
| 12:00 | 2.5.2 | A METHODOLOGY FOR AUTOMATED DESIGN OF EMBEDDED BIT-FLIPS DETECTORS IN POST-SILICON VALIDATION Speakers: Pouya Taatizadeh and Nicola Nicolici, McMaster University, CA Abstract Post-silicon validation is concerned with detecting design errors that escape to silicon prototypes and need to be fixed before committing to high-volume manufacturing. Electrical errors are particularly difficult to catch during the pre-silicon phase because of the insufficient accuracy of device models, which is often traded-off against simulation time. This challenge is further aggravated by the rising number of voltage domains, especially if subtle errors are excited in unique electrical states. Since these electrically-induced subtle errors most commonly manifest in the logic domain as bit-flips, to the best of our knowledge there are no systematic methods to design embedded hardware monitors for generic logic blocks that can detect bit-flips with low detection latency. Toward this goal, we propose a methodology that relies on design assertions that are ranked based on their potential to detect bit-flips and subsequently mapped into user-constrained embedded hardware monitors with the aim to increase bit-flip coverage estimate. Download Paper (PDF; Only available from the DATE venue WiFi) |
| 12:30 | 2.5.3 | DATA MINING DIAGNOSTICS AND BUG MRIS FOR HW BUG LOCALIZATION Speakers: Monica Farkash1, Bryan Hickerson2 and Balavinayagam Samynathan1 1University of Texas at Austin, US; 2IBM, US Abstract This paper addresses the challenge of minimizing the time and resources required to localize bugs in HW dynamic functional verification. Our diagnostics solution eliminates the need to back trace from point of failure to its origin, decreasing the overall debugging time. The proposed solution dynamically analyses data extracted from sets of passing and failing tests to identify behavior discrepancies, which it expresses as source code statements, coverage events and timing during simulation. It also provides a visual diagnostic support, an image of the behavior discrepancies in time which we call a Machine Reasoning Image (MRI). This paper describes in detail our data mining solution based on coverage data, HDL hierarchies and time analysis of coverage events. Our approach brings a data mining solution to the problem of HW bug localization. It defines new concepts, provides in-depth analysis, presents supporting algorithms, and shows actual results on archetypical problems from PowerPC core verification as an industrial application. Download Paper (PDF; Only available from the DATE venue WiFi) |
| 12:45 | 2.5.4 | RTL PROPERTY ABSTRACTION FOR TLM ASSERTION-BASED VERIFICATION Speakers: Nicola Bombieri1, Riccardo Filippozzi1, Graziano Pravadelli1 and Francesco Stefanni2 1University of Verona, IT; 2EDALab s.r.l., IT Abstract Different techniques and commercial tools are at the state of the art to reuse existing RTL IP models to generate more abstract (i.e., TLM) IP implementations for system-level design. In contrast, reusing, at TLM, an assertion-based verification (ABV) environment originally developed for an RTL IP is still an open problem. The lack of an effective and efficient solution forces verification engineers to shoulder a time consuming and error-prone manual re-definition, at TLM, of existing assertion libraries. This paper is intended to fill in the gap by presenting a technique to automatically abstract properties defined for RTL IPs and to create dynamic ABV environments for the corresponding TLM models. Download Paper (PDF; Only available from the DATE venue WiFi) |
| 13:00 | IP1-7, 970 | MINIMIZING THE NUMBER OF PROCESS CORNER SIMULATIONS DURING DESIGN VERIFICATION Speakers: Michael Shoniker, Bruce Cockburn, Jie Han and Witold Pedrycz, University of Alberta, CA Abstract Integrated circuit designs need to be verified in simulation over a large number of process corners that represent the expected range of transistor properties, supply voltages, and die temperatures. Each process corner can require substantial simulation time. Unfortunately, the required number of corners has been growing rapidly in the latest semiconductor technologies. We consider the problem of minimizing the required number of process corner simulations by iteratively learning a model of the output functions in order to confidently estimate key maximum and/or minimum properties of those functions. Depending on the output function, the required number of corner simulations can be reduced by factors of up to 95%. Download Paper (PDF; Only available from the DATE venue WiFi) |
| 13:00 | End of session Lunch Break, Keynote session from 1320 - 1420 (Room Oisans) sponsored by Mentor Graphics in front of the session room Salle Oisans and in the Exhibition area Coffee Break in Exhibition AreaOn all conference days (Tuesday to Thursday), coffee and tea will be served during the coffee breaks at the below-mentioned times in the exhibition area. Lunch BreakOn Tuesday and Wednesday, lunch boxes will be served in front of the session room Salle Oisans and in the exhibition area for fully registered delegates (a voucher will be given upon registration on-site). On Thursday, lunch will be served in Room Les Ecrins (for fully registered conference delegates only). Tuesday, March 10, 2015Coffee Break 10:30 - 11:30 Lunch Break 13:00 - 14:30; Keynote session from 13:20 - 14:20 (Room Oisans) sponsored by Mentor Graphics Coffee Break 16:00 - 17:00 Wednesday, March 11, 2015Coffee Break 10:00 - 11:00 Lunch Break 12:30 - 14:30, Keynote lectures from 12:50 - 14:20 (Room Oisans) Coffee Break 16:00 - 17:00 Thursday, March 12, 2015Coffee Break 10:00 - 11:00 Lunch Break 12:30 - 14:00, Keynote lecture from 13:20 - 13:50 Coffee Break 15:30 - 16:00 |
Visit us at DATE 2015
