Date: Wednesday 26 March 2014
Time: 11:00 - 12:30
Location / Room: Konferenz 3

Chair:
Christoph Scholl, University of Freiburg, DE

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

Formal methods are traditionally used to verify the correctness or hardware, software, or protocols. This session introduces a set of applications which extend the use of formal methods into new domains. The first three papers demonstrate novel ways to bridge formal verification results into the synthesis domain. The fourth leverages formal reasoning to certify the correctness of photonic systems.

Time	Label	Presentation Title Authors
11:00	6.5.1	(Best Paper Award Candidate) USING MAXBMC FOR PARETO-OPTIMAL CIRCUIT INITIALIZATION Speakers: Sven Reimer, Matthias Sauer, Tobias Schubert and Bernd Becker, University of Freiburg, DE Abstract Abstract—In this paper we present MaxBMC, a novel formalism for solving optimization problems in sequential systems. Our approach combines techniques from symbolic SAT-based Bounded Model Checking (BMC) and incremental MaxSAT, leading to the first MaxBMC solver. In traditional BMC safety and liveness properties are validated. We extend this formalism: in case the required property is satisfied, an optimization problem is defined to maximize the quality of the reached witnesses. Further, we compare its qualities in different depths of the system, leading to Pareto-optimal solutions. We state a sound and complete algorithm that not only tackles the optimization problem but moreover verifies whether a global optimum has been identified by using a complete BMC solver as back-end. As a first reference application we present the problem of circuit initialization. Additionally, we give pointers to other tasks which can be covered by our formalism quite naturally and further demonstrate the efficiency and effectiveness of our approach.
11:30	6.5.2	PARTIAL WITNESSES FROM PREPROCESSED QUANTIFIED BOOLEAN FORMULAS Speakers: Martina Seidl1 and Robert Könighofer2 1JKU Linz, AT; 2TU Graz, AT Abstract For effectively solving quantified Boolean formulas (QBF) in prenex conjunctive normal form, preprocessors have shown to be indispensable. A preprocessor rewrites a formula in such a manner that information valuable for the solver is made explicit and irrelevant information is removed. For this purpose, rewriting techniques, which would be too costly when repeatedly applied during the solving process, are used. Unfortunately, many of these techniques are not model preserving and therefore incompatible with recent certification frameworks. In consequence, the application of a preprocessor prohibits the xtraction of witnesses encoding a solution or a counterexample. In this paper, we show how to obtain an assignment for the variables of the outermost quantifier block as partial witness which is sufficient for many practical applications. We modified the publicly available preprocessor bloqqer for extracting partial witnesses. We empirically compare the effectiveness of the modified and the original version of bloqqer. Further, we apply the new version of bloqqer for solving hardware synthesis problems for which it turns out to be extremely beneficial.
12:00	6.5.3	EQUIVALENCE CHECKING FOR FUNCTION PIPELINING IN BEHAVIORAL SYNTHESIS Speakers: Kecheng Hao1, Sandip Ray2 and Fei Xie3 1Xilinx Inc., US; 2Strategic CAD Labs, Intel Corporation, US; 3Portland State University, US Abstract Function pipelining is a key transformation in high-level synthesis. However, synthesizing the complex pipeline logic is an error-prone process. Sequential equivalence checking (SEC) support is highly desired to provide confidence in the correctness of synthesized pipelines. However, SEC for function pipelining is challenging due to the significant difference between the behavioral specification and the synthesized RTL. Furthermore, function pipelines include hardware logic for dynamically inserting "bubbles" (pipeline stalls), which bring additional difficulties in equivalence checking. We develop an SEC framework for behaviorally synthesized function pipelines by (1) building a reference pipeline model with a certified function pipelining transformation, which faithfully captures bubble insertion; and (2) checking the equivalence between the reference model and synthesized RTL implementation. We demonstrate the scalability of our approach on industry-strength designs synthesized by a commercial tool.
12:15	6.5.4	TOWARDS THE FORMAL ANALYSIS OF MICRORESONATORS BASED PHOTONIC SYSTEMS Speakers: Umair Siddique1 and Sofiene Tahar2 1Concordia University, Montreal, Canada, CA; 2Department of Electrical and Computer Engineering, Concordia University, CA Abstract Recent developments in the fabrication technology attracted the attention of optical engineers and physicists in the area of VLSI photonics. Due to the physical nature of light-wave systems and their usage in safety critical domains such as human surgeries and high budget space missions, it is indispensable to build high assurance systems. Traditionally, the analysis of such systems has been carried out by paper-and-pencil based proofs and numerical computations. However, these techniques cannot provide perfectly accurate results due to the risk of human error and inherent approximations of numerical algorithms. In order to overcome these limitations, we propose to use higher-order logic theorem proving to improve the analysis in the domain of integrated optics or VLSI photonics. In particular, this paper provides a higher-order logic formalization of optical microresonators which are the most fundamental building blocks of many photonic devices. In order to illustrate the practical utilization of our work, we present the formal analysis of 2-D microresonator lattice optical filters.
12:30	IP3-4, 108	SKETCHILOG: SKETCHING COMBINATIONAL CIRCUITS Speakers: Andrew Becker, David Novo and Paolo Ienne, École Polytechnique Fédérale de Lausanne, CH Abstract Despite the progress of higher-level languages and tools, Register Transfer Level (RTL) is still by far the dominant input format for high performance digital designs. Experienced designers can directly express their microarchitectural intuitions in RTL. Yet, RTL is terribly verbose, burdened with trivial details, and thus error prone. In this paper, we augment a modern RTL language (Chisel) with new semantic elements to express an imprecise specification: a sketch. We show how, in combination with a naive, unoptimized, but functionally correct reference, a designer can utilize the language and supporting infrastructure to focus on the key design intuition and omit some of the necessary details. The resulting design is exactly or almost exactly as good as the one the designer could have achieved by spending the time to manually complete the sketch. We show that, even limiting ourselves to combinational circuits, realistic instances of meaningful design problems are solved quickly, saving considerable design and debugging effort.
12:31	IP3-5, 557	TOWARDS VERIFYING DETERMINISM OF SYSTEMC DESIGNS Speakers: Hoang M. Le and Rolf Drechsler, University of Bremen, DE Abstract Ensuring the correctness of high-level SystemC designs is an important and challenging problem in today's Electronic System Level (ESL) methodology. Prevalently, a design is checked against a functional specification given by e.g. a testcase with reference output or a user-defined property. Another research direction takes the view of a SystemC design as a piece of concurrent software. The design is then checked for common concurrency problems and thus, a functional specification is not required. Along this line, several methods for deadlock detection and race analysis have been developed. In this work, we propose to consider a new concurrency verification problem, namely input-output determinism, for SystemC designs. That means for each possible input, the design must produce the same output under any valid process schedule. We argue that determinism verification is stronger than both deadlock detection and race analysis. Beside being an attractive correctness criterion itself, proven determinism helps to accelerate both simulative and formal verification. We also present a preliminary study to show the feasibility of determinism verification for SystemC designs.
12:30		End of session Lunch Break in Exhibition Area Sandwich lunch