Shop : Details
Shop
Details
45,80 €ISBN 978-3-8440-2468-5Paperback152 Seiten39 Abbildungen224 g21 x 14,8 cmEnglischDissertation
Januar 2014
Sacha Loitz
A Property Checking Methodology for Weakly Programmable System-on-Chip IPs
Eine Methode zur Eigenschaftsprüfung von schwach programmierbaren System-on-Chip IPs
Over the last years we have seen an increasing trend towards application speci?c instruction
set processors that are designed in order to meet the required ?exibility, energy ef?ciency
and performance constraints. In its extreme extend these processors are that
specialized that they only offer a limited programmability meeting exactly the demands
of the targeted application domain. Such processors are called weakly programmable
system-on-chip IPs (WPIP). The focus of these WPIPs is to offer just as much ?exibility
as required while delivering energy ef?ciency and performance comparable to that of custom
hardware. A main characteristic of these WPIPs is a customized memory architecture
with memories being accessed from several pipeline stages.
It turns out that the design ?ow followed by the designers of such WPIP designs hampers the validation of these IPs. On the one hand simulation based approaches can not achieve a suf?cient coverage. Formal veri?cation techniques, on the other hand, can achieve a suf?cient coverage, however, the design ?ow and distributed memory architecture forbid the usage of the veri?cation techniques as they are used in today’s formal veri?cation of standard processors.
This dissertation presents a systematic approach to completely verify these WPIP designs. A main aspect of the presented technique is that the veri?cation engineer is only required to specify the intended behavior at the level of well documented pipeline operations resulting in the operational ISA (OISA) model introduced in this work. The additional information required to handle the side-effects of the distributed memory access as well the behavior ensuring that the property set is complete are automatically generated by an analysis of the OISA model.
For WPIPs software and hardware are tightly coupled together making it important to ensure that the combined hardware software system is working correctly. The second part of this work presents how to reuse the property set from the hardware veri?cation for the veri?cation of the software.
The presented approach is demonstrated at the example of two WPIPs for channel decoding. Even so these WPIPs were intensively simulated beforehand several bugs were discovered with the presented formal veri?cation methodology.
It turns out that the design ?ow followed by the designers of such WPIP designs hampers the validation of these IPs. On the one hand simulation based approaches can not achieve a suf?cient coverage. Formal veri?cation techniques, on the other hand, can achieve a suf?cient coverage, however, the design ?ow and distributed memory architecture forbid the usage of the veri?cation techniques as they are used in today’s formal veri?cation of standard processors.
This dissertation presents a systematic approach to completely verify these WPIP designs. A main aspect of the presented technique is that the veri?cation engineer is only required to specify the intended behavior at the level of well documented pipeline operations resulting in the operational ISA (OISA) model introduced in this work. The additional information required to handle the side-effects of the distributed memory access as well the behavior ensuring that the property set is complete are automatically generated by an analysis of the OISA model.
For WPIPs software and hardware are tightly coupled together making it important to ensure that the combined hardware software system is working correctly. The second part of this work presents how to reuse the property set from the hardware veri?cation for the veri?cation of the software.
The presented approach is demonstrated at the example of two WPIPs for channel decoding. Even so these WPIPs were intensively simulated beforehand several bugs were discovered with the presented formal veri?cation methodology.
Schlagwörter: formal verification; application specific instruction set processors; completeness; Formale Verifikation; Anwendungsspezifische Prozessoren; Vollständigkeit; hardware verification; software verification; Hardware Verifikation; Software Verifikation
Verfügbare Online-Dokumente zu diesem Titel
Sie benötigen den Adobe Reader, um diese Dateien ansehen zu können. Hier erhalten Sie eine kleine Hilfe und Informationen, zum Download der PDF-Dateien.
Bitte beachten Sie, dass die Online-Dokumente nicht ausdruckbar und nicht editierbar sind.
Bitte beachten Sie auch weitere Informationen unter: Hilfe und Informationen.
Bitte beachten Sie auch weitere Informationen unter: Hilfe und Informationen.
| Dokument |  | Abstract / Kurzzusammenfassung | ||
| Dateiart |  | |||
| Kosten |  | frei | ||
| Aktion |  | Download der Datei | ||
| Dokument |  | Gesamtdokument | ||
| Dateiart | | |||
| Kosten |  | 34,35 € | ||
| Aktion |  | Zahlungspflichtig kaufen und download der Datei | ||
| Dokument |  | Inhaltsverzeichnis | ||
| Dateiart | | |||
| Kosten | | frei | ||
| Aktion | | Download der Datei | ||
Benutzereinstellungen für registrierte Online-Kunden (Online-Dokumente)
Sie können hier Ihre Adressdaten ändern sowie bereits georderte Dokumente erneut aufrufen.
Benutzer
Nicht angemeldet
Export bibliographischer Daten
Shaker Verlag GmbH
Am Langen Graben 15a
52353 Düren
Am Langen Graben 15a
52353 Düren
Mo. - Do. 8:00 Uhr bis 16:00 Uhr
Fr. 8:00 Uhr bis 15:00 Uhr
Fr. 8:00 Uhr bis 15:00 Uhr
Kontaktieren Sie uns. Wir helfen Ihnen gerne weiter.
