Date: Thursday 12 March 2015
Time: 16:00 - 17:30
Location / Room: Belle Etoile
Chair:
Julien Schmaltz, Eindhoven University of Technology, NL
Co-Chair:
Gianpiero Cabodi, Politecnico di Torino, IT
The first three papers of this session present strong advances to the scalability of Boolean and arithmetic solvers.
| Time | Label | Presentation Title Authors |
|---|---|---|
| 16:00 | 12.2.1 | SOLVING DQBF THROUGH QUANTIFIER ELIMINATION Speakers: Karina Gitina, Ralf Wimmer, Sven Reimer, Matthias Sauer, Christoph Scholl and Bernd Becker, University of Freiburg, DE Abstract We show how to solve dependency quantified Boolean formulas (DQBF) using a quantifier elimination strategy which yields an equivalent QBF that can be decided using any standard QBF solver. The elimination is accompanied by a number of optimizations which help reduce memory consumption and computation time. We apply our solver HQS to problems from the domain of verification of incomplete combinational circuits to demonstrate the effectiveness of the proposed algorithm. The results show enormous improvements both in the number of solved instances and in the computation times compared to existing work on validating DQBF. Download Paper (PDF; Only available from the DATE venue WiFi) |
| 16:30 | 12.2.2 | FORMAL VERIFICATION OF SEQUENTIAL GALOIS FIELD ARITHMETIC CIRCUITS USING ALGEBRAIC GEOMETRY Speakers: Xiaojun Sun1, Priyank Kalla2, Tim Pruss1 and Florian Enescu3 1University of Utah, US; 2University of utah, US; 3Georgia State University, US Abstract Sequential Galois field (F_{2^k}) arithmetic circuits take k-bit inputs and produce a k-bit result, after k-clock cycles of operation. Formal verification of such sequential arithmetic circuits with large datapath size is beyond the capabilities of contemporary verification techniques. To address this problem, this paper describes a verification method based on algebraic geometry that: i) implicitly unrolls the sequential arithmetic circuit over multiple (k) clock-cycles; and ii) represents the function computed by the state-registers of the circuit, canonically, as a multi-variate word-level polynomial over F_{2^k}. Our approach employs the Groebner basis theory over a specific elimination ideal. Moreover, an efficient implementation is described to identify the k-cycle computation performed by the circuit at word-level. We can verify up to 100-bit sequential Galois field multipliers, whereas conventional techniques fail beyond 23-bit circuits. Download Paper (PDF; Only available from the DATE venue WiFi) |
| 17:00 | 12.2.3 | A UNIVERSAL MACRO BLOCK MAPPING SCHEME FOR ARITHMETIC CIRCUITS Speakers: Xing Wei, Yi Diao, Tak-Kei Lam and Yu-Liang Wu, The Chinese University of Hong Kong, HK Abstract A macro block is a functional unit that can be re-used in circuit designs. The problem of general macro block mapping is to identify such embedded parts, whose I/O signals are unknown, from the netlist that may have been optimized in various ways. The mapping results can then be used to ease the functional verification process or for replacement by more advanced intellectual property (IP) macros. In the past literatures, the mapping problem is mostly limited to the identification of a single adder or multiplier with I/O signals given, which is already NP-hard. However, in today's typical arithmetic circuits (like digital signal processing (DSP) applications), it is not unusual to have combinations of arithmetic operators implemented as macro blocks for performance gain. To solve this new practical mapping problem, we propose a flow to identify and build a forest of one-bit-adder trees using structural information and formal verification techniques, followed by algorithms that locate macro boundaries and I/O signal orders. Experimental results show that our algorithm is highly practical and scalable. It is capable of identifying any combinations of arbitrary adders and multipliers such as (a + b) × c and a × b + c × d + e × f , where each operand is a multi-bit constant or variable. Most of the benchmarks in ICCAD 2013 CAD Contest [1] can be well handled by our algorithm. Download Paper (PDF; Only available from the DATE venue WiFi) |
| 17:15 | 12.2.4 | TOWARDS AN ACCURATE RELIABILITY, AVAILABILITY AND MAINTAINABILITY ANALYSIS APPROACH FOR SATELLITE SYSTEMS BASED ON PROBABILISTIC MODEL CHECKING Speakers: Khaza Anuarul Hoque1, Otmane Ait Mohamed1 and Yvon Savaria2 1Concordia University, CA; 2Polytechnique Montreal, CA Abstract From navigation to telecommunication, and from weather forecasting to military, or entertainment services - satellites play a major role in our daily lives. Satellites in the Medium Earth Orbit (MEO) and geostationary orbit have a life span of 10 years or more. Reliability, Availability and Maintainability (RAM) analysis of a satellite system is a crucial part at their design phase to ensure the highest availability and optimized reliability. This paper shows the formal modeling and verification of RAM related properties of a satellite system. In a previously reported approach, time between possible failures and time between repairs are assumed to follow an exponential distribution, which does not represent a realistic scenario. In contrast, in our work, discrete time delays in the classical Continuous Time Markov Chain (CTMC) are approximated using the Erlang distribution. This is done by approximating nonexponential holding time with several intermediate states based on a phase type distribution. The RAM properties are then verified using the PRISM model checker.We present and compare modeling results with those obtained with a previously reported approach that demonstrate an improved modeling accuracy. Download Paper (PDF; Only available from the DATE venue WiFi) |
| 17:30 | End of session | |