5.2 Improving Formal Verification and Applications to GPUs and High-Level Synthesis
Date: Wednesday 27 March 2019
Time: 08:30 - 10:00
Location / Room: Room 2
Chair:
Alessandro Cimatti, Fondazione Bruno Kessler, IT
Co-Chair:
Gianpiero Cabodi, Politecnico di Torino, IT
The session includes three technical and three application papers. The technical papers aim at improving and evaluating advanced model checking engines, and combining algebraic reasoning and SAT. The application papers show how formal verification is used for the correctness of GPU assembly programs, equivalence checking for high-level synthesis, and assessing failure rates of CMOS.
| Time | Label | Presentation Title Authors |
|---|---|---|
| 08:30 | 5.2.1 | (Best Paper Award Candidate) FBPDR: IN-DEPTH COMBINATION OF FORWARD AND BACKWARD ANALYSIS IN PROPERTY DIRECTED REACHABILITY Speaker: Tobias Seufert, University of Freiburg, DE Authors: Tobias Seufert and Christoph Scholl, University Freiburg, DE Abstract We describe a thoroughly interweaved forward and backward version of PDR/IC3 called fbPDR. Motivated by the complementary strengths of PDR and Reverse PDR and by related work showing the benefits of collaboration between the two, fbPDR lifts the combination to a new level. We lay the theoretical groundwork for sharing learned lemmas between PDR and Reverse PDR and demonstrate the effectiveness of our approach on benchmarks from the Hardware Model Checking Competition. Download Paper (PDF; Only available from the DATE venue WiFi) |
| 09:00 | 5.2.2 | HIGH COVERAGE CONCOLIC EQUIVALENCE CHECKING Speaker: Sagar Chaki, Mentor Graphics, US Authors: Pritam Roy, Sagar Chaki and Pankaj Chauhan, Mentor Graphics, US Abstract A concolic approach, called SLEC-CF, to check sequential equivalence between a high-level (e.g., C++/SystemC) hardware description and an RTL (e.g., Verilog) is presented. SLEC-CF searches for counterexamples over the possible values of a set of "control signals" in a depth-first lexicographic manner, avoiding values that are unrealizable by any concrete input. In addition, SLEC-CF respects user-specified design constraints during search, thus only producing stimuli that are of relevance to users. It is a superior alternative to random simulations, which produce an overwhelming number of irrelevant stimuli for user-constrained designs, and are therefore of limited effectiveness. To handle complex designs, we present an incremental version of SLEC-CF, which iteratively increases the search depth, and set of control signals, and uses a cache to reuse prior results. We implemented SLEC-CF on top an existing industrial tool for sequential equivalence checking. Experimental results indicate that SLEC-CF clearly outperforms random simulation in terms of coverage achieved. On complex designs, incremental SLEC-CF demonstrates superior ability to achieve good coverage in almost all cases, compared to non-incremental SLEC-CF. Download Paper (PDF; Only available from the DATE venue WiFi) |
| 09:30 | 5.2.3 | BOSPHORUS: BRIDGING ANF AND CNF SOLVERS Speaker: Mate Soos, National University of Singapore, SG Authors: Davin Choo1, Mate Soos2, Kian Ming A. Chai1 and Kuldeep S Meel2 1DSO National Laboratories, SG; 2National University of Singapore, SG Abstract Algebraic Normal Form (ANF) and Conjunctive Normal Form (CNF) are commonly used to encode problems in Boolean algebra. ANFs are typically solved via Grobner basis algorithms, often using more memory than is feasible; while CNFs are solved using SAT solvers, which cannot exploit the algebra of polynomials naturally. We propose a paradigm that bridges between ANF and CNF solving techniques: the techniques are applied in an iterative manner to learn facts to augment the original problems. Experiments on over 1,100 benchmarks arising from four different applications domains demonstrate that learnt facts can significantly improve runtime and enable more benchmarks to be solved. Download Paper (PDF; Only available from the DATE venue WiFi) |
| 09:45 | 5.2.4 | CUDA AU COQ: A FRAMEWORK FOR MACHINE-VALIDATING GPU ASSEMBLY PROGRAMS Speaker: Benjamin Ferrell, Univeristy Texas at Dallas, US Authors: Benjamin Ferrell, Jun Duan and Kevin Hamlen, University of Texas at Dallas, US Abstract A prototype framework for formal, machine-checked validation of GPU pseudo-assembly code algorithms using the Coq proof assistant is presented and discussed. The framework is the first to afford GPU programmers a reliable means of formally machine-validating high-assurance GPU computations without trusting any specific source-to-assembly compilation toolchain. A formal operational semantics for the PTX pseudo-assembly language is expressed as inductive, dependent Coq types, facilitating development of proofs and proof tactics that refer directly to the compiled PTX object code. Challenges modeling PTX's complex and highly parallelized computation model in Coq, with sufficient clarity and generality to tractably prove useful properties of realistic GPU programs, are discussed. Examples demonstrate how the prototype can already be used to validate some basic yet realistic programs. Download Paper (PDF; Only available from the DATE venue WiFi) |
| 10:00 | IP2-9, 3 | USING STATISTICAL MODEL CHECKING TO ASSESS RELIABILITY FOR BATHTUB-SHAPED FAILURE RATES Speaker and Author: Josef Strnadel, Brno University of Technology, CZ Abstract Ideally, the reliability can be assessed analytically, provided that an analytical solution exists and its presumptions are met. Otherwise, alternative approaches to the assessment must apply. This paper proposes a novel, simulation based approach that relies on stochastic timed automata. Based on the automata, our paper explains principles of creating reliability models for various scenarios. Our approach expects that a reliability model is then processed by a statistical model checking method, used to assess the reliability by statistical processing of simulation results over the model. Main goal of this paper is to show that instruments of stochastic timed automata and statistical model checking are capable of facilitating the assessment process even for adverse conditions such as bathtub shaped failure rates. Download Paper (PDF; Only available from the DATE venue WiFi) |
| 10:01 | IP2-10, 498 | EMPIRICAL EVALUATION OF IC3-BASED MODEL CHECKING TECHNIQUES ON VERILOG RTL DESIGNS Speaker: Aman Goel, University of Michigan, US Authors: Aman Goel and Karem Sakallah, University of Michigan, US Abstract IC3-based algorithms have emerged as effective scalable approaches for hardware model checking. In this paper we evaluate six implementations of IC3-based model checkers on a diverse set of publicly-available and proprietary industrial Verilog RTL designs. Four of the six verifiers we examined operate at the bit level and two employ abstraction to take advantage of word-level RTL semantics. Overall, the word-level verifier employing data abstraction outperformed the others, especially on the large industrial designs. The analysis helped us identify several key insights on the techniques underlying these tools, their strengths and weaknesses, differences and commonalities, and opportunities for improvement. Download Paper (PDF; Only available from the DATE venue WiFi) |
| 10:00 | End of session Coffee Break in Exhibition Area
On 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 Breaks (Lunch Area)On all conference days (Tuesday to Thursday), a seated lunch (lunch buffet) will be offered in the Lunch Area to fully registered conference delegates only. There will be badge control at the entrance to the lunch break area. Tuesday, March 26, 2019
Wednesday, March 27, 2019
Thursday, March 28, 2019
|
DATE Newsletter
Stay informed on our latest news!
DATE Smartphone App
available at
In the Whova App search for "DATE 2019" in the event list and use the Password: "DATE".
Visit us at DATE 2019
