Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Dominator-based Algorithms in Logic Synthesis and Verification
KTH, School of Information and Communication Technology (ICT), Electronic, Computer and Software Systems, ECS.
2007 (English)Doctoral thesis, monograph (Other academic)
Abstract [en]

Today's EDA (Electronic Design Automation) industry faces enormous challenges. Their primary cause is the tremendous increase of the complexity of modern digital designs. Graph algorithms are widely applied to solve various EDA problems. In particular, graph dominators, which provide information about the origin and the end of reconverging paths in a circuit graph, proved to be useful in various CAD (Computer Aided Design) applications such as equivalence checking, ATPG, technology mapping, and power optimization.

This thesis provides a study on graph dominators in logic synthesis and verification.

The thesis contributes a set of algorithms for computing dominators in circuit graphs. An algorithm is proposed for finding absolute dominators in circuit graphs. The achieved speedup of three orders of magnitude on several designs enables the computation of absolute dominators in large industrial designs in a few seconds. Moreover, the computation of single-vertex dominators in large multiple-output circuit graphs is considerably improved. The proposed algorithm reduces the overall runtime by efficiently recognizing and re-using isomorphic structures in dominator trees rooted at different outputs of the circuit graph. Finally, common multiple-vertex dominators are introduced. The algorithm to compute them is faster and finds more multiple-vertex dominators than previous approaches.

The thesis also proposes new dominator-based algorithms in the area of decomposition and combinational equivalence checking. A structural decomposition technique is introduced, which finds all simple-disjoint decompositions of a Boolean function which are reflected in the circuit graph. The experimental results demonstrate that the proposed technique outperforms state-of-the-art functional decomposition techniques. Finally, an approach to check the equivalence of two Boolean functions probabilistically is investigated. The proposed algorithm partitions the equivalence check employing dominators in the circuit graph. The experimental results confirm that, in comparison to traditional BDD-based equivalence checking methods, the memory consumption is considerably reduced by using the proposed technique.

Place, publisher, year, edition, pages
Stockholm: KTH , 2007. , xiv, 151 p.
Series
Trita-ICT-ECS AVH, ISSN 1653-6363 ; 2008:01
Keyword [en]
graph dominators, formal verification, logic synthesis, equivalence checking, decomposition
National Category
Other Electrical Engineering, Electronic Engineering, Information Engineering
Identifiers
URN: urn:nbn:se:kth:diva-4579ISBN: 978-91-7178-804-7 (print)OAI: oai:DiVA.org:kth-4579DiVA: diva2:12952
Public defence
2008-01-11, Sal D, KTH-Forum, Isafjordsgatan 39,, Kista, 13:00
Opponent
Supervisors
Note
QC 20100804Available from: 2007-12-14 Created: 2007-12-14 Last updated: 2010-08-04Bibliographically approved

Open Access in DiVA

fulltext(1714 kB)174 downloads
File information
File name FULLTEXT01.pdfFile size 1714 kBChecksum MD5
866ea5084d1160ad0f483937f5c06ad488a4c0ed88074471da49cda51b5433ddb017e813
Type fulltextMimetype application/pdf

Search in DiVA

By author/editor
Krenz-Bååth, René
By organisation
Electronic, Computer and Software Systems, ECS
Other Electrical Engineering, Electronic Engineering, Information Engineering

Search outside of DiVA

GoogleGoogle Scholar
Total: 174 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

isbn
urn-nbn

Altmetric score

isbn
urn-nbn
Total: 427 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf