Date: Wednesday 11 March 2020
Time: 08:30 - 10:00
Location / Room: Stendhal
Chair:
Alessandro Cimatti, Fondazione Bruno Kessler, IT
Co-Chair:
Heinz Riener, EPFL, CH
The session presents several new techniques in hardware verification. The technical papers propose methods for the formal verification of industrial arithmetic circuits and processors, and show how reinforcement learning can be used for verification of shared memory protocols. Two interactive presentations describe how to use high-level synthesis to supply security guarantees and to generate certificates when verifying multipliers.
| Time | Label | Presentation Title Authors |
|---|---|---|
| 08:30 | 5.4.1 | GAP-FREE PROCESSOR VERIFICATION BY S²QED AND PROPERTY GENERATION Speaker: Keerthikumara Devarajegowda, Infineon Technologies, DE Authors: Keerthikumara Devarajegowda1, Mohammad Rahmani Fadiheh2, Eshan Singh3, Clark Barrett3, Subhasish Mitra3, Wolfgang Ecker1, Dominik Stoffel2 and Wolfgang Kunz2 1Infineon Technologies, DE; 2TU Kaiserslautern, DE; 3Stanford University, US Abstract The required manual effort and verification expertise are among the main hurdles for adopting formal verification in processor design flows. Developing a set of properties that fully covers all instruction behaviors is a laborious and challenging task. This paper proposes a highly automated and "complete" processor verification approach which requires considerably less manual effort and expertise compared to the state of the art. The proposed approach extends the S²QED approach to cover both single and multiple instruction bugs and ensures that a design is completely verified according to a well-defined criterion. This makes the approach robust against human errors. The properties are simple and can be automatically generated from an ISA model with small manual effort. Furthermore, unlike in conventional property checking, the verification engineer does not need to explicitly specify the processor's behavior in different special scenarios, such as stalling, exception, or speculation, since these are taken care of implicitly by the proposed computational model. The great promise of the approach is shown by an industrial case study with a 5-stage RISC-V processor. Download Paper (PDF; Only available from the DATE venue WiFi) |
| 09:00 | 5.4.2 | SPEAR: HARDWARE-BASED IMPLICIT REWRITING FOR SQUARE-ROOT VERIFICATION Speaker: Maciej Ciesielski, University of Massachusetts Amherst, US Authors: Atif Yasin1, Tiankai Su1, Sebastien Pillement2 and Maciej Ciesielski1 1University of Massachusetts Amherst, US; 2University of Nantes France, FR Abstract The paper addresses the formal verification of gate-level square-root circuits. Division and square root functions are some of the most complex arithmetic operations to implement and proving the correctness of their hardware implementation is of great importance. In contrast to standard approaches that use satisfiability and equivalence checking techniques, the presented method verifies whether the gate-level square-root circuit actually performs a root operation, instead of checking equivalence with a reference design. The method extends the algebraic rewriting technique developed earlier for multipliers and introduces a novel technique of implicit hardware rewriting. The tool called SPEAR based on hardware rewriting enables the verification of a 256-bit gate-level square-root circuit with 0.26 million gates in under 18 minutes. Download Paper (PDF; Only available from the DATE venue WiFi) |
| 09:30 | 5.4.3 | A REINFORCEMENT LEARNING APPROACH TO DIRECTED TEST GENERATION FOR SHARED MEMORY VERIFICATION Speaker: Nícolas Pfeifer, Federal University of Santa Catarina, BR Authors: Nicolas Pfeifer, Bruno V. Zimpel, Gabriel A. G. Andrade and Luiz C. V. dos Santos, Federal University of Santa Catarina, BR Abstract Multicore chips are expected to rely on coherent shared memory. Albeit the coherence hardware can scale gracefully, the protocol state space grows exponentially with core count. That is why design verification requires directed test generation (DTG) for dynamic coverage control under the tight time constraints resulting from slow simulation and short verification budgets. Next generation EDA tools are expected to exploit Machine Learning for reaching high coverage in less time. We propose a technique that addresses DTG as a decision process and tries to find a decision-making policy for maximizing the cumulative coverage, as a result of successive actions taken by an agent. Instead of simply relying on learning, our technique builds upon the legacy from constrained random test generation (RTG). It casts DTG as coverage-driven RTG, and it explores distinct RTG engines subject to progressively tighter constraints. We compared three Reinforcement Learning generators with a state-of-the-art generator based on Genetic Programming. The experimental results show that the proper enforcement of constraints is more efficient for guiding learning towards higher coverage than simply letting the generator learn how to select the most promising memory events for increasing coverage. For a 3-level MESI 32-core design, the proposed approach led to the highest observed coverage (95.81%), and it was 2.4 times faster than the baseline generator to reach the latter's maximal coverage. Download Paper (PDF; Only available from the DATE venue WiFi) |
| 09:45 | 5.4.4 | TOWARDS FORMAL VERIFICATION OF OPTIMIZED AND INDUSTRIAL MULTIPLIERS Speaker: Alireza Mahzoon, University of Bremen, DE Authors: Alireza Mahzoon1, Daniel Grosse2, Christoph Scholl3 and Rolf Drechsler2 1University of Bremen, DE; 2University of Bremen / DFKI, DE; 3University of Freiburg, DE Abstract Formal verification methods have made huge progress over the last decades. However, proving the correctness of arithmetic circuits involving integer multipliers still drives the verification techniques to their limits. Recently, Symbolic Computer Algebra (SCA) methods have shown good results in the verification of both large and non-trivial multipliers. Their success is mainly based on (1) reverse engineering and identifying basic building blocks, (2) finding converging gate cones which start from the basic building blocks and (3) early removal of redundant terms (vanishing monomials) to avoid the blow-up during backward rewriting. Despite these important accomplishments, verifying optimized and technology-mapped multipliers is an almost unexplored area. This creates major barriers for industrial use as most of the designs are area and delay optimized. To overcome the barriers, we propose a novel SCA-method which supports the formal verification of a large variety of optimized multipliers. Our method takes advantage of a dynamic substitution ordering to avoid the monomial explosion during backward rewriting. Experimental results confirm the efficiency of our approach in the verification of a wide range of optimized multipliers including industrial benchmarks. Download Paper (PDF; Only available from the DATE venue WiFi) |
| 10:00 | IP2-12, 151 | FROM DRUP TO PAC AND BACK Speaker: Daniela Kaufmann, Johannes Kepler University Linz, AT Authors: Daniela Kaufmann, Armin Biere and Manuel Kauers, Johannes Kepler University Linz, AT Abstract Currently the most efficient automatic approach to verify gate-level multipliers combines SAT solving and computer algebra. In order to increase confidence in the verification, proof certificates are generated. However, due to different solving techniques, these certificates require two different proof formats, namely DRUP and PAC. A combined proof has so far been missing. Correctness of this approach can thus only be trusted up to the correctness of compositional reasoning. In this paper we show how to generate a single proof in one proof format, which then allows to certify correctness using one simple proof checker. We further investigate empirically the effect on proof generation and checking time as well as on proof size. It turns out that PAC proofs are much more compact and faster to check. Download Paper (PDF; Only available from the DATE venue WiFi) |
| 10:01 | IP2-13, 956 | VERIFIABLE SECURITY TEMPLATES FOR HARDWARE Speaker: Bill Harrison, Oak Ridge National Laboratory, US Authors: William Harrison1 and Gerard Allwein2 1Oak Ridge National Laboratory, US; 2Naval Research Laboratory, US Abstract But HLS has, with a few notable exceptions, not focused on transferring ideas and techniques from high assurance software formal methods to hardware development, despite there being a sophisticated and mature body of research in that area. Just as it has introduced software engineering virtues, we believe HLS can also become a vector for retrofitting software formal methods to the challenge of high assurance security in hardware. This paper introduces the Device Calculus and its mechanization in the Agda proof checking system. The Device Calculus is a starting point for exploring formal methods and security within high-level synthesis flows. We illustrate the Device Calculus with a number of examples of formally verifiable security templates---i.e., functions in the Device Calculus that express common security structures at a high-level of abstraction. Download Paper (PDF; Only available from the DATE venue WiFi) |
| 10:00 | End of session | |