Joakim Urdahl

Path Predicate Abstraction

for Sound System-Level Modeling of Digital Circuits


Front	Back

ISBN:

978-3-8440-4233-7

Series:

Elektronik

Keywords:

Abstraction; Refinement; Hardware; Circuits; SoC; ESL; AML

Type of publication:

Thesis

Language:

English

Pages:

142 pages

Figures:

21 figures

Weight:

209 g

Format:

21 x 14,8 cm

Bindung:

Paperback

Price:

45,80 € / 57,20 SFr

Published:

February 2016

Buy:

Download:

Available PDF-Files for this title:

You need the Adobe Reader, to open the files. Here you get help and information, for the download.

These files are not printable.


	Document		Document
	Type		PDF
	Costs		34,35 EUR
	Action		Purchase in obligation and display of file - 1,0 MB (1049806 Byte)
	Action		Purchase in obligation and download of file - 1,0 MB (1049806 Byte)


	Document		Table of contents
	Type		PDF
	Costs		free
	Action		Display of file - 62 kB (63971 Byte)
	Action		Download of file - 62 kB (63971 Byte)

User settings for registered users

You can change your address here or download your paid documents again.

User:	Not logged in.
Actions:	Login / Register Forgotten your password?

Recommendation:

You want to recommend this title?

Review copy:

Here you can order a review copy.

Link:

You want to link this page? Click here.

Export citations:

Text
BibTex
RIS

Abstract:

Path Predicate Abstraction (PPA) is a formalism suitable for describing the abstraction/refinement relationship between highly abstract models at an Electronic System Level (ESL) and their implementations at the Register Transfer Level (RTL). In such a relationship the properties of the ESL model translate, without further proof, to corresponding properties of the RTL implementation, i.e., the ESL model is sound with respect to the implementation. Thus, verification results obtained based on the much simpler ESL model can be trusted as valid also for the RTL implementation. If the creation of such sound ESL models can be made efficient in practice then the costs for the verification of digital systems can be drastically reduced.

This dissertation contributes the theoretical framework of PPA as well as approaches for applying PPA efficiently in practice, both "bottom up" to create sound abstractions for already existing RTL implementations and as an integrated part of a "top down" design flow. In both approaches the soundness of the abstraction is established by formal property checking. All involved properties are of a specific form facilitating SAT-based proof algorithms that scale well, as shown in experimental results, also for large industrial designs.