Tools and Techniques for Property-Based Design

Here, you will find the public deliverables for workpage 2, Tools and Techniques for Property-Based Design.

Task 2.1. Methodology Development

Executive Summary
Deliverable name	Property-driven design and implementation					link	pdf
number	D2.1/1	lead	TU Graz	due	8	delivered	20040831, reissue 20050519
Related Deliverables

|This document describes the methodology of property-based error localization and property-based synthesis, which together form Workpackage 2. Error localization addresses the problem of debugging. When a failure is detected during the verification of a block, finding the fault that causes it can be very time consuming. This lengthens the design cycle, often right before delivery time, when delays are especially bothersome. Error localization aims to automatically find and, if possible, correct the fault, thus freeing up designer resources for more complex and creative tasks such as design. We consider the design cycle of a block to consist of specification, design, and repeated iterations of detecting the presence of a fault followed by localization and correction. Automating the detection of a fault is the aim of verification tools; fault localization aims to automate the second step, and correction automates the last. The supervision of a designer remains necessary even for automatic correction, to make sure that the suggested correction adheres to unstated or non-functional requirements. Property synthesis aims to shorten the design cycle by automating the process of designing a block. We identify the following benefits: 1. The need to hand-code blocks that are not area or timing critical is removed. Automatically generated blocks are guaranteed to fulfill their functional specifications. 2. Designers can develop their block in the presence of a fully operational environment because functional prototypes of blocks can be created right after specification. Thus, integration testing can start right away and a major source of design mistakes is circumvented. Also, prototypes can be used as a starting point for an efficient hand implementation. 3. Specification faults are found very early in the design process, as they are immediately apparent in the synthesized system. Thus, a correct specification is obtained earlier and incorrect implementations are avoided. Both error localization and property synthesis aim to automate important parts of the design flow, shortening it and reducing time to market.

Task 2.2. Research and Development

Executive Summary
Deliverable name	Property-based logic synthesis for rapid design prototyping					link	pdf
number	D2.2/1	lead	TU Graz	due	20	delivered	20050901
Related Deliverables	D2.2/3 D2.3/1
This document describes the theory of property-based synthesis. Property-based synthesis deals with automatically synthesizing a design from a specification given in the linear-time fragment of PSL.We describe three different approaches to handle property-based synthesis. These approaches are complementary: they are able to synthesize different subsets of PSL with different degrees of computational complexity. The more complete the fragment is, the more expensive is synthesis, and we show three different tradeoffs to this question. The nondeterministic approach is based on an automata oriented approach to PSL model checking. It can only synthesize a subset of PSL, but can do so very efficiently. This approach is likely to be too limited for general synthesis but is very well suited for a limited synthesis problem, namely that of completion of partially implemented systems. Completion of partially implemented systems can be used to repair faulty systems, a novel and very relevant application, at a reasonable cost [SB05]. The approach of synthesis from generalized reactivity[1] specifications works for a larger class of specifications, more precisely for all specifications expressible using a generalized reactivity[1] acceptance condition. The basic idea of this approach is to transform the specification into a particular form to which a triply nested fixpoint algorithm can be applied. Its complexity is expected to be feasible even for large sets of specifications. Third, we present a complete approach that is applicable to the entire linear-time fragment of PSL. Its complexity bound is doubly exponential. This approach is primarily applicable for cases in which the other two approaches fail.

Executive Summary
Deliverable name	Property-based error localization					link	pdf
number	D2.2/2	lead	TU Graz	due	16	delivered	20050501
Related Deliverables	D2.2/4 D2.3/2
Property verification tools, be they static or dynamic, yield a trace as evidence that a design violates a property. Getting from a trace to the cause of the failure can be very time consuming. The subject of this work is to automate the localization of a fault. We present two methods. The correction approach combines fault localization with correction. If a property is violated, the method finds the possible locations for the fault and suggests corrections. We state the localization and correction problem as a game that is won if there is a correction that is valid for all possible inputs. This is a very powerful fully automatic method. For invariants, the most frequently used class of properties, the method is complete. The approach is based on a heuristic, therefore for complex general PSL properties we cannot guarantee that a correction is found, but in most cases we are successful. Finding a correction may be hard for complex circuits. For large and complex circuits we introduce our localization approach. This method does not find corrections, but is based on consistency of the observations. It does not guarantee that all locations marked as suspicions can actually be used to correct the design, but it reduces the amount of the design to be inspected to a fraction and is computationally much easier. We provide an example where the number of components to be considered faulty is reduced to 7% of all components.

Executive Summary
Deliverable name	Manual for Property-based synthesis tool					link	pdf
number	D2.2/3	lead	TU Graz	due	31	delivered	20060813
Related Deliverables	D2.2/1 D2.3/1
We present our property-based synthesis tool Lily. Given a set of properties written in the linear-time fragment of PSL and a partition of the signals used in those properties into input and output signals, Lily synthesizes a functionally correct design for the given properties. The synthesized design, a finite state machine, is provided as a VERILOG module or as a labeled directed graph in DOT format. This document states how to use and install Lily and gives technical and theoretical details about the tool.

Executive Summary
Deliverable name	Manual for Property-based error localization tool					link	pdf
number	D2.2/4	lead	TU Graz	due	32	delivered	20060905
Related Deliverables	D2.2/2 D2.3/2
Property verification tools, be they static or dynamic, yield a trace as evidence that a design violates a property. Getting from a trace to the cause of the failure can be very time consuming. The subject of our tool Bufi is to automate the localization of a fault. Bufi reduces the amount of the design to be inspected to a fraction of its original size and is computationally comparable to bounded model checking. This document explains how to use Bufi and gives the technical and theoretical background of the tool.

Deliverable name	Research report on timed/analog synthesis					link	pdf
number	D2.2/5	lead	Verimag	due	36	delivered	20070101
Related Deliverables
Executive Summary	The present report describes the effort invested within the PROSYD project in order to develop the theoretical and algorithmic infrastructure for applying controller synthesis algorithms to timed and analog circuits. It includes a survey on synthesis algorithm for timed and hybrid automata, a new class of algorithms for optimal continuous control as well as work in progress on synthesizing circuits directly from high-level specifications, expressed using the real-time temporal logic MTL underlying the analog extension of PSL.

Task2.3. Case Studies

Executive Summary
Deliverable name	Evaluation of tools and methodology for property-based logic synthesis					link	PDF
number	D2.3/1	lead	TU Graz	due	36	delivered
Related Deliverables	D2.2/1 D2.2/3
In this document we describe two case studies that we performed using the property-based synthesis techniques developed in the PROSYD project. The first case study is the generalized buffer, an IBM tutorial design used also in the error localization case study. The second case study is the arbiter for ARM's AHB bus. This case study demonstrates that property synthesis can be used for real life commercial control blocks. Automatic synthesis of logic from its specification has long been considered an unattainable dream. The conclusions of the case studies are that it is no longer a ream. Although we still run in to size restrictions relatively early, we are able to synthesize realistic examples. In this document, we show the specifications that we derived for the two case studies, we describe how to generate circuits from the results of the synthesis algorithm, and we discuss the benefits and disadvantages of property-based synthesis.

Executive Summary
Deliverable name	Evaluation of tools developed for error localization					link	pdf
number	D2.3/2	lead	IBM-HRL	due	36	delivered	20061231
Related Deliverables	D2.2/2 D2.2/4
Property verification tools yield a trace as evidence that a design violates a property. Getting from the trace to the cause of the failure can be very time consuming. The property-based error localization tool, Bufi, is aimed at automating the localization of a fault. This work describes case studies performed on this tool by both IBM and OneSpin^?. The contribution and usefulness of the tool are evaluated; and the conditions under which the tool is beneficial are discussed.

Executive Summary
Deliverable name	Report on experiences in property based design					link	pdf
number	D2.3/3	lead	IBM-HRL	due	36	delivered	20061225
Related Deliverables	D2.3/1 D2.3/2
This document provides a summary of PROSYD experience with case studies on the property-based synthesis and error-localization tools derived in work package WP2. Two synthesis and four error-localization case studies are discussed. The performance and usefulness of algorithms and tools are evaluated; and the conditions on tools efficiency are discussed.

Public

Webs
Main
Public
Sandbox
TWiki

Copyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback