Date: Thursday 17 March 2016
Time: 08:30 - 10:00
Location / Room: Konferenz 3
Chair:
Markus Wedler, Synopsys GmbH, DE
Co-Chair:
Julien Schmaltz, Eindhoven University of Technology, NL
The session presents advancements in formal reasoning at the bit-level. The first paper makes significant improvements to the verification of multipliers. The second and third papers show progress in the analysis of memory-locked errors and clock domain crossing. The session closes with two IP presentations about using software analyzers for hardware verification and generating word-level models from bit-level designs.
| Time | Label | Presentation Title Authors |
|---|---|---|
| 08:30 | 9.5.1 | (Best Paper Award Candidate) FORMAL VERIFICATION OF INTEGER MULTIPLIERS BY COMBINING GRöBNER BASIS WITH LOGIC REDUCTION Speaker: Amr Sayed-Ahmed, University of Bremen, DE Authors: Amr Sayed Ahmed1, Daniel Grosse1, Ulrich Kühne1, Mathias Soeken1 and Rolf Drechsler2 1University of Bremen, DE; 2University of Bremen and DFKI, DE Abstract Formal verification utilizing symbolic computer algebra has demonstrated the ability to formally verify large Galois field arithmetic circuits and basic architectures of integer arithmetic circuits. The technique models the circuit as Gröbner basis polynomials and reduces the polynomial equation of the circuit specification wrt. the polynomials model. However, during the Gröbner basis reduction, the technique suffers from exponential blow-up in the size of the polynomials, if it is applied on parallel adders and recoded multipliers. In this paper, we address the reasons of this blow-up and present an approach that allows to apply the technique on basic and complex parallel architectures of multipliers. The approach is based on applying a logic reduction rule during Gröbner basis rewriting. The rule uses structural circuit information to remove terms that evaluate to zero before their blow-up. The experiments show that the approach is applicable up to 128 bit multipliers. Download Paper (PDF; Only available from the DATE venue WiFi) |
| 09:00 | 9.5.2 | ROOT-CAUSE ANALYSIS FOR MEMORY-LOCKED ERRORS Speaker: John Adler, University of Toronto, CA Authors: John Adler, Djordje Maksimovic and Andreas Veneris, University of Toronto, CA Abstract Half of the time in the design cycle today is spent on verifying and debugging the correctness of a design. Although some debugging tasks have been automated, determining the root-cause of errors that have been locked in memory for a number of clock cycles before they propagate to an observation point remains a time consuming effort. This is because the error traces exposing such behavior can be excessively long, a fact that requires modeling the circuit for many time-frames. This paper introduces a performance-driven debugging methodology for pinpointing the root-cause of memory-locked errors. The technique models only a sliding time window and a final time window explicitly at any one time, while interstitial time-frames are linked with a lightweight memory model. This technique is later extended to a complete methodology that diagnoses errors that may be missed. Experiments on industrial designs with memory-locked errors demonstrate a 72% reduction in peak memory usage with a comparable runtime to existing methodologies. Download Paper (PDF; Only available from the DATE venue WiFi) |
| 09:30 | 9.5.3 | FORMAL VERIFICATION OF CLOCK DOMAIN CROSSING USING GATE-LEVEL MODELS OF METASTABLE FLIP-FLOPS Speaker: Ghaith Tarawneh, Newcastle University, GB Authors: Ghaith Tarawneh, Andrey Mokhov and Alex Yakovlev, Newcastle University, GB Abstract Verifying clock domain boundary logic is a major challenge to the design of modern multi-clock systems. We present a novel verification approach that addresses the issue of domain crossing failures at a fundamental level. The approach relies on substituting flip-flops with model circuits and applying topological transformations to simulate the transfer of timing violations in gate-level netlists. This makes timing violations and their effects reproducible in discrete cycle-based simulation and amenable for identification and debugging similar to typical synchronous design failures. We show that this approach, when combined with formal verification, is inherently capable of reproducing many of the problematic issues at clock domain boundaries and outperforms the structural and functional heuristics used by state of the art commercial tools in several respects. It reports fewer false positives, can be applied to non-stereotypical designs, can determine failure consequences, can demonstrate failures in signal waveforms and requires no input from the designer about what design patterns are used. Case examples and verification results of several multi-clock testbench designs are presented. Download Paper (PDF; Only available from the DATE venue WiFi) |
| 10:00 | IP4-11, 274 | UNBOUNDED SAFETY VERIFICATION FOR HARDWARE USING SOFTWARE ANALYZERS Speaker: Rajdeep Mukherjee, University of Oxford, GB Authors: Rajdeep Mukherjee, Peter Schrammel, Daniel Kroening and Tom Melham, University of Oxford, GB Abstract Demand for scalable hardware verification is ever increasing. We propose an unbounded safety verification framework for hardware, at the heart of which is a software verifier. To this end, we synthesize Verilog at register transfer level into a software-netlist, represented as a word-level ANSI-C program. The proposed tool flow allows us to leverage the precision and scalability of state-of-the-art software verification techniques. In particular, we evaluate unbounded proof techniques, such as predicate abstraction, k-induction, interpolation, and IC3/PDR; and we compare the performance of verification tools from the hardware and software domains that use these techniques. To the best of our knowledge, this is the first attempt to perform unbounded verification of hardware using software analyzers. Download Paper (PDF; Only available from the DATE venue WiFi) |
| 10:01 | IP4-12, 765 | VERILOG2SMV: A TOOL FOR WORD-LEVEL VERIFICATION Speaker: Ahmed Irfan, Fondazione Bruno Kessler and University of Trento, IT Authors: Ahmed Irfan1, Alessandro Cimatti2, Alberto Griggio2, Marco Roveri2 and Roberto Sebastiani3 1Fondazione Bruno Kessler and University of Trento, IT; 2Fondazione Bruno Kessler, IT; 3University of Trento, IT Abstract Verification is an essential step of the hardware design lifecycle. Usually verification is done at the gate level (Boolean level). We present verilog2smv, a tool that generates word-level model checking problems from Verilog designs augmented with assertions. A key aspect of our tool is that memories in the designs are treated without any form of abstraction. verilog2smv can be used for RTL verification by chaining with a word-level model checker like nuXmv. To this extent, we present also some experimental results over Verilog verification benchmarks, using verilog2smv + nuXmv as a tool-chain. Download Paper (PDF; Only available from the DATE venue WiFi) |
| 10:02 | IP4-13, 717 | TOWARDS FORMAL VERIFICATION OF REAL-WORLD SYSTEMC TLM PERIPHERAL MODELS - A CASE STUDY Speaker: Vladimir Herdt, University of Bremen, DE Authors: Hoang M. Le1, Vladimir Herdt1, Daniel Grosse1 and Rolf Drechsler2 1University of Bremen, DE; 2University of Bremen and DFKI, DE Abstract SystemC-based Virtual Prototypes (VPs) serve as reference models for various activities in the modern design flow and therefore, the functional correctness of each individual components and the VPs as a whole should be subjected to rigorous formal verification. In the last few years, notable progress on SystemC formal verification has been made. This paper presents a case study on applying a recent approach to formally verify TLM peripheral models. To the best of our knowledge, this is the first formal verification case study targeting this important class of VP components. First, we show how to bridge the gap between the industry-accepted modeling pattern for TLM peripheral models and the semantics currently supported by SystemC formal verification approaches. Then, we report verification results for the interrupt controller of the LEON3-based SoCRocket VP used by the European Space Agency and reflect on our experiences and lessons learned in the process. Download Paper (PDF; Only available from the DATE venue WiFi) |
| 10:00 | End of session Coffee Break in Exhibition Area |