10.7 Expanding the Applicability of Formal Methods

Date: Thursday 12 March 2015
Time: 11:00 - 12:30
Location / Room: Les Bans

Chair:
Barbara Jobstmann, École Polytechnique Fédérale de Lausanne (EPFL), CH

Co-Chair:
Christoph Scholl, University Freiburg, DE

The first two papers propose improved solutions for error diagnosis and software bounded model checking. The next two papers are devoted to abstraction and synthesis techniques between RTL and high-level models of on-chip communication networks. Then the first IP expands the applicability of equivalence checkers to asynchronous circuits. The last two IPs present emerging applications of model checking.

Time	Label	Presentation Title Authors
11:00	10.7.1	AUTOMATED RECTIFICATION METHODOLOGIES TO FUNCTIONAL STATE-SPACE UNREACHABILITY Speakers: Ryan Berryhill and Andreas Veneris, University of Toronto, CA Abstract In the modern design cycle significant manual resources are dedicated to fix a design when verification shows that a state is not reachable. As traditional debugging typically involves the use of an error trace that exhibits the problem, there is little automation to aid an engineer understand why a state is not reachable and how to correct this problem. This paper presents a novel methodology that automates this task. In detail, a process that involves intertwined steps of state approximation, reachability analysis and traditional debugging is developed to identify design locations where fixes can be applied so the target state becomes reachable. An initial formulation identifies such error locations when the target state is reachable directly from the reachable set of states. This is later extended for the cases where more than one state transition is required to reach an unreachable state from the existing reachable set. Empirical results on industrial level designs show a performance which is orders of magnitude faster than the state-of-the-art confirming the practicality of the proposed automated methodology. Download Paper (PDF; Only available from the DATE venue WiFi)
11:30	10.7.2	OVER-APPROXIMATING LOOPS TO PROVE PROPERTIES USING BOUNDED MODEL CHECKING Speakers: Priyanka Darke, Bharti Chimdyalwar, Venkatesh R, Ulka Shrotri and Ravindra Metta, TCS, IN Abstract Bounded Model Checkers (BMCs) are widely used to detect violations of program properties up to a bounded execution length of the program. However when it comes to proving the properties, BMCs are unable to provide a sound result for programs with loops of large or unknown bounds. To address this limitation, we developed a new loop over-approximation technique LA. LA replaces a given loop in a program with an abstract loop having a smaller known bound by combining the techniques of output abstraction and a novel abstract acceleration, suitably augmented with a new application of induction. The resulting transformed program can then be fed to any bounded model checker to provide a sound proof of the desired properties. We call this approach, of LA followed by BMC, as LABMC. We evaluated the effectiveness of LABMC on some of the SV-COMP14 loop benchmarks, each with a property encoded into it. Well known BMCs failed to prove most of these properties due to loops of large, infinite or unknown bounds while LABMC obtained promising results. We also performed experiments on a real world automotive application on which the well known BMCs were able to prove only one of the 186 array accesses to be within array bounds. LABMC was able to successfully prove 131 of those array accesses to be within array bounds. Download Paper (PDF; Only available from the DATE venue WiFi)
12:00	10.7.3	AUTOMATIC EXTRACTION OF MICRO-ARCHITECTURAL MODELS OF COMMUNICATION FABRICS FROM REGISTER TRANSFER LEVEL DESIGNS Speakers: Sebastiaan Joosten and Julien Schmaltz, Eindhoven University of Technology, NL Abstract Multi-core processors and Systems-on-Chips are composed of a large number of processing and memory elements interconnected by complex communication fabrics. These fabrics are large systems made of many queues and distributed control logic. Recent studies have demonstrated that high levels models of these networks are either tractable for verification or can provide key invariants to improve hardware model checkers. Formally verifying Register Transfer Level (RTL) designs of these networks is an important challenge, yet still open. This paper bridges the gap between high level models and RTL designs. We propose an algorithm that from a Verilog description automatically produces its corresponding micro-architectural model. We prove that the extracted model is transfer equivalent to the original RTL circuit. We illustrate our approach on a typical example of communication fabrics: a scoreboard with credit-flow control. Download Paper (PDF; Only available from the DATE venue WiFi)
12:15	10.7.4	GALS SYNTHESIS AND VERIFICATION FOR XMAS MODELS Speakers: Frank Burns, Danil Sokolov and Alex Yakovlev, Newcastle University, GB Abstract In this paper a novel Globally Asynchronous Locally Synchronous~(GALS) synthesis and verification environment is introduced for xMAS models. xMAS models are a new communication paradigm which can be used to model circuits and networks for the purpose of synthesis, testing and verification. Previous attempts at synthesis and verification of xMAS models have been proposed for synchronous implementations only. This paper provides an extension of xMAS and translation into Circuit Petri net models for GALS synthesis and verification. Synthesis techniques based on Circuit Petri net translation are presented and a new xMAS component is introduced which acts as a wrapper for different GALS styles. Novel verification techniques using unfolding to occurrence nets are then proposed. Our results show that the work presented here provides a suitable platform for integrating xMAS into a GALS environment. Download Paper (PDF; Only available from the DATE venue WiFi)
12:30	IP5-7, 299	LOGICAL EQUIVALENCE CHECKING OF ASYNCHRONOUS CIRCUITS USING COMMERCIAL TOOLS Speakers: Arash Saifhashemi¹, Hsin-Ho Huang², Priyanka Bhalerao³ and Peter Beerel² ¹Intel, US; ²University of Southern California, US; ³yahoo, US Abstract We propose a method for logical equivalence check (LEC) of asynchronous circuits using commercial synchronous tools. In particular, we verify the equivalence of asynchronous circuits which are modeled at the CSP-level in SystemVerilog as well as circuits modeled at the micro-architectural level using conditional communication library primitives. Our approach is based on a novel three-valued logic model that abstracts the detailed handshaking protocol and is thus agnostic to different gate-level implementations, making it applicable to a variety of different design styles. Our experimental results with commercial LEC tools on a variety of computational blocks and an asynchronous microprocessor demonstrate the applicability and limitations of the proposed approach. Download Paper (PDF; Only available from the DATE venue WiFi)
12:31	IP5-8, 219	MAY-HAPPEN-IN-PARALLEL ANALYSIS OF ELECTRONIC SYSTEM LEVEL MODELS USING UPPAAL MODEL CHECKING Speakers: Che-Wei Chang and Rainer Doemer, University of California Irvine, US Abstract In this paper, we propose an approach for May- Happen-in-Parallel (MHP) analysis of electronic system level (ESL) design which models parallel discrete event simulation with concurrent automaton processes and formally identify those MHP states. Our MHP analysis utilizes formal verification by use of the UPPAAL model checker. The proposed approach converts the system model in SpecC SLDL into an UPPAAL model and generates a set of queries that automatically and completely finds all possible MHP pairs. The experimental results show our approach can report more precise MHP analysis results compared to other works at the cost of extended analysis run time. Download Paper (PDF; Only available from the DATE venue WiFi)
12:32	IP5-9, 583	VERIFYING SYNCHRONOUS REACTIVE SYSTEMS USING LAZY ABSTRACTION Speakers: Kumar Madhukar¹, Mandayam Srivas², Bjorn Wachter³, Daniel Kroening³ and Ravindra Metta¹ ¹Tata Research Development and Design Center, IN; ²Chennai Mathematical Institute, IN; ³University of Oxford, GB Abstract Embedded software systems are frequently modeled as a set of synchronous reactive processes. The transitions performed by the processes are given as sequential, atomic code blocks. Most existing verifiers flatten such programs into a global transition system, to be able to apply off-the-shelf verification methods. However, this monolithic approach fails to exploit the lock-step execution of the processes, severely limiting scalability. We present a novel formal verification technique that analyses synchronous concurrency explicitly rather than encoding it. We present a variant of Lazy Abstraction with Interpolants (LAWI), a technique successfully used in software verification, and tailor it to synchronous reactive concurrency. We exploit the synchronous communication structure by fixing an execution schedule, circumventing the exponential blow-up of state space caused by simulating synchronous behaviour by means of interleavings. The technique is implemented in SYMPARA, a verification tool for synchronous reactive systems. To evaluate the effectiveness of our technique, we compare SYMPARA with Bounded Model Checking and k-induction, and a LAWI-based verifier for multi-threaded (asynchronous) software. On several realistic examples SYMPARA outperforms the other tools by an order of magnitude. Download Paper (PDF; Only available from the DATE venue WiFi)
12:30		End of session Lunch Break, Keynote lecture from 1320 - 1350 (Room Oisans) in Les Écrins Coffee Break in Exhibition Area On all conference days (Tuesday to Thursday), coffee and tea will be served during the coffee breaks at the below-mentioned times in the exhibition area. Lunch Break On Tuesday and Wednesday, lunch boxes will be served in front of the session room Salle Oisans and in the exhibition area for fully registered delegates (a voucher will be given upon registration on-site). On Thursday, lunch will be served in Room Les Ecrins (for fully registered conference delegates only). Tuesday, March 10, 2015 Coffee Break 10:30 - 11:30 Lunch Break 13:00 - 14:30; Keynote session from 13:20 - 14:20 (Room Oisans) sponsored by Mentor Graphics Coffee Break 16:00 - 17:00 Wednesday, March 11, 2015 Coffee Break 10:00 - 11:00 Lunch Break 12:30 - 14:30, Keynote lectures from 12:50 - 14:20 (Room Oisans) Coffee Break 16:00 - 17:00 Thursday, March 12, 2015 Coffee Break 10:00 - 11:00 Lunch Break 12:30 - 14:00, Keynote lecture from 13:20 - 13:50 Coffee Break 15:30 - 16:00