5.2 Improving Formal Verification and Applications to GPUs and High-Level Synthesis

Printer-friendly version PDF version

Date: Wednesday, March 27, 2019
Time: 08:30 - 10:00
Location / Room: Room 2

Chair:
Alessandro Cimatti, Fondazione Bruno Kessler, IT, Contact Alessandro Cimatti

Co-Chair:
Gianpiero Cabodi, Politecnico di Torino, IT, Contact Gianpiero Cabodi

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.

TimeLabelPresentation Title
Authors
08:305.2.1FBPDR: 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.
09:005.2.2HIGH COVERAGE CONCOLIC EQUIVALENCE CHECKING
Speaker:
Sagar Chaki, Mentor, US
Authors:
Pritam Roy, Sagar Chaki and Pankaj Chauhan, Mentor, 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.
09:305.2.3BOSPHORUS: 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 Gr"obner 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 emph{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.
09:455.2.4CUDA 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.
10:00IP2-9, 3USING 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.
10:01IP2-10, 498EMPIRICAL 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.
10:00End of session
Coffee Break in Exhibition Area



Coffee Breaks in the 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

  • Coffee Break 10:30 - 11:30
  • Lunch Break 13:00 - 14:30
  • Awards Presentation and Keynote Lecture in ""TBD"" 13:50 - 14:20
  • Coffee Break 16:00 - 17:00

Wednesday, March 27, 2019

  • Coffee Break 10:00 - 11:00
  • Lunch Break 12:30 - 14:30
  • Awards Presentation and Keynote Lecture in ""TBD"" 13:30 - 14:20
  • Coffee Break 16:00 - 17:00

Thursday, March 28, 2019

  • Coffee Break 10:00 - 11:00
  • Lunch Break 12:30 - 14:00
  • Keynote Lecture in ""TBD"" 13:20 - 13:50
  • Coffee Break 15:30 - 16:00