Tools and Techniques for Property-Based Requirements Engineering

Here, you will find the public deliverables for workpage 1, Tools and Techniques for Property-Based Requirements Engineering.

Task 1.1. Methodology Development

Executive Summary
Deliverable name	Property-Driven Specification of VLSI design					link	pdf
number	D1.1/1	lead	IBM-HRL	due	6	delivered	20040630, reissue 20050501
Related Deliverables
This report describes a PSL-based methodology for Property-Driven Specification of VLSI design. PSL provides a means to write specifications that are both easy to read and mathematically precise. Thus, one important use of PSL is for documentation, either in place of or, more typically, in conjunction with a natural language specification. The PSL specification can then be used as input to the design phase, which benefits from a more precise starting point for logic design. In the verification phase, the PSL specification is reused to support the increasingly popular ABV style of verification. The purpose of this document is to describe a methodology for the use of PSL in the specification phase. Before commencing to describe the methodology, we briefly describe the PROSYD vision for the use of PSL throughout the design cycle, in order to better motivate the specification methodology described. We then provide the methodology itself. Finally, we present an example specification in PSL.

Executive Summary
Deliverable name	Reuse-aware property-driven specification					link	pdf
number	D1.1/2	lead	STM-UK	due	13	delivered	20050125
Related Deliverables
It is desirable to write properties of a design in such a way that they can be reused. This document analyses the different ways in which properties may be reused, and how properties can be written so as to facilitate the various types of reuse. It provides guidelines and illustrative examples.

Executive Summary
Deliverable name	Property-by-Example guide: a handbook of PSL/Sugar examples					link	pdf
number	D1.1/3	lead	IBM-HRL	due	8	delivered	20040831, reissue 20050501
Related Deliverables
PSL is currently being used by hardware designers, architects, and verification engineers, for specification and verification of hardware. Newcomers to PSL begin by learning the language basics: the syntax and semantics. However, experience shows that after mastering these building blocks, some users still encounter difficulties when they begin writing PSL properties in real-life settings. Beginners, facing the wealth of choices offerred by the language, require guidance in choosing the best way to write a property. This document aims to alleviate such initial difficulties by guiding the reader through a set of real-life examples, representing typical properties that may be encountered in everyday work. Each example is explained both graphically and verbally, and is accompanied by a discussion, in order to answer questions that frequently arise in the writing of PSL. The main section of this document, Section 2, presents a set of properties that were used in a real-life hardware verification project. Each property is accompanied by alternative properties, either equivalent to the original property or otherwise related to it. The equivalent properties illustrate various styles of writing, and provide advice on good writing style. Related but non-equivalent properties are presented in order to prevent commonly occurring errors, by pointing out subtle differences that an inexperienced user may not be aware of. Common forms of properties are presented, to help the user identify the template that is most appropriate for each case. All of the properties are accompanied by timing diagrams, which illustrate possible behaviours described by each property, and point out the differences between nonequivalent properties. An additional set of typical properties is presented in Section 3. These properties were not taken from a single hardware design project, but were collected from various contexts, in order to illustrate interesting uses of PSL constructs.

Task 1.2. Research and Development

Executive Summary
Deliverable name	Research report on property simulation					link	pdf
number	D1.2/1	lead	TU Graz	due	9	delivered	20040930, reissue 20050501
Related Deliverables	D1.2/4
Properties in PSL may be hard to understand. What is currently provided to help designers in developing a clear understanding of the language is not enough. The material is either not comprehensive (like tutorials and examples handbooks), or it is not suitable for professionals that do not have a proper education in formal methods (like the formal semantics in the PSL Language Reference Manual). When a design fails a property, it may be because the design is incorrect, or because the property is incorrect. Worse, due to a misunderstanding of the semantics, the property could actually express something different from what the designer has in mind, and in this case, the propertys passing is meaningless. In order to minimize such cases, it is essential that the meaning of a property is absolutely clear to the user. The main factor inhibiting the understanding of properties is that a specification in PSL is currently not executable. This work aims to alleviate that drawback by proposing an automated method of deriving example traces from properties. Two concerns are of importance: 1. A designer needs to be able to explore the property by proposing constraints on the traces and asking the tool if a trace exists that satisfies the constraints and the property. 2. A representative overview of the behavior of the property must be given. We propose a tool that helps a designer explore a property, show the theory underlying the functioning of the tool, and provide a mockup of the tool to illustrate the interaction with the tool. We discuss some alternatives for presenting the output of the tool and discuss their relative merit. The research is expected to benefit both novices and expert verification engineers, the former for the exploration of simple properties, and the latter for the understanding of the interaction between properties in a larger set of interacting properties. The concept of property simulation is novel to this paper. There are as yet no interactive tools to help a designer understand a property. We build on existing work in temporal logics, and extend it with novel approaches to visualize properties, to capture user constraints, to find properties that are interesting, and to make sure that all possible behavior allowed by the property is captured in simulation. We propose two novel technical approaches for property simulation based on Büchi automata and Separated Normal Form, respectively. The main advantage of Separated Normal Form is its efficiency, but Büchi automata are amenable to coverage techniques. We are studying methods to combine the two approaches.

Executive Summary
Deliverable name	Novel techniques for property assurance					link	pdf
number	D1.2/2	lead	ITC-Irst	due	8	delivered	20040831
Related Deliverables	D1.2/5
Property assurance is the activity of eliciting requirements that really capture the designer intent within the development of systems adopting a property-based approach in such a way that the design process is guided by the set of properties that the systems are called to satisfy. The way this activity is performed is dictated by a methodology that guarantees the correctness of the activity itself and prescribes how to develop a specification out of a set of initial properties: the methodology defines what to do, how to do it and which technologies to use. Property assurance is not the activity of producing an implementation that satisfies given properties; the focus is on the specification phase, and the step from a specification to an implementation that is correct with respect to the specification is up to other activities (e.g. property synthesis), methodologies and technologies. Sinergies between property assurance and property synthesis do exist. Indeed, integrated in a process together with property synthesis, property assurance may provide a way to ease the delivery of implementations, written for example in VHDL or Verilog, that satisfy by construction a given set of properties written in a property specification language like PSL/Sugar. Since implementations automatically synthesized from a set of properties could be not as efficient and performing as hand written code, the coupling property assurance/property synthesis could not fit the development of performance-driven systems. Other interesting results could stemp up from the coupling property assurance/property simulation as far as the understanding of specifications and the training of designer on temporal formalisms are regarded. The input of property assurance is a set of properties/requirements that describe the behaviour of the system and possibly of the environment. Among the system properties there are those which are assumed to hold and those that must be guaranteed to hold given the assumptions. The output is a requirements specification of a system that satisfies those properties. In the setting of the PROSYD project, the reference specification formalism is PSL/Sugar, consequently, both the input and the output are given as a collection of logical and temporal relationships between and among subordinate Boolean expressions, sequential expressions, and other properties that in aggregate represent a set of behaviors. People involved in any phase of the design and implementation of a system would greatly benefit from the introduction of a property assurance based methodology; indeed, having a property based approach and a methodology that allows deriving a specification from a set of properties (from the initial set of rather abstract and general assertions about the system and the environment, to a detailed description of its behaviour) would help to better define the interfaces between the various phases of the system development process and would foster a better and smoother integration of formal methods in hardware design.

Executive Summary
Deliverable name	Front-end for PSL/Sugar					link	tar
number	D1.2/3	lead	IBM-HRL	due	9	delivered	20040901/20050412
Related Deliverables	D1.2/6
Individuals and EDA companies are encouraged to use the PSL/Sugar language as a frontend for assertion-based verification. The PSL/Sugar Parser is available herein in source code, and accessing it will require acceptance of the terms of the simple IBM Common Public License.

Executive Summary
Deliverable name	Manual for Property Assurance and Simulation tool					link	pdf tar
number	D1.2/4-5	lead	TU Graz	due	23	delivered	20051130
Related Deliverables	D1.2/1 D1.2/2
This document describes the results of the joint effort for PROSYD Deliverable D1.2/4-5. We have developed and implemented RAT, a requirements analysis tool that supports the designer in understanding and developing a specification in PSL.The tool implements the Property Assurance methodology described in Deliverable D1.2/2 and the Property Simulation methods described in Deliverable D1.2/1. Together, these techniques allow for a principled construction of a correct specification, and allow the user to explore the behavior of the constructed specification. In this document, we describe a requirements analysis methodology, and the design and implementation issues for RAT. We include the user manual and installation instructions. RAT s web home is http://rat.itc.it.

Executive Summary
Deliverable name	Manual for Textual property specification tool					link	pdf
number	D1.2/6	lead	IBM-HRL	due	20	delivered	20050901/20051220
Related Deliverables	D1.2/3
PSLText is a tool for editing of PSL code. It is part of the Prosyd toolset, and is used in the framework of the Prosyd methodology. PSLText is especially intended for use during the specification stage of the Prosyd methodology, in which the architect augments an English specification document with PSL statements, thus clarifying and formalizing the intention of the English text. These PSL staterments are written using the PSLText tool. PSLText features for supporting this methodology include syntax colouring (displaying code elements in various colours according to functionality), automatic indentation (according to the structure of the code), and one-click insertion of reference comments (for inserting information connecting the PSL code to the English specification text). PSLText supports two PSL flavours: Verilog flavour and GDL flavour. PSLText has been implemented as a plug-in for XEmacs, which is an open source text editor. PSLText functions as a PSL language mode within XEmacs. It can be installed as an extension to any existing XEmacs installation. PSLText is based on a pre-existing XEmacs language mode for the Sugar 2.0 language (in GDL flavour only), which was developed by IBM. The work on PSLText incudes two major upgrades to the pre-existing tool: Support for Verilog flavour has been added; The supported language has been upgraded from Sugar 2.0 to PSL. In addition, a user manual has been written for the PSLText tool.

Executive Summary
Deliverable name	Research report on property realizability.					link	pdf
number	D1.2/7	lead	ITC-irst	due	28	delivered	20060501
Related Deliverables	D1.2/8
This document describes the theory of property realizability. Property realizability is the preliminary check before property synthesis which in turn deals with automatically synthesizing a design from a specification given in the linear-time fragment of PSL. In this document we review the theory of realizability and the techniques used so far to tackle this problem. Then we identify sufficient conditions for checking the realizability or unrealizability of a specification and we provide a description of the we identified to verify those conditions. The algorithms can then be implemented using BDD or QBF techniques, both approaches are discussed. Finally we consider the problem of showing the designer useful debugging information.

Executive Summary
Deliverable name	Manual for property realizability tool.					link	pdf tar
number	D1.2/8	lead	ITC-irst	due	36	delivered	20061227
Related Deliverables	D1.2/7 D1.2/4-5
This documents describes a tool based on the model checkers NuSMV and VIS able to deal with property realizability problems. Also the theory the tool is based on is explained. Property realizability is the preliminary check before property synthesis which in turn deals with automatically synthesizing a design from a specification given in the linear-time fragment of PSL. For more information on the theory of realizability see the previous research report D1.2/7.

Task 1.3. Language Extensions

Executive Summary
Deliverable name	Extending PSL for Analog Circuits					link	pdf
number	D1.3/1	lead	Verimag	due	14	delivered	20050214
Related Deliverables	D1.3/2
This document is a first proposal for an extension of PSL toward real-time and analog properties. It represents mainly the work of Verimag and Weizmann with a participation of ST in giving insights about the the design and validation of such circuits. Additional useful information about analog design was provided by sources outside PROSYD, including Dolphin SA, CEA/LETI, Intel, Professors Rutenbar and Krogh from CMU and Prof. Hedrich from Hannover.

Deliverable name	Final Proposal for PSL Analog extensions					link	pdf
number	D1.3/2	lead	Verimag	due	36	delivered	20061231
Related Deliverables	D1.3/1
Executive Summary	This document presents the final proposal for an extension of PSL toward realtime and analog properties. It is based on the results described in Deliverable 1.3/1 and on the feedback from the analog designers of STMicroelectronics Italy. The resulting STL/PSL language allows to specify properties of analog and mixed-signal systems. STL/PSL logic is mainly intended to be used for lightweight verification of such properties.

Task 1.4. Case Studies

Deliverable name	Joint report 1 Case studies in property based requirements specification					link	pdf (Wishbone spec annex)
number	D1.4/1	lead	STM-Italy	due	33	delivered	20061101
Related Deliverables	D1.1/1 D1.1/2 D1.1/3 D1.5/1 D1.2/4-5 D1.2/6 D3.2/7 D3.2/8 D3.2/17 D3.4/1
Executive Summary This report describes twelve case studies on a wide range of designs and communication architectures currently under development in system-on-chip projects of large semiconductor companies. In the case studies, property-based specifications in PSL are constructed, guided by the methodology documents and supported by the tools in Workpackage 1. It is shown how the specifications cover the architectures or the functionalities of the designs. The contribution of the tools is evaluated, and the overall productivity benefits of a property-based specification approach are assessed.

Task 1.5. Development of Property Libraries and Repositories

Deliverable name	Manual for Repositories of PSL/Sugar properties					link	pdf
number	D1.5/1	lead	STM-France	due	36	delivered	20061231
Related Deliverables	D1.1/2
Executive Summary Reuse is widely spread in the hardware design flows and concerns all the involved materials including properties. The goal of this task is to develop sets of PSL properties that can be reused for differing designs. These properties cover essential areas of hardware designs, protocols, FIFOs, stacks and configuration registers.

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