Date: Thursday 22 March 2018
Time: 16:00 - 17:30
Location / Room: Konf. 1
Chair:
Christoph Scholl, University of Freiburg, DE
Co-Chair:
Gianpiero Cabodi, Politecnico di Torino, IT
This session explores formal design methodology for asynchroneous pipelines, reasons about decomposing assume/guarantee contracts, links high-level models and RTL designs, and also improves arithmetic circuit verification.
| Time | Label | Presentation Title Authors |
|---|---|---|
| 16:00 | 12.3.1 | IMPROVING AND EXTENDING THE ALGEBRAIC APPROACH FOR VERIFYING GATE-LEVEL MULTIPLIERS Speaker: Armin Biere, Johannes Kepler Universität Linz, AT Authors: Daniela Ritirc, Armin Biere and Manuel Kauers, Johannes Kepler University Linz, AT Abstract The currently most effective approach for verifying gate-level multipliers uses Computer Algebra. It reduces a word-level multiplier specification by a Gröbner basis derived from a gate-level implementation. This reduction produces zero if and only if the circuit is a multiplier. We improve this approach by extracting full- and half-adder constraints to reduce the Gröbner basis, which speeds up computation substantially. Refactoring the specification in terms of partial products instead of inputs yields further improvements. As a third contribution we extend these algebraic techniques to verify the equivalence of bit-level multipliers without using a word-level specification. Download Paper (PDF; Only available from the DATE venue WiFi) |
| 16:30 | 12.3.2 | RECONFIGURABLE ASYNCHRONOUS PIPELINES: FROM FORMAL MODELS TO SILICON Speaker: Danil Sokolov, Newcastle University, GB Authors: Danil Sokolov, Alessandro de Gennaro and Andrey Mokhov, Newcastle University, GB Abstract Dataflow pipelines are widely used in the design of high-throughput computation systems. Real-life applications often require dynamically reconfigurable pipelines to differently process data items or adjust to the current operating mode. Reconfigurable synchronous pipelines are known since 1980s and are well supported by formal models and tools. Reconfigurable asynchronous pipelines on the other hand, have neither a formal behavioural model, nor mature EDA support, making them unattractive to industry. This paper presents a model and an open-source tool for the design and verification of reconfigurable asynchronous pipelines, and validates this approach in silicon. Download Paper (PDF; Only available from the DATE venue WiFi) |
| 17:00 | 12.3.3 | AUTOMATIC GENERATION OF HARDWARE CHECKERS FROM FORMAL MICRO-ARCHITECTURAL SPECIFICATIONS Speaker: Alexander Fedotov, Eindhoven University of Technology, NL Authors: Alexander Fedotov and Julien Schmaltz, Eindhoven University of Technology, NL Abstract To manage design complexity, high-level models are used to evaluate the functionality and performance of design solutions. There is a significant gap between these high-level models and the Register Transfer Level (RTL) implementations actually produced by designers. We address the challenge of bridging this gap, namely, relating abstract specifications to RTL implementations. An important feature of our proposed approach is to support emph{non-deterministic} specifications. From such a non-deterministic model, we automatically compute a representation of its observable behaviour. We then turn this representation into a System Verilog checker. The checker is connected to the input and output interfaces of the RTL implementation. The resulting combination is given to a commercial EDA tool to prove inclusion of the traces of the implementation into the traces of the specification. Our method is implemented for the formal micro-architectural description language (MaDL) — based on the xMAS formalism originally proposed by Intel — and exemplified on several examples. Download Paper (PDF; Only available from the DATE venue WiFi) |
| 17:15 | 12.3.4 | SPECIFICATION DECOMPOSITION FOR SYNTHESIS FROM LIBRARIES OF LTL ASSUME/GUARANTEE CONTRACTS Speaker: Antonio Iannopollo, UC Berkeley, IT Authors: Antonio Iannopollo, Stavros Tripakis and Alberto Sangiovanni Vincentelli, University of California, Berkeley, US Abstract Contract-Based Design is a methodology that allows for compositional design of complex systems. Given a contract representing a specification, it is possible to formally satisfy it by composing a number of simpler contracts. When these simpler contracts are chosen from a library of existing solutions, we talk about synthesis from contract libraries. There are techniques to automate the synthesis process, but they are computationally intensive, especially for complex specifications. In this paper, we describe an efficient technique to partition a specification, i.e., an LTL-based Assume/Guarantee contract, in a number of simpler sub-specifications which can be satisfied independently. Once all these smaller problems are solved, it is possible to safely merge their solutions to satisfy the original specification. We show the effectiveness of our technique in an industrial case study. Download Paper (PDF; Only available from the DATE venue WiFi) |
| 17:30 | End of session | |