Public WebTools and Techniques for Property Verification
Here, you will find the public deliverables for workpage 3, Tools and Techniques for Property Verification.Task 3.1. Methodology Development
| Deliverable name | Methodology document on managing the trade-offs between robustness and coverage in a combined static and dynamic verification environment | link | |||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D3.1/1 | lead | Infineon | due | 6 | delivered | 20040621/20050331 | ||
| Related Deliverables | |||||||||
| Executive Summary | |||||||||
| This document describes important aspects concerning advanced combined static and dynamic verification flows. Important aspects of such a combined flow include modelling the environment, technology impact on properties, content of properties for the various design phases, and interaction of static and dynamic checking. Further we discuss methodology and management aspects as well as tool and language specific requirements. | |||||||||
| Deliverable name | Methodology document on effective leverage of various static checking engines. | link | |||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D3.1/2 | lead | IBM-HRL | due | 15 | delivered | 20050331, posted 20050516 | ||
| Related Deliverables | |||||||||
| Executive Summary | |||||||||
| Model checking (MC) is a way to verify logic designs against certain desired properties. Model checkers exhaustively check all possible input sequences, or search all possible reachable design states. This methodology document provides guidance for the effective leverage of various model-checking and semi-formal engines, based on design characteristics such as block size, sequential depth, function, and maturity. It presents a method for managing the trade-off between performance and coverage in a platform that uses among other static engines classical SMV-based model checker and a Boolean satifiability (SAT) bounded model checker. | |||||||||
Task 3.2. Research and Development
| Deliverable name | Research report on improved decision heuristics for high-performance SAT-based static property checking. | link | pdf annex pdf | ||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D3.2/1 | lead | IBM-HRL | due | 6 | delivered | 20040701/20050508, annex 20041101/20050508 | ||
| Related Deliverables | D3.2/7 D3.2/8 D3.2/9 | ||||||||
| Executive Summary | |||||||||
| This document contains important aspects of SAT Solver performances and specification for improving this performance. | |||||||||
| Deliverable name | Research report on improved symbolic search strategies and model reduction for static property checking. | link | |||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D3.2/2 | lead | IBM-HRL | due | 15 | delivered | 20050315/20050321 | ||
| Related Deliverables | D3.2/7 D3.2/8 D3.2/9 | ||||||||
| Executive Summary | |||||||||
| Model checking is a way to verify logic designs against certain desired properties of the designs. Model checkers exhaustively check all possible input sequences, or search all possible reachable design states. To do this efficiently, the design is usually transformed into a logically equivalent design by a series of transformations called reductions. The design after reductions should be easier to explore exhaustively. This research report examines two specific reductions, the first called retiming reduction and the second called quantifier reduction. We discuss various implementation issues, and check the effectiveness of both empirically. We conclude that using the retiming reduction is effective in only a small set of problems. For other designs, the retiming reduction simply transforms a given problem into an equivalently hard problem. Quantifier reduction is very successful in reducing model checking time, but is usually very time-consuming by itself. Therefore, quantifier reduction, as described in this report, shows no significant improvement in the overall verification time. | |||||||||
| Deliverable name | Research report on exploitation of RT information in static property checking algorithms. | link | |||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D3.2/3 | lead | Infineon | due | 6 | delivered | 20040616/20050331 | ||
| Related Deliverables | D3.2/7 D3.2/8 D3.2/9 | ||||||||
| Executive Summary | |||||||||
| This document describes an approach for preserving the RTL structure of designs and properties to be exploited in property checking algorithms. Two approaches, for preprocessing such problems are considered, namely symmetry reduction and date path scaling, and the effects are outlined. | |||||||||
| Deliverable name | Research report on automata construction algorithms optimized for PSL/Sugar (static checking) | link | |||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D3.2/4 | lead | TU Graz | due | 18 | delivered | 20050630 | ||
| Related Deliverables | D3.2/10 | ||||||||
| Executive Summary | |||||||||
| Property verification and synthesis tools work with automata to represent both the model to examine and the property to check. Subject of this work is to show the steps necessary for creation of automata for properties given in PSL. Automata construction for the temporal logic LTL is a well known problem. We extend this to automata for the core of PSL, denoted here LTL WR. The extensions over LTL take two directions: First, the logic is interpreted over finite, possibly truncated as well as infinite words. In another direction, the new basic formulas for weak and strong regular expressions and operators to combine them with other formulas are added to the language. The regular expressions used in Sugar extend the usual one by the intersection operator ("length-matching sequence conjunction"). We show that for every LTL WR formula j there exists a Büchi automaton whose size is doubly exponential in the size of j. We discuss how the suggested constructions can be used in the process of model checking PSL properties using the automata-theoretic approach. We further show an efficient algorithm to derive a symbolic representation for a subset of the language. The work presented here is easily extended to the full foundation language of PSL, which extends LTL WR by a set of abbreviations. | |||||||||
| Deliverable name | Research report on optimized dynamic property checking algorithms for digital designs | link | |||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D3.2/5 | lead | IBM-HRL | due | 20 | delivered | 20050901/20051225 | ||
| Related Deliverables | |||||||||
| Executive Summary | |||||||||
| We present algorithms for automatic generations of facilities intended for dynamic verifications - HDL simulation monitors (also known as checkers) and trace analyzers - from properties written in Property Specification Language (PSL). This deliverable presents a full development flow from basic algorithms and optimizations to descriptions of tool prototypes. | |||||||||
| Deliverable name | Research report on checking digital, timed and analog PSL/Sugar properties, based on 1.3/1. | link | |||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D3.2/6 | lead | Verimag | due | 25 | delivered | 20050207, posted 20050215 | ||
| Related Deliverables | D3.2/13 | ||||||||
| Executive Summary | |||||||||
| This report explores different approaches for extending property checking algorithms toward timed and analog signals. The purpose of this document is to survey different approaches to the problem checking whether individual simulation traces satisfy temporal properties, and to introduce new results on the topic obtained by the PROSYD consortium for timed and analog properties. | |||||||||
| Deliverable name | Improved static property checking tool, based on algorithmic framework reported in 3.2/1, 3.2/2. | link | |||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D3.2/7 | lead | IBM-HRL | due | 19 | delivered | 20050731, posted 20050920 | ||
| Related Deliverables | D3.2/1 D3.2/2 D3.2/3 | ||||||||
| Executive Summary | |||||||||
| The Achilles heel of Model Checking tools is the size problem. State-of-the-art tools, including RuleBasePE, are currently mostly used for block level verification, and only rarely for unit verification. In order for model checking to live up to its potential the tools need to scale to larger tasks. The purpose of this deliverable is to implement enhancements to the RuleBasePE model checking tool. These enhancements are a result of research, some of which was done in the scope of the PROSYD project, and some of which comes from academic published work. The deliverable encompasses enhancements to two of RuleBasePE's verification engines - the SAT engine, and SmartLoc - as well as a new engine called Interpolator. | |||||||||
| Deliverable name | Manual for Improved static property checking tool, based on algorithmic framework reported in 3.2/1, 3.2/2, 3.2/3. | link | |||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D3.2/8 | lead | Infineon | due | 18 | delivered | 20050630/20050724 | ||
| Related Deliverables | D3.2/1 D3.2/2 D3.2/3 | ||||||||
| Executive Summary | |||||||||
| The CVE static verification engine has been tuned using several optimisations. On a test-bench of PSL properties, an overall speed-up of more than 100% has been observed. | |||||||||
| Deliverable name | Manual for Improved static property checking tool, based on algorithmic framework reported in 3.2/1, 3.2/2. | link | |||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D3.2/9 | lead | ITC-Irst | due | 22 | delivered | 20051031 | ||
| Related Deliverables | D3.2/1 D3.2/2 D3.2/3 | ||||||||
| Executive Summary | |||||||||
| This document contains the description of the work performed under the effort for Deliverable D3.2/9 for the improvements of the NuSMV static property checking tool based on the algorithmic framework reported in Deliverable D3.2/1. | |||||||||
| Deliverable name | Manual for Tool for property-based synthesis of optimized Büchi automata for static analysis, based on algorithmic framework reported in 3.2/4. | link | pdf BuechiToolDownload | ||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D3.2/10 | lead | TU Graz | due | 32 | delivered | 20060903 | ||
| Related Deliverables | D3.2/4 | ||||||||
| Executive Summary | |||||||||
| In this deliverable we present an implementation of an optimized PSL automata construction. With our tool a designer can derive alternating and nondeterministic explicit automata from PSL formulae. Furthermore our tool offers the option of deriving a symbolic representation in the SMV format (used e.g. by the NuSMV [10] model checker) using a new approach we presented at the 11th International Conference on Implementation and Application of Automata, 2006 in [8]. We performed extensive experiments with our optimizations and symbolic representations, shown in [8]. | |||||||||
| Deliverable name | Manual for Property-based automatic generation of simulation monitors for digital designs, based on algorithmic framework reported in 3.2/5. | link | |||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D3.2/11 | lead | IBM-HRL | due | 30 | delivered | 20060702/20061210 | ||
| Related Deliverables | D3.2/5 | ||||||||
| Executive Summary | |||||||||
| This document provides a description of the simulation monitor optimization implemented inside IBM FoCs? – tool for automatic generation of simulation monitors from PSL specifications. The materials covered in the document offer background information – a basic description of the FoCs? tool, excerpts from the user guide and simulation monitor optimization implemented in the framework of this deliverable. | |||||||||
| Deliverable name | Manual for Property-based automatic generation of simulation monitors for digital, timed, and analog designs, based on algorithmic framework reported in 3.2/6. | link | |||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D3.2/13 | lead | Verimag | due | 36 | delivered | 20070101 | ||
| Related Deliverables | D3.2/6 | ||||||||
| Executive Summary | |||||||||
| Common property verification tools are usually designed for checking the correctness of discrete, and to a lesser extent real-time systems. The STL/PSL Monitor tool extends the formal methods to the continuous and mixed-signal domain by providing lightweight verification of properties on continuous and Boolean dense signals expressed in the STL/PSL logic. | |||||||||
| Deliverable name | Manual for Property-based analysis of simulation traces based on algorithmic framework reported in 3.2/5. | link | |||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D3.2/14 | lead | IBM-HRL | due | 30 | delivered | 20060628 | ||
| Related Deliverables | D3.2/5 | ||||||||
| Executive Summary | |||||||||
| This document provides a description of a trace analyzer tool for the postsimulation PSL specification-based analysis of the simulation traces. The materials in this document cover the basic description of the trace analysis process and provide a simple user's guide for the trace analysis tool. | |||||||||
| Deliverable name | Support for embedded PSL in Verilog Flavour - Static Checking. | link | |||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D3.2/15 | lead | IBM-HRL | due | 27 | delivered | 20060330 | ||
| Related Deliverables | D3.2/16 | ||||||||
| Executive Summary | |||||||||
| One of the challenges verification engineers must address while doing assertion-based verification is attaching behaviour checking properties to their correct context in the design. The RuleBase? PE static verification tool already supports one method of attaching properties to their context by binding the verification units. The purpose of this deliverable is to provide another method of attaching properties to their context in the design by writing them down where they should be attached—in other words, writing embedded assertions. | |||||||||
| Deliverable name | Support for embedded PSL in Verilog Flavour - observers. | link | |||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D3.2/16 | lead | IBM-HRL | due | 30 | delivered | 20060628 | ||
| Related Deliverables | D3.2/15 | ||||||||
| Executive Summary | |||||||||
| One of the challenges verification engineers must address while doing assertion based verification is attaching behaviour-checking properties to their correct context within the design. The PSL language provides a method known as 'binding' for attaching properties to their context; binding attaches the verification units to their relevant design units. This method is supported by FoCs?, the IBM tool for generation of simulation observers from PSL statements. The purpose of this deliverable is to extend FoCs? with the ability to generate observers from the properties that are written explicitly in the design and to attach them to the correct context—in other words, to generate observers from embedded assertions. | |||||||||
| Deliverable name | Fast simulation of property-based specification. | link | |||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D3.2/17 | lead | Onespin | due | 30 | delivered | 20060702 | ||
| Related Deliverables | |||||||||
| Executive Summary | |||||||||
| A method to write properties as an executable specification is presented. Rather than simulating the implementation-level details, the specification can thus be simulated, allowing for a speed-up over standard simulators. | |||||||||
| Deliverable name | Research report on static verification of analog design. | link | |||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D3.2/18 | lead | Verimag | due | 36 | delivered | 20070101 | ||
| Related Deliverables | |||||||||
| Executive Summary | |||||||||
| The present report describes the effort invested within the PROSYD project in order to bring verification of continuous and hybrid systems closer to industrial reality. It describes progress in three major reasearch directions: 1 Reachability computation: an adaptation of static digital verification methods to the analog domain, a kind of "set based" simulation. These methods are considered computationally hard and require sophisticated combination of numerical analysis, graph algorithms and computational geometry; 2) Simulation-based techniques: finding a finite set of trajectories that "cover" in some sense the reachable state space, and whose correctness implies correctness of all other trajectories; 3) Bisimulation metrics: an adaptation and refinement of the ideas underlying {\em equivalence checking} of digital systems to continuous systems. Naturally, these measures are quantitative and quantify the distance between the two compared systems. | |||||||||
Task 3.3. Porting of Tools
| Deliverable name | Manual for Port with VIS | link | pdf ToolDownloads | ||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D3.3/1 | lead | TU Graz | due | 18 | delivered | 20050630 | ||
| Related Deliverables | |||||||||
| Executive Summary | |||||||||
| We have ported VIS (Verification Interacting with Synthesis) to support model checking in PSL. We give installation instructions in Section 2. The detailed documentation of the VIS commands is distributed in electronic form. In Section 3, we give the syntax for the added commands (but not for the existing ones). Then, in Section 4, we give technical details of the implementation and the underlying theory. Finally, the appendix contains the new VIS user manual. | |||||||||
| Deliverable name | Manual for port of IBM-HRL tools | link | |||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D3.3/2 | lead | IBM-HRL | due | 18 | delivered | 20050630/20051220 | ||
| Related Deliverables | |||||||||
| Executive Summary | |||||||||
| PSL/Sugar originated as a proprietary language named "Sugar", which was used as the property specification language of the IBM tools. As part of the Accellera effort for standardizing a property specification language, IBM proposed an enhanced version of the Sugar language, with the name Sugar 2.0. The goal of this deliverable was to upgrade the input language of the IBM tools from the limited subset of Sugar 2.0 to PSL. This was done by adding support for new features, including entirely new support for the Verilog flavour, and by updating and expanding support for existing features, to bring them into compliance with the PSL standard. | |||||||||
| Deliverable name | Manual for port of Infineon tools | link | |||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D3.3/3 | lead | Infineon | due | 18 | delivered | 20050630/20050724 | ||
| Related Deliverables | |||||||||
| Executive Summary | |||||||||
| The CVE property checker has been enhanced to support properties written in the PSL language. | |||||||||
| Deliverable name | Manual for port of of NuSMV | link | pdf Tool Download | ||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D3.3/4 | lead | ITC-Irst | due | 19 | delivered | 20050719 | ||
| Related Deliverables | |||||||||
| Executive Summary | |||||||||
| This document contains the description of the work performed under the effort for Deliverable 3.4/4 for the porting of NuSMV to PSL. | |||||||||
Task 3.4. Case Studies
| Deliverable name | Joint report on case studies in property based verification | link | |||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D3.4/1 | lead | STM-Italy | due | 36 | delivered | 20061231 | ||
| Related Deliverables | D1.1/1 D1.1/2 D1.2/6 D1.4/1 D3.1/1 D3.1/2 D3.2/1 D3.2/2 D3.2/3 D3.2/5 D3.2/7 D3.2/8 D3.2/9 D3.2/11 D3.2/14 D3.2/15 D3.2/16 D3.2/17 D3.3/2 | ||||||||
| Executive Summary | |||||||||
| This report describes twelve case studies on a wide range of designs and communication architectures that had been under development in a number of large semiconductor companies during PROSYD life. In the case studies, property-based verification in PSL are constructed, guided by the methodology documents on property specification D1.1/1, on property reuse D1.1/2, on static/dynamic verification techniques combination D3.1/1, and on using different checking engines D3.1/2. Property verification activities have been supported by tools described in Workpackage 3. It is shown how the verification activities have been quantitatively and qualitatively affected by PROSYD outcomes: the contribution of the tools is evaluated, and the overall productivity benefits of a property-based verification approach are assessed. | |||||||||
| Deliverable name | Analog case study | link | |||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D3.4/2 | lead | Verimag | due | 36 | delivered | 20070101 | ||
| Related Deliverables | |||||||||
| Executive Summary | |||||||||
| This document describes the analog case study on a Flash memory simulation provided by ST Microelectronics Italy. The case study explores in practice the benefitsof extending formal specification to analog designs, by expressing the desired continuous behavior of the Flesh memory cell with the STL/PSL specification language developed during the project and described in Deliverables 1.3/1 [M05] and 1.3/2 [NM+06], and by checking its correctness with the STL/PSL Monitor tool presented in Deliverable 3.2/13 [NM06]. | |||||||||
Public Web
Create New Topic
Index
Search
Changes
Notifications
Statistics
Preferences
Main |
|
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