| Deliverable name | Property-Driven Specification of VLSI design | link | |||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D1.1/1 | lead | IBM-HRL | due | 6 | delivered | 20040630, reissue 20050501 | ||
| Related Deliverables | |||||||||
| Executive Summary | |||||||||
| Deliverable name | Reuse-aware property-driven specification | link | |||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D1.1/2 | lead | STM-UK | due | 10 | delivered | 20050125 | ||
| Related Deliverables | |||||||||
| Executive Summary | |||||||||
| Deliverable name | Property-by-Example guide: a handbook of PSL/Sugar examples | link | |||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D1.1/3 | lead | IBM-HRL | due | 8 | delivered | 20040831, reissue 20050501 | ||
| Related Deliverables | |||||||||
| Executive Summary | |||||||||
| Deliverable name | Research report on property simulation | link | |||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D1.2/1 | lead | TU Graz | due | 9 | delivered | 20040930, reissue 20050501 | ||
| Related Deliverables | |||||||||
| Executive Summary | |||||||||
| Deliverable name | Novel techniques for property assurance | link | |||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D1.2/2 | lead | ITC-Irst | due | 8 | delivered | 20040831 | ||
| Related Deliverables | |||||||||
| 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 | |||||||||
| Executive Summary | |||||||||
| Deliverable name | Manual for Property simulation tool | link | |||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D1.2/4 | lead | TU Graz | due | 21 | delivered | |||
| Related Deliverables | |||||||||
| Executive Summary | |||||||||
| Deliverable name | Manual for Property assurance tool | link | |||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D1.2/5 | lead | ITC-Irst | due | 22 | delivered | |||
| Related Deliverables | |||||||||
| Executive Summary | |||||||||
| Deliverable name | Manual for Textual property specification tool | link | |||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D1.2/6 | lead | IBM-HRL | due | 20 | delivered | |||
| Related Deliverables | |||||||||
| Executive Summary | |||||||||
| Deliverable name | Proposal for language extensions | link | |||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D1.3/1 | lead | Verimag | due | 12 | delivered | 20050214 | ||
| Related Deliverables | |||||||||
| Executive Summary | |||||||||
| Deliverable name | Final Proposal for language extension | link | |||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D1.3/2 | lead | Verimag | due | 36 | delivered | |||
| Related Deliverables | |||||||||
| Executive Summary | |||||||||
| Deliverable name | Joint report 1 Case studies in property based requirements specification | link | |||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D1.4/1 | lead | STM-Italy | due | 33 | delivered | |||
| Related Deliverables | |||||||||
| Executive Summary | |||||||||
| Deliverable name | Manual for Repositories of PSL/Sugar properties | link | |||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D1.5/1 | lead | due | 36 | delivered | ||||
| Related Deliverables | |||||||||
| Executive Summary | |||||||||
| Deliverable name | Property-driven design and implementation | link | |||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D2.1/1 | lead | TU Graz | due | 8 | delivered | 20040831, reissue 20050519 | ||
| Related Deliverables | |||||||||
| Executive Summary | |||||||||
| Deliverable name | Property-based logic synthesis for rapid design prototyping | link | |||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D2.2/1 | lead | TU Graz | due | 20 | delivered | 20050901 | ||
| Related Deliverables | |||||||||
| Executive Summary | |||||||||
| Deliverable name | Property-based error localization | link | |||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D2.2/2 | lead | TU Graz | due | 16 | delivered | 20050501 | ||
| Related Deliverables | |||||||||
| Executive Summary | |||||||||
| Deliverable name | Manual for Property-based synthesis tool | link | |||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D2.2/3 | lead | TU Graz | due | 31 | delivered | |||
| Related Deliverables | |||||||||
| Executive Summary | |||||||||
| Deliverable name | Manual for Property-based error localization tool | link | |||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D2.2/4 | lead | TU Graz | due | 32 | delivered | |||
| Related Deliverables | |||||||||
| Executive Summary | |||||||||
| Deliverable name | Evaluation of tools and methodology for property-based logic synthesis | link | |||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D2.3/1 | lead | IBM-HRL | due | 36 | delivered | |||
| Related Deliverables | |||||||||
| Executive Summary | |||||||||
| Deliverable name | Evaluation of tools developed for error localization | link | |||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D2.3/2 | lead | TU Graz | due | 36 | delivered | |||
| Related Deliverables | |||||||||
| Executive Summary | |||||||||
| Deliverable name | Report on experiences in property based design | link | |||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D2.3/3 | lead | IBM-HRL | due | 36 | delivered | |||
| Related Deliverables | |||||||||
| Executive Summary | |||||||||
| 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 | |||||||||
| 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 | |||||||||
| 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 | |||||||||
| Executive Summary | |||||||||
| 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 | |||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D3.2/10 | lead | TU Graz | due | 32 | delivered | |||
| Related Deliverables | |||||||||
| Executive Summary | |||||||||
| Deliverable name | Manual for Property-based automatic generation of test drivers and 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 | |||
| Related Deliverables | |||||||||
| Executive Summary | |||||||||
| Deliverable name | Manual for Property-based automatic generation of simulation monitors for digital design, based on algorithmic framework reported in 3.2/5. | link | |||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D3.2/12 | lead | Infineon | due | 30 | delivered | |||
| Related Deliverables | |||||||||
| Executive Summary | |||||||||
| 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 | |||
| Related Deliverables | |||||||||
| Executive Summary | |||||||||
| 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 | Weizmann | due | 23 | delivered | |||
| Related Deliverables | |||||||||
| Executive Summary | |||||||||
| 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 | 13 | delivered | 20050315/20050321 | ||
| Related Deliverables | |||||||||
| Executive Summary | |||||||||
| 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 | |||||||||
| Executive Summary | |||||||||
| Deliverable name | Research report on automata construction algorithms optimized for PSL/Sugar (static checking) | link | |||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D3.2/4 | lead | TU Graz | due | 16 | delivered | 20050630 | ||
| Related Deliverables | |||||||||
| Executive Summary | |||||||||
| Deliverable name | Research report on optimized dynamic property checking algorithms for digital designs | link | |||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D3.2/5 | lead | Weizmann | due | 20 | delivered | |||
| Related Deliverables | |||||||||
| Executive Summary | |||||||||
| 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 | 24 | delivered | |||
| Related Deliverables | |||||||||
| Executive Summary | |||||||||
| 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 | |||||||||
| Executive Summary | |||||||||
| 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 | 16 | delivered | 20050630/20050724 | ||
| Related Deliverables | |||||||||
| Executive Summary | |||||||||
| 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 | |||
| Related Deliverables | |||||||||
| Executive Summary | |||||||||
| 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 | |||||||||
| Deliverable name | Manual for port of IBM-HRL tools | link | |||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D3.3/2 | lead | IBM-HRL | due | 18 | delivered | |||
| Related Deliverables | |||||||||
| Executive Summary | |||||||||
| Deliverable name | Manual for port of Infineon tools | link | |||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D3.3/3 | lead | Infineon | due | 18 | delivered | 20050630/20050724 | ||
| Related Deliverables | |||||||||
| Executive Summary | |||||||||
| Deliverable name | Manual for port of of NuSMV | link | pdf Tool Download | ||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D3.3/4 | lead | ITC-Irst | due | 18 | delivered | 20050719 | ||
| Related Deliverables | |||||||||
| Executive Summary | |||||||||
| Deliverable name | Joint report on case studies in property based verification | link | |||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D3.4/1 | lead | STM-UK | due | 36 | delivered | |||
| Related Deliverables | |||||||||
| Executive Summary | |||||||||
| Deliverable name | Project web site | link | |||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D4.1/1 | lead | TU Graz | due | 3 | delivered | 20040415 | ||
| Related Deliverables | |||||||||
| Executive Summary | |||||||||
| Deliverable name | Technology implementation plan | link | |||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D4.2/2 | lead | IBM | due | 36 | delivered | |||
| Related Deliverables | |||||||||
| Executive Summary | |||||||||
| Deliverable name | Annual language study and recommendation to Accellera | link | |||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D4.3/1 | lead | IBM-HRL | due | 36 | delivered | |||
| Related Deliverables | |||||||||
| Executive Summary | |||||||||
| Deliverable name | Annual response from Accellera | link | |||||||
|---|---|---|---|---|---|---|---|---|---|
| number | D4.3/2 | lead | Accellera | due | 26 | delivered | |||
| Related Deliverables | |||||||||
| Executive Summary | |||||||||