Refine
Year of publication
Document Type
- Preprint (759)
- Article (402)
- Working Paper (119)
- Doctoral Thesis (93)
- Diploma Thesis (47)
- Conference Proceeding (41)
- Book (37)
- Bachelor Thesis (36)
- diplomthesis (28)
- Report (25)
Has Fulltext
- yes (1619)
Is part of the Bibliography
- no (1619)
Keywords
Institute
- Informatik (1619) (remove)
Funktionsorientierte Bausteine zur Integration kontinuierlicher Medien in verteilte Anwendungen
(1997)
Das Ziel der vorliegenden Arbeit war die Entwicklung einer komfortablen Beschreibung verteilter Anwendungen, die kontinuierliche Medien integrieren. Die Klarheit des Ansatzes ergibt sich aus der Beschränkung auf die anwenderrelevanten Funktionalitäten. Weitere Gebiete, die systembezogen sind, wurden nur soweit wie nötig behandelt. Die Aufgaben anderer Bereiche, wie des Betriebssystems und des Managementsystems sowie der Kommunikationsdienste, konnten nur gestreift werden, indem die anwendungsabhängigen Anforderungen spezifiziert wurden. Durch deren Extraktion und die Zuordnung der Anforderungen an die einzelnen Bereiche, ergibt sich eine klarere Sicht auf Betriebssystem, Management und Kommunikationsdienste und deren notwendige Weiterentwicklung. Das entwickelte Funktionenmodell beschreibt zusammenhängend alle mit kontinuierlichen Medien verbundenen Arbeiten. In der vorliegenden Arbeit wurde gezeigt, wie aus den Funktionen auf kontinuierlichen Medien durch die Spezifikation geeigneter Schnittstellen Bausteine zur Integration der Medien in verteilte Anwendungen erstellt werden. Die Beschrei bung der Bausteine erfolgt durch diese Schnittstellen; es sind Steuer-, Daten- und Managementschnittstellen. Die Herauslösung der gesonderten Beschreibung der Multimedia-Datenflußstruktur schafft einerseits die Grundlage für eine Teilklassifikation der Anwendungen nach Medien-Gesichtspunkten. Andererseits kann die Erstellung einer Anwendung aus einer bestimmten Anwendungsklasse, wie zum Beispiel ein einfaches Wiedergabesystem, durch die gesonderte Beschreibung der Multimedia-Datenflußstruktur schneller in der Bausteinstruktur realisiert werden. Das Funktionenmodell wird auch in [Fritzsche96] beschrieben. Das in dieser Arbeit konzipierte Bausteinmodell gewährleistet eine integrierte Beschreibung von Geräten, Werkzeugen und Anwendungen kontinuierlicher Medien. Die verwendete Beschreibungstechnik erlaubt dabei nicht nur eine übersichtliche Darstellung sondern bietet auch hierarchische Strukturierungen an. Das Zusammenspiel der Bausteine erfordert zu sätzliche Komponenten zur Steuerung und Abstimmung der einzelnen Funktionen, die in dieser Arbeit neu eingeführt werden. Es lassen sich sowohl zentralistische als auch verteilte Steuerungen realisieren. Mit einer entsprechenden Schnittstelle versehen kann eine Steuerkomponente eine ganze Gruppe von Bausteinen dem Benutzer als Einheit zur Verfügung stellen. Somit lassen sich auch verschiedene Medien und/oder mehrere Funktionen gemeinsam mit einer Steuerkomponente zu einem Baustein zusammenfassen. Diese zusammenge setzten Bausteine bieten nun echte Multifunktionalität und Multimedialität. Durch die Komponenten- und Anwendungsmodellierung nach [Zimm93] wird darüber hinaus eine flexible, auch dynamisch änderbare Anwendungsstruktur vom Anwendungs-Management ermöglicht. Das Bausteinmodell wird auch in [Fritzsche96] behandelt. Bisherigen Ansätzen für Multimedia-Komponenten fehlt die allgemeine Interoperabilität der Komponenten. Diese kann nur durch eine umfassende, formale Spezifikation der Komponenten-Schnittstellen, insbesondere aber von Steuerschnittstellen, erfolgen. Zur Spezifikation der Schnittstellen ist die Integration der kontinuierlichen oder zeitabhängigen Medien als abstrakte Datentypen unabdingbar. Auf diese Art werden aus den Komponenten Bausteine. Im vorliegenden Ansatz wurden erstmalig Steuerschnittstellen für Multimedia-Komponenten spezifiziert und als Hierarchie dargestellt. Der neue Ansatz erlaubt es daher, multimediale Systeme nach einem Baukastensystem zu erstellen, indem Bausteine durch Bindung untereinander zu einer Anwendung zusammengesetzt werden. Nach der Verbindungsstruktur der multimedialen Anwendung können verschiedene Anwendungstypen unterschieden werden. Die Definition der Komponentenschnittstellen bezieht sich auf ein abstraktes Datenmodell für kontinuierliche Medien. Das Datenmodell ist eine eigenständige Weiterentwicklung der Ansätze von [Herrtw91] und [Gibbs94] und kann auch zur Realisierung der Komponenten verwendet werden. Multimediadaten wurden zunächst auf zwei Ebenen als Sequenz und Sequenzelemente modelliert. Daraus lassen sich bereits einige Funktionen auf den Daten ableiten, die von den Bausteinen realisiert werden müssen. Kennzeichnend für die Sequenzelemente ist, daß sie die Zeitparameter Zeitpunkt und Dauer besitzen und damit eine explizite Integration der Zeit in das Datenmodell realisieren. Aus diesen Parametern der Elemente können auch für die Sequenz die Parameter Zeitpunkt und Dauer abgeleitet werden. Somit könnte eine Sequenz selbst wieder Element einer Sequenz werden. Da diese Sequenzen von Sequenzen aber zum Teil schwer zu handhaben sind und zum Aufbau von sehr komplexen Verschachtelungen verleiten, wird in dieser Arbeit eine andere Erweiterung der Datenhierarchie, eine Liste, vorgestellt. Diese Erweiterung führt nur eine weitere Hierarchieebene oder Granularitätsstufe ein, ist aber durch die vorgegebenen Funktionen gleichmächtig wie die Verschachtelung der Sequenzen, im Operationsablauf aber leichter nachzuvollziehen. Die Liste repräsentiert die gröbste Granularitätsstufe. Diese ist mit der Titelfolge einer Schallplatte oder einer CD vergleichbar. Die einzelnen Teile haben zueinander nur eine lose Ordnung. In der ersten Verfeinerung der Granularität wird in jedem einzelnen Listenelement eine strenge zeitliche Ordnung gefordert; ein Listenelement ist eine Sequenz. In der zweiten Stufe der Verfeinerung, der Unterteilung der Sequenzen, treten die bereits bekannten Se quenzelemente auf. Die Daten werden im Ticker-Schrittgeber-Modell interpretiert. Dieses Modell erhält zwei Zeitebenen, den Ticker als Bezugssystem der Funktionen untereinander und den Schrittgeber als Steuerung der einzelnen Funktionen. Ein zweistufiges Uhrenmodell mir festgesetzten Operationen und Uhrenbeziehungen wird in dieser Arbeit neu eingeführt. Die Beziehung zwischen Schrittgeber und Ticker ist, daß ein Schritt nach einer bestimmten Anzahl von Ticks erfolgt. Der Startwert des Tickers kann frei gewählt werden, ebenso der Startwert des Schrittgebers. Für den Schrittgeber bestimmt sein Start-Tick, wann er beginnt fortzuschreiten. Ein Schrittgeber ist mit genau einer Sequenz verbunden, deren Start-Schritt beschreibt, bei welchem Schrittwert das erste Sequenzelement gültig wird. Die Start-Zeitpunkte der Elemente und ihre Dauern werden in Schritten gemessen. Das Datenmodell für Multimedia wurde in [Fritzsche95] veröffentlicht. Implementierungen Als Grundlage für die Entwicklung der Bausteine zur Integration kontinuierlicher Medien in verteilte Anwendungen wurden die Funktionen auf den Medien herangezogen. Diese sind in ihren einfachsten Formen die Grundfunktionen Perzeption, Präsentation und Speicherung der Medien, wobei die Speicherung in die Funktionen Schreiben in den Speicher und Lesen aus dem Speicher geteilt wird. Die durch die Perzeption festgelegten, oder künstlich erzeugten Mediendaten können zwischen den einzelnen Funktionen übertragen werden. Eine Bearbeitung der Daten ist beim Austausch zwischen den Funktionen möglich. Die Veränderung der Daten und ihr Bezug zu den Grundfunktionen wird durch die Verarbeitungsfunktionen der Typen f 1 bis f 5 beschrieben. Die Funktionen werden durch Operationen gesteuert, die aus dem Datenmodell abgeleitet werden. Insbesondere wird so auch die explizite Veränderung der Zeitparameter möglich. Somit bietet das Datenmodell eine geeignete Grundlage für jede Art der Verarbeitung kontinuierlicher Medien. Das entwickelte Modell unterstützt die Anwendungserstellung durch objektorientierte Ansätze auf den Ebenen der Konzeption, der Anwendungsspezifikation und der Komponentenentwicklung. Konzeptionell bietet das Funktionenmodell die schnelle und übersichtliche Darstellung der Anwendung. Die aus dem Funktionenmodell ableitbare Anwendungsspezifikation unterstützt die weitere Entwicklung durch Anwendungs- und Komponentenschablonen, sowie durch die vorgefertigte und erweiterbare Hierarchie der Schnittstellen und durch die Bibliotheken für Standardbausteine. Die Verwendung dieser Elemente der Anwendungsspezifikation läßt sich teilweise automatisieren. Das Ergebnis der Anwendungsspezifikation ist eine Menge von Komponenten, die alle vollständig spezifiziert sind. Diese Komponenten sind die funktionsorientierten Bausteine zur Integration kontinuierlicher Medien in verteilte Anwendungen. Im ersten Schritt wurde das vorgestellte Datenmodell mit seinen Operationen in einer objektorientierten Programmiersprache (C [Lipp91]) implementiert [Braun92]. Darauf aufbauend wurden verschiedene Anwendungsfunktionen und Normalisierungsoperationen entwickelt und für den Bereich Audio realisiert [Bast93]. Die von den Funktionen auf kontinuierlichen Medien abgeleiteten Bausteine werden, wie in der vorliegenden Arbeit ausführlich dargestellt, als Komponenten verteilter Anwendungen realisiert. Aus den verschiedenen Realisierungsebenen sollen hier zwei Beispiele hervorgehoben werden. Zunächst wird auf die Komponentenrealisierung eingegangen; danach folgt die Realisierung von Tickern und enger Kopplung. Diese beiden Punkte stellen zentrale Aufgaben des Ansatzes dar. Realisierung von Komponenten Die Realisierung der Komponenten gliedert sich in zwei Abschnitte. Der erste Abschnitt ist die Zerlegung einer Komponente in Standardobjekte nach [Zimm93]. Die Standardobjekte entstammen Kommunikationsklassen, Stub- und Dispatcherklassen, Anwendungsklassen und Kooperationsprotokollklassen. Die Objekte der Anwendungsklassen realisieren die Anwendungsfunktionalität der Komponente. Das Ausprogrammieren dieser Objekte stellt den zweiten Abschnitt der Komponentenrealisierung dar. Dazu liefert das entwickelte Datenmodell die Programmierunterstützung. Zur Abbildung der Spezifikationskonstrukte der Komponenten auf Implementierungskonstrukte wird in [Zimm93] eine Methode vorgestellt, die die unterschiedlichen Konstrukte für Schnittstellen, Kommunikationskontexte und Komponenten auf Klassen und Objekte abbildet. So entsteht eine Klassenhierarchie von C Klassen [Lipp91] für kommunikations-, anwendung-s und managementorientierte Objekte. Weiterhin wird in [Zimm93] ein Verfahren vorgestellt, durch das in Abhängigkeit von den Eigenschaften einer Komponente parallel ablaufende Datenflüsse in ein System von leichtgewichtigen Prozessen (Threads) transformiert werden können. Als Resultat gewinnt man eine modulare Softwarearchitektur der Komponente, die sich aus interagierenden Objekten und zugehörigen Threads zusammen setzt. In [Zimm93] werden folgende Objektklassen unterschieden: . Kommunikationsklassen . Stub- und Dispatcherklassen . Anwendungsklassen . Kooperationsprotokollklassen. Eine elementare Objektarchitektur aus diesen Klassen ist in Abbildung 54 dargestellt. Es gibt jeweils eine Realisierung für eine Supplier-Komponente und eine Consumer- Komponente. Die Anwendungsobjekte können bezüglich ihrer Funktionalität in initiierende und akzeptierende Objekte eingeteilt werden. Im Falle unidirektionaler Schnittstellen sind die Anwendungsobjekte auf der Konsumentenseite (z.B. Benutzerkomponente) für die Initiierung von Methoden an Schnittstellenobjekten verantwortlich. Beispielsweise ist ein Anwendungsobjekt innerhalb der Benutzerkomponente für die Initiierung der Steueroperationen verantwortlich. Im Falle von interaktiven Komponenten [Zimm93] erfolgt dazu ein Benutzerdialog mit einem interaktiven Benutzer. Also realisiert innerhalb der Benutzerkomponente das Anwendungsobjekt einen solchen Benutzerdialog. Anwendungsobjekte auf der Konsumentenseite stellen somit typischerweise keine eigenen Methoden bereit, sondern bestehen lediglich aus einem Konstruktor. Auf der akzeptierenden Seite, den Anbieter (Supplier), realisiert ein Anwendungsobjekt die Operationen an einer Schnittstelle. Dazu wird eine Methode accept benötigt, falls ein verbindungsorientierter Kommunikationskontext zugrunde liegt. Diese Methode dient der Behandlung eingehender Verbindungswünsche. In [Alireza94] werden verschiedene Komponentenrealisierungen ausführlich vorgestellt. Die Realisierung der Ticker und Schrittgeber stellt die Einbettung der zeitbezogenen Komponenten in ihre (Betriebssystem) Umgebung dar. Ähnlich, wie eine Komponente über den Socketmechanismus Zugang zum Kommunikationssystem erhält, erhält eine zeitbezogene Komponente über den Ticker-Schrittgeber-Mechanismus Zugang zum Zeitbezugssystem. Denn die Schrittgeber beziehen sich auf Ticker, Ticker aber auf die Systemzeit. Da auch die Systemzeit als Takt zur Verfügung gestellt wird, können Ticker und Schrittgeber wegen ihrer ähnlichen Funktionalitäten aus einer gemeinsamen Zeitgeberklasse abgeleitet werden. Im Anhang C ist die Deklaration dieser gemeinsamen Klasse angegeben. In einer Anwendung beziehen sich die Schrittgeber verschiedener Komponenten auf einen gemeinsamen Ticker. Dieser Ticker liegt in der Systemumgebung der den Komponenten gemeinsamen interaktiven Benutzerkomponente. Die interaktive Benutzerkomponente verteilt die Ticks über die Steuerschnittstellen an die Komponenten und realisiert so die enge Kopplung der Komponenten. Bei einer Tickrate von 600 Hz ist es nur innerhalb eines Systems sinnvoll jeden Tick als Ereignis zu verteilen. Anstatt nun zu jedem Tick ein Ereignis zu verteilen werden bei der Tickverteilung Tickwerte mit fester Rate verteilt, wobei diese Rate in die Größenordnung der Schritte fällt. Um die Übertragungsraten gemäß den Anforderungen an der Steuerschnittstelle klein zu halten, wird zu jedem Schritt nur ein Teil (1 Byte) des Tickwertes übertragen. Begonnen wird mit der Übertragung des höchstwertigen Bytes, so daß im letzten Schritt einer Tickerübertragung mit dem letzten Byte der genaue aktuelle Tickwert übertragen wird. Ähnliche Verfahren werden bereits bei anderen Synchronisations verfahren verwendet. Eine genaue Beschreibung sowie die Kodierung für die verschachtelte Übertragung von Tickwerten und SchnittstellenAufrufen wird in [Hesme93] vorgestellt. Weitere Entwicklung Zur Realisierung verteilter multimedialer Anwendungen, muß man die einzelnen verteilten Komponenten bestimmen und ihre Funktion beschreiben. Die Komponenten tauschen unter einander Steuerungsinformationen und Multimediadaten aus. Diese Daten und das beim Austausch verwendete Protokoll sollten allgemein standardisiert sein, um den Zusammen schluß heterogener Systeme zu ermöglichen. In der vorliegenden Arbeit wurde gezeigt, wie sowohl die Daten als auch das Zusammenspiel der Komponenten festgelegt werden können. Obwohl alle Geräteklassen und Geräte funktionen sowie verschiedene Werkzeuge entwickelt wurden, und das vorgestellte Modell die gesamte Entwicklung verteilter multimedialer Anwendungen unterstützt, ist dieses große Gebiet noch lange nicht erschöpfend behandelt. Eine Erweiterung der Managementschnittstellen und die Realisierung von komplexen Werkzeugen sind die vordringlichsten Aufgaben. Damit entsteht ein mächtiges Entwicklungswerkzeug für Multimediaanwendungen. Funktionsorientierte Bausteine zur Integration kontinuierlicher Medien in verteilte Anwendungen Eine weitere Aufgabe ist die genauere Untersuchung der Nebenbedingungen, die zur Unterscheidung der Funktionen der Typen f 1 bis f 5 führten. Aus diesen Untersuchungen sowie aus den Ergebnissen der Ticker- und Schrittgeber-Realisierung lassen sich dann genauer spezifizierte Anforderungen an die Betriebs- oder Kommunikations-Systeme ableiten.
This paper proposes a non-standard way to combine lazy functional languages with I/O. In order to demonstrate the usefulness of the approach, a tiny lazy functional core language FUNDIO , which is also a call-by-need lambda calculus, is investigated. The syntax of FUNDIO has case, letrec, constructors and an IO-interface: its operational semantics is described by small-step reductions. A contextual approximation and equivalence depending on the input-output behavior of normal order reduction sequences is defined and a context lemma is proved. This enables to study a semantics of FUNDIO and its semantic properties. The paper demonstrates that the technique of complete reduction diagrams enables to show a considerable set of program transformations to be correct. Several optimizations of evaluation are given, including strictness optimizations and an abstract machine, and shown to be correct w.r.t. contextual equivalence. Correctness of strictness optimizations also justifies correctness of parallel evaluation. Thus this calculus has a potential to integrate non-strict functional programming with a non-deterministic approach to input-output and also to provide a useful semantics for this combination. It is argued that monadic IO and unsafePerformIO can be combined in Haskell, and that the result is reliable, if all reductions and transformations are correct w.r.t. to the FUNDIO-semantics. Of course, we do not address the typing problems the are involved in the usage of Haskell s unsafePerformIO. The semantics can also be used as a novel semantics for strict functional languages with IO, where the sequence of IOs is not fixed.
Dendritic spines are considered a morphological proxy for excitatory synapses, rendering them a target of many different lines of research. Over recent years, it has become possible to image simultaneously large numbers of dendritic spines in 3D volumes of neural tissue. In contrast, currently no automated method for spine detection exists that comes close to the detection performance reached by human experts. However, exploiting such datasets requires new tools for the fully automated detection and analysis of large numbers of spines. Here, we developed an efficient analysis pipeline to detect large numbers of dendritic spines in volumetric fluorescence imaging data. The core of our pipeline is a deep convolutional neural network, which was pretrained on a general-purpose image library, and then optimized on the spine detection task. This transfer learning approach is data efficient while achieving a high detection precision. To train and validate the model we generated a labelled dataset using five human expert annotators to account for the variability in human spine detection. The pipeline enables fully automated dendritic spine detection and reaches a near human-level detection performance. Our method for spine detection is fast, accurate and robust, and thus well suited for large-scale datasets with thousands of spines. The code is easily applicable to new datasets, achieving high detection performance, even without any retraining or adjustment of model parameters.
Highlights
• Transparency of design, reference frames and support for action were found to support students' sense-making of LA dashboards.
• The higher the overall SRL score, the more relevant the three factors were perceived by learners.
• Learner goals affect how relevant students find reference frames.
• The SRL effect on the perceived relevance of transparency depends on learner goals.
Abstract
Unequal stakeholder engagement is a common pitfall of adoption approaches of learning analytics in higher education leading to lower buy-in and flawed tools that fail to meet the needs of their target groups. With each design decision, we make assumptions on how learners will make sense of the visualisations, but we know very little about how students make sense of dashboard and which aspects influence their sense-making. We investigated how learner goals and self-regulated learning (SRL) skills influence dashboard sense-making following a mixed-methods research methodology: a qualitative pre-study followed-up with an extensive quantitative study with 247 university students. We uncovered three latent variables for sense-making: transparency of design, reference frames and support for action. SRL skills are predictors for how relevant students find these constructs. Learner goals have a significant effect only on the perceived relevance of reference frames. Knowing which factors influence students' sense-making will lead to more inclusive and flexible designs that will cater to the needs of both novice and expert learners.
Fraktale Planetengenerierung
(2006)
Wie die Diplomarbeit gezeigt hat, lassen sich zwar ganze Planeten ohne größere Verzerrungen mit Hilfe fraktaler Methoden modellieren. Allerdings stößt die Darstellungsqualität an ihre Grenzen, da sich gängige Level-of-Detail-Algorithmen, wie ROAM bzw. Röttger, nicht einfach an die durch das Surface-Refinement gegebenen Bedingungen anpassen. Insbesondere die Triangulierung durch gleichseitige Dreiecke hat sich als problematisch erwiesen. Ohne diese LOD-Techniken kann aber nur eine relativ geringe Auflösung berechnet werden. Der vorgestellte Level-of-Detail-Algorithmus stellt zwar keinen Ersatz für die obengenannten Verfahren dar. Er bietet aber eine sehr gute Grundlage, denn er schränkt einfach und dadurch sehr schnell den Bereich ein, in dem sich der Betrachter bzw. die virtuelle Kamera befindet. Dies ist vorallem auch deshalb wichtig, weil die bisher entwickelten LOD-Algorithmen nur mit vergleichsweise kleinen Flächen wirklich effizient funktionieren. Eine Kombination aus dem in der Diplomarbeit entwickelten Verfahren und einem ROAM/Röttger-ähnlichen Algorithmus würde deren jeweiligen Schwächen beheben. Die eigentliche Modellierung der Landschaft bzw. der Gebirgszüge lässt sich dagegen problemlos auch auf sphärische Körper übertragen, zumindest wenn man dafür den Plasma-Algorithmus verwendet.
Effiziente kryptographische Algorithmen sind ein wichtiger Grundstein für viele neue Anwendungen, wie zum Beispiel das Internet der Dinge (IoT) oder kontaktlose Zahlungssysteme. Daher ist es wichtig, dass neue Algorithmen mit verbesserten Sicherheitseigenschaften und speziellen Leistungseigenschaften entwickelt und analysiert werden. Ein Beispiel ist der aktuelle Trend zu leichtgewichtigen Algorithmen. Diese Entwicklungen erleichtern die Implementierung neuartiger Systeme und ermöglichen auch einen Schutz von bestehenden Systemen durch eine Anpassung auf den neuesten Stand der Technik. Neben der kryptologischen Analyse, ist die Bewertung von Implementierungs-Aspekten sehr wichtig, damit eine realistische Einschätzung der erzielbaren Leistung möglich ist.
Daher müssen für jeden neuen Algorithmus unterschiedliche Software- und Hardwarearchitekturen evaluiert werden. Die systematische Bewertung von Software-Implementierungen für unterschiedliche Hardware-Architekturen hat in den letzten Jahren große Fortschritte gemacht, zum Beispiel durch den SHA-3 Wettbewerb. Im Vergleich dazu ist die Evaluation für Hardware-Plattformen wie z.B. FPGAs weiterhin sehr zeitaufwendig und fehleranfällig. Dies liegt an vielen Faktoren, z.B. an den mannigfaltigen Möglichkeiten der verschiedenen Zieltechnologien. Ein möglicher Verbesserungsansatz besteht darin, die Bewertung mit einem abstrakteren Ansatz zu beginnen, um interessante Architekturen und Implementierungen anhand von theoretischen Eigenschaften auszuwählen.
Der erste Hauptbeitrag dieser Arbeit ist die Entwicklung einer abstrakten Bewertungsmethodik, die auf einem theoretischen Modell von getakteten Schaltungen basiert. Das Modell verbessert das Verständnis von Grundeigenschaften dieser Schaltungen und erleichtert auch die abstrakte Modellierung von Architekturen für einen spezifischen Algorithmus. Wenn mehrere verschiedene Architekturen für den gleichen Algorithmus ausgewertet werden, ist es auch möglich zu bestimmen, ob ein Algorithmus gut skaliert. Beispielsweise können Auswirkungen einer Verkleinerung des Datenpfades auf die Größe des Speicherverbrauchs analysiert werden. Basierend auf der entwickelten Methodik können wichtige Eigenschaften, wie der Speicherbedarf, die Anzahl an Taktzyklen oder die Pipeline-Tiefe systematisch bewertet werden. Damit kann eine grobe Schätzung für die Effektivtät einer Architektur abgeleitet werden.
Die Performance-Abschätzung wird auch durch ein theoretisches Konzept der Optimalität der Anzahl an Taktzyklen untermauert. Optimal in diesem Sinne ist eine Architektur, wenn sie verzögerungsfrei ist, d.h. keine Wartezyklen benötigt. Durch die Betrachtung von Datenabhängigkeiten zwischen den einzelnen Runden kann eine minimale und maximale Anzahl an Taktzyklen ermittelt werden. Eine Verletzung dieser Grenzen würde bedeuten, dass die Berechnung der Runden-Funktion nicht alle Ausgangs-Bits produziert hat, wenn diese für die nächste Runde benötigt werden und somit würden Wartezyklen entstehen.
Der zweite Beitrag der Dissertation nutzt die Analysemethodik für mehrere Hash-Funktion. Es werden sechs Hash-Funktionen bewertet: BLAKE, Grøstl, Keccak, JH, Skein und Photon. Die ersten fünf Hash-Funktionen sind die Finalisten des SHA-3 Wettbewerb. Die SHA-3 Finalisten haben eine hohe Sicherheit als oberstes Design-Ziel und nur in zweiter Linie eine hohe Performance. Im Gegensatz dazu wurde Photon für leichtgewichtige Anwendungen konzipiert, z.B. RFID-Tags. Dazu wurde auch die Sicherheit von Photon reduziert. Für jeden Algorithmus wird eine oder mehrere mögliche Organisationensformen des Speichers entwickelt. Als nächstes wird die Anzahl von Taktzyklen auf der Grundlage der Speicherorganisation ermittelt. Das generelle Ziel dabei ist die Entwicklung von Architekturen mit einer optimalen Anzahl von Taktzyklen. Die Diskussion konzentriert sich als nächstes auf verschiedene Möglichkeiten die Runden-Funktion optimal umzusetzen. Das Ergebnis der Evaluierung umfasst mindestens die Schätzung der minimalen Speicheranforderung, die analysierte Pipeline-Tiefe und den theoretischen Durchsatz für lange Nachrichten mit einer festgelegten Taktfrequenz. Diese Ergebnisse lassen eine Einschätzung über die mögliche Leistung der jeweiligen Architekturen zu.
Der dritte Beitrag der Arbeit besteht aus mehreren Implementierungs-Ergebnissen. Zunächst werden Ergebnisse für die SHA-3 Finalisten BLAKE, Grøstl, JH, Keccak und Skein gezeigt. Von den fünf Algorithmen haben alle außer Skein eine relativ hohe Performanz, während Skein abgeschlagen ist. Eine weitere Untersuchung konzentriert sich auf kleinere Implementierungen des SHA-3 Siegers Keccak. Dazu gehören auch nicht standardisierte Varianten mit einem kleineren Zustand. Diese kleineren Versionen werden mit ersten FPGA-Ergebnissen für die Photon Hash-Funktion verglichen. Eine wesentliche Erkenntnis davon ist, dass Keccak auch für FPGA-Anwendungen mit beschränktem Ressourcen-Bedarf prinzipiell sehr wettbewerbsfähig ist.
The constantly increasing memory density and performance of recent Field Programmable Gate Arrays (FPGA) has boosted a usage in many technical applications such as particle accelerators, automotive industry as well as defense and space. Some of these fields of interest are characterized by the presence of ionizing radiation as caused by natural decay or artificial excitation processes. Unfortunately, this type of radiation affects various digital circuits, including transistors forming Static Random Access Memory (SRAM) storage cells that constitute the technology node for high performance FPGAs. Various digital misbehavior in temporal or permanent manner as well as physical destruction of transistors are the consequence. Therefore, the mitigation of such effects becomes an essential design rule when using SRAM FPGAs in ionizing radiation environments. Tolerance against soft errors can be handled across various layers of modern FPGA design, starting with the most basic silicon manufacturing process, towards configuration, firmware, and system design, until finally ending up with application and software engineering. But only a highly optimized, joint concept of system-wide fault tolerance provides sufficient resilience against ionizing radiation effects without losing too much valuable device resources to the safety approach. This concept is introduced, analyzed, improved and validated in the present work. It includes, but is not limited to, static configuration scrubbing, various firmware redundancy approaches, dynamic memory conservation as well as state machine protection. Guidelines are given to improve manual design practices concerning fault tolerance and tools are shown to reduce necessary efforts. Finally, the SysCore development platform has been maintained to support the recommended design methods and act as Device Under Test (DUT) for all particle irradiation experiments that prove the efficiency of the proposed concept of system-wide fault tolerance for SRAM FPGAs in ionizing radiation environments.
Relational data exchange deals with translating relational data according to a given specification. This problem is one of the many tasks that arise in data integration, for example, in data restructuring, in ETL (Extract-Transform-Load) processes used for updating data warehouses, or in data exchange between different, possibly independently created, applications. Systems for relational data exchange exist for several decades now. Motivated by their experiences with one of those systems, Fagin, Kolaitis, Miller, and Popa (2003) studied fundamental and algorithmic issues arising in relational data exchange. One of these issues is how to answer queries that are posed against the target schema (i.e., against the result of the data exchange) so that the answers are consistent with the source data. For monotonic queries, the certain answers semantics proposed by Fagin, Kolaitis, Miller, and Popa (2003) is appropriate. For many non-monotonic queries, however, the certain answers semantics was shown to yield counter-intuitive results. This thesis deals with computing the certain answers for monotonic queries on the one hand, and on the other hand, it deals with the issue of which semantics are appropriate for answering non-monotonic queries, and how hard it is to evaluate non-monotonic queries under these semantics. As shown by Fagin, Kolaitis, Miller, and Popa (2003), computing the certain answers for unions of conjunctive queries - a subclass of the monotonic queries - basically reduces to computing universal solutions, provided the data transformation is specified by a set of tgds (tuple-generating dependencies) and egds (equality-generating dependencies). If M is such a specification and S is a source database, then T is called a solution for S under M if T is a possible result of translating S according to M. Intuitively, universal solutions are most general solutions. Since the above-mentioned work by Fagin, Kolaitis, Miller, and Popa it was unknown whether it is decidable if a source database has a universal solution under a given data exchange specification. In this thesis, we show that this problem is undecidable. More precisely, we construct a specification M that consists of tgds only so that it is undecidable whether a given source database has a universal solution under M. From the proof it also follows that it is undecidable whether the chase procedure - by which universal models can be obtained - terminates on a given source database and the set of tgds in M. The above results in particular strengthen results of Deutsch, Nash, and Remmel (2008). Concerning the issue of which semantics are appropriate for answering non-monotonic queries, we study several semantics for answering such queries. All of these semantics are based on the closed world assumption (CWA). First, the CWA-semantics of Libkin (2006) are extended so that they can be applied to specifications consisting of tgds and egds. The key is to extend the concept of CWA-solution, on which the CWA-semantics are based. CWA-solutions are characterized as universal solutions that are derivable from the source database using a suitably controlled version of the chase procedure. In particular, if CWA-solutions exist, then there is a minimal CWA-solution that is unique up to isomorphism: the core of the universal solutions introduced by Fagin, Kolaitis, and Popa (2003). We show that evaluation of a query under some of the CWA-semantics reduces to computing the certain answers to the query on the minimal CWA-solution. The CWA-semantics resolve some the known problems with answering non-monotonic queries. There are, however, two natural properties that are not possessed by the CWA-semantics. On the one hand, queries may be answered differently with respect to data exchange specifications that are logically equivalent. On the other hand, there are queries whose answer under the CWA-semantics intuitively contradicts the information derivable from the source database and the data exchange specification. To find an alternative semantics, we first test several CWA-based semantics from the area of deductive databases for their suitability regarding non-monotonic query answering in relational data exchange. More precisely, we focus on the CWA-semantics by Reiter (1978), the GCWA-semantics (Minker 1982), the EGCWA-semantics (Yahya, Henschen 1985) and the PWS-semantics (Chan 1993). It turns out that these semantics are either too weak or too strong, or do not possess the desired properties. Finally, based on the GCWA-semantics we develop the GCWA*-semantics which intuitively possesses the desired properties. For monotonic queries, some of the CWA-semantics as well as the GCWA*-semantics coincide with the certain answers semantics, that is, results obtained for the certain answers semantics carry over to those semantics. When studying the complexity of evaluating non-monotonic queries under the above-mentioned semantics, we focus on the data complexity, that is, the complexity when the data exchange specification and the query are fixed. We show that in many cases, evaluating non-monotonic queries is hard: co-NP- or NP-complete, or even undecidable. For example, evaluating conjunctive queries with at least one negative literal under simple specifications may be co-NP-hard. Notice, however, that this result only says that there is such a query and such a specification for which the problem is hard, but not that the problem is hard for all such queries and specifications. On the other hand, we identify a broad class of queries - the class of universal queries - which can be evaluated in polynomial time under the GCWA*-semantics, provided the data exchange specification is suitably restricted. More precisely, we show that universal queries can be evaluated on the core of the universal solutions, independent of the source database and the specification.
Two-particle angular correlations between trigger particles in the forward pseudorapidity range (2.5<|η|<4.0) and associated particles in the central range (|η|<1.0) are measured with the ALICE detector in p-Pb collisions at a nucleon-nucleon centre-of-mass energy of 5.02 TeV. The trigger particles are reconstructed using the muon spectrometer, and the associated particles by the central barrel tracking detectors. In high-multiplicity events, the double-ridge structure, previously discovered in two-particle angular correlations at midrapidity, is found to persist to the pseudorapidity ranges studied in this Letter. The second-order Fourier coefficients for muons in high-multiplicity events are extracted after jet-like correlations from low-multiplicity events have been subtracted. The coefficients are found to have a similar transverse momentum (pT) dependence in p-going (p-Pb) and Pb-going (Pb-p) configurations, with the Pb-going coefficients larger by about 16±6%, rather independent of pT within the uncertainties of the measurement. The data are compared with calculations using the AMPT model, which predicts a different pT and η dependence than observed in the data. The results are sensitive to the parent particle v2 and composition of reconstructed muon tracks, where the contribution from heavy flavour decays are expected to dominate at pT>2 GeV/c.
Two-particle angular correlations between trigger particles in the forward pseudorapidity range (2.5<|η|<4.0) and associated particles in the central range (|η|<1.0) are measured with the ALICE detector in p-Pb collisions at a nucleon-nucleon centre-of-mass energy of 5.02 TeV. The trigger particles are reconstructed using the muon spectrometer, and the associated particles by the central barrel tracking detectors. In high-multiplicity events, the double-ridge structure, previously discovered in two-particle angular correlations at midrapidity, is found to persist to the pseudorapidity ranges studied in this Letter. The second-order Fourier coefficients for muons in high-multiplicity events are extracted after jet-like correlations from low-multiplicity events have been subtracted. The coefficients are found to have a similar transverse momentum (pT) dependence in p-going (p-Pb) and Pb-going (Pb-p) configurations, with the Pb-going coefficients larger by about 16±6%, rather independent of pT within the uncertainties of the measurement. The data are compared with calculations using the AMPT model, which predicts a different pT and η dependence than observed in the data. The results are sensitive to the parent particle v2 and composition of reconstructed muon tracks, where the contribution from heavy flavour decays are expected to dominate at pT>2 GeV/c.
Two-particle angular correlations between trigger particles in the forward pseudorapidity range (2.5<|η|<4.0) and associated particles in the central range (|η|<1.0) are measured with the ALICE detector in p-Pb collisions at a nucleon-nucleon centre-of-mass energy of 5.02 TeV. The trigger particles are reconstructed using the muon spectrometer, and the associated particles by the central barrel tracking detectors. In high-multiplicity events, the double-ridge structure, previously discovered in two-particle angular correlations at midrapidity, is found to persist to the pseudorapidity ranges studied in this Letter. The second-order Fourier coefficients for muons in high-multiplicity events are extracted after jet-like correlations from low-multiplicity events have been subtracted. The coefficients are found to have a similar transverse momentum (pT) dependence in p-going (p-Pb) and Pb-going (Pb-p) configurations, with the Pb-going coefficients larger by about 16±6%, rather independent of pT within the uncertainties of the measurement. The data are compared with calculations using the AMPT model, which predicts a different pT and η dependence than observed in the data. The results are sensitive to the parent particle v2 and composition of reconstructed muon tracks, where the contribution from heavy flavour decays are expected to dominate at pT>2 GeV/c.
Two-particle angular correlations between trigger particles in the forward pseudorapidity range (2.5<|η|<4.0) and associated particles in the central range (|η|<1.0) are measured with the ALICE detector in p-Pb collisions at a nucleon-nucleon centre-of-mass energy of 5.02 TeV. The trigger particles are reconstructed using the muon spectrometer, and the associated particles by the central barrel tracking detectors. In high-multiplicity events, the double-ridge structure, previously discovered in two-particle angular correlations at midrapidity, is found to persist to the pseudorapidity ranges studied in this Letter. The second-order Fourier coefficients for muons in high-multiplicity events are extracted after jet-like correlations from low-multiplicity events have been subtracted. The coefficients are found to have a similar transverse momentum (pT) dependence in p-going (p-Pb) and Pb-going (Pb-p) configurations, with the Pb-going coefficients larger by about 16±6%, rather independent of pT within the uncertainties of the measurement. The data are compared with calculations using the AMPT model, which predicts a different pT and η dependence than observed in the data. The results are sensitive to the parent particle v2 and composition of reconstructed muon tracks, where the contribution from heavy flavour decays are expected to dominate at pT>2 GeV/c.
The strength of forward-backward (FB) multiplicity correlations is measured by the ALICE detector in proton-proton (pp) collisions at s√=0.9, 2.76 and 7 TeV. The measurement is performed in the central pseudorapidity region (|η|<0.8) for the transverse momentum pT>0.3 GeV/c. Two separate pseudorapidity windows of width (δη) ranging from 0.2 to 0.8 are chosen symmetrically around η=0. The multiplicity correlation strength (bcor) is studied as a function of the pseudorapidity gap (ηgap) between the two windows as well as the width of these windows. The correlation strength is found to decrease with increasing ηgap and shows a non-linear increase with δη. A sizable increase of the correlation strength with the collision energy, which cannot be explained exclusively by the increase of the mean multiplicity inside the windows, is observed. The correlation coefficient is also measured for multiplicities in different configurations of two azimuthal sectors selected within the symmetric FB η-windows. Two different contributions, the short-range (SR) and the long-range (LR), are observed. The energy dependence of bcor is found to be weak for the SR component while it is strong for the LR component. Moreover, the correlation coefficient is studied for particles belonging to various transverse momentum intervals chosen to have the same mean multiplicity. Both SR and LR contributions to bcor are found to increase with pT in this case. Results are compared to PYTHIA and PHOJET event generators and to a string-based phenomenological model. The observed dependencies of bcor add new constraints on phenomenological models.
The strength of forward-backward (FB) multiplicity correlations is measured by the ALICE detector in proton-proton (pp) collisions at s√=0.9, 2.76 and 7 TeV. The measurement is performed in the central pseudorapidity region (|η|<0.8) for the transverse momentum pT>0.3 GeV/c. Two separate pseudorapidity windows of width (δη) ranging from 0.2 to 0.8 are chosen symmetrically around η=0. The multiplicity correlation strength (bcor) is studied as a function of the pseudorapidity gap (ηgap) between the two windows as well as the width of these windows. The correlation strength is found to decrease with increasing ηgap and shows a non-linear increase with δη. A sizable increase of the correlation strength with the collision energy, which cannot be explained exclusively by the increase of the mean multiplicity inside the windows, is observed. The correlation coefficient is also measured for multiplicities in different configurations of two azimuthal sectors selected within the symmetric FB η-windows. Two different contributions, the short-range (SR) and the long-range (LR), are observed. The energy dependence of bcor is found to be weak for the SR component while it is strong for the LR component. Moreover, the correlation coefficient is studied for particles belonging to various transverse momentum intervals chosen to have the same mean multiplicity. Both SR and LR contributions to bcor are found to increase with pT in this case. Results are compared to PYTHIA and PHOJET event generators and to a string-based phenomenological model. The observed dependencies of bcor add new constraints on phenomenological models.
The strength of forward-backward (FB) multiplicity correlations is measured by the ALICE detector in proton-proton (pp) collisions at s√=0.9, 2.76 and 7 TeV. The measurement is performed in the central pseudorapidity region (|η|<0.8) for the transverse momentum pT>0.3 GeV/c. Two separate pseudorapidity windows of width (δη) ranging from 0.2 to 0.8 are chosen symmetrically around η=0. The multiplicity correlation strength (bcor) is studied as a function of the pseudorapidity gap (ηgap) between the two windows as well as the width of these windows. The correlation strength is found to decrease with increasing ηgap and shows a non-linear increase with δη. A sizable increase of the correlation strength with the collision energy, which cannot be explained exclusively by the increase of the mean multiplicity inside the windows, is observed. The correlation coefficient is also measured for multiplicities in different configurations of two azimuthal sectors selected within the symmetric FB η-windows. Two different contributions, the short-range (SR) and the long-range (LR), are observed. The energy dependence of bcor is found to be weak for the SR component while it is strong for the LR component. Moreover, the correlation coefficient is studied for particles belonging to various transverse momentum intervals chosen to have the same mean multiplicity. Both SR and LR contributions to bcor are found to increase with pT in this case. Results are compared to PYTHIA and PHOJET event generators and to a string-based phenomenological model. The observed dependencies of bcor add new constraints on phenomenological models.
The production of J/ψ is measured as a function of charged-particle multiplicity at forward rapidity in proton−proton (pp) collisions at center-of-mass energies s√= 5.02 and 13 TeV. The J/ψ mesons are reconstructed via their decay into dimuons in the rapidity interval (2.5 <y< 4.0), whereas the charged-particle multiplicity density (dNch/dη) is measured at midrapidity (|η|<1). The production rate as a function of multiplicity is reported as the ratio of the yield in a given multiplicity interval to the multiplicity-integrated one. This observable shows a linear increase with charged-particle multiplicity normalized to the corresponding average value for inelastic events (dNch/dη/⟨dNch/dη⟩), at both the colliding energies. Measurements are compared with available ALICE results at midrapidity and theoretical model calculations. First measurement of the mean transverse momentum (⟨pT⟩) of J/ψ in pp collisions exhibits an increasing trend as a function of dNch/dη/⟨dNch/dη⟩ showing a saturation towards high charged-particle multiplicities.
The production of J/ψ is measured as a function of charged-particle multiplicity at forward rapidity in proton-proton (pp) collisions at center-of-mass energies s√ = 5.02 and 13 TeV. The J/ψ mesons are reconstructed via their decay into dimuons in the rapidity interval (2.5 < y < 4.0), whereas the charged-particle multiplicity density (dNch/dη) is measured at midrapidity (|η| < 1). The production rate as a function of multiplicity is reported as the ratio of the yield in a given multiplicity interval to the multiplicity-integrated one. This observable shows a linear increase with charged-particle multiplicity normalized to the corresponding average value for inelastic events (dNch/dη/〈dNch/dη〉), at both the colliding energies. Measurements are compared with available ALICE results at midrapidity and theoretical model calculations. First measurement of the mean transverse momentum (〈pT〉) of J/ψ in pp collisions exhibits an increasing trend as a function of dNch/dη/〈dNch/dη〉 showing a saturation towards high charged-particle multiplicities.
The production of J/ψ is measured as a function of charged-particle multiplicity at forward rapidity in proton−proton (pp) collisions at center-of-mass energies s√= 5.02 and 13 TeV. The J/ψ mesons are reconstructed via their decay into dimuons in the rapidity interval (2.5 <y< 4.0), whereas the charged-particle multiplicity density (\dnchdeta) is measured at midrapidity (|η|<1). The production rate as a function of multiplicity is reported as the ratio of the yield in a given multiplicity interval to the multiplicity-integrated one. This observable shows a linear increase with charged-particle multiplicity normalized to the corresponding average value for inelastic events (dNch/dη/⟨dNch/dη⟩), at both the colliding energies. Measurements are compared with available ALICE results at midrapidity and theoretical model calculations. First measurement of the mean transverse momentum (⟨pT⟩) of J/ψ in pp collisions exhibits an increasing trend as a function of dNch/dη/⟨dNch/dη⟩ showing a saturation towards high charged-particle multiplicities.
This thesis has explored how structural techniques can be applied to the problem of formal verification for sequential circuits. Algorithms for formal verification which operate on non-canonical gate netlist representations of digital circuits have certain advantages over the traditional techniques based on canonical representations as BDDs. They allow to exploit problem-specific knowledge because they can take into account structural properties of the designs being analyzed. This allows us to break the problem down into sub-problems which are (hopefully) easier to be solved. However, in the past, the main application of such structural techniques was in the field of combinational equivalence checking. One reason for this is that the behaviour of a sequential system does not only depend on its inputs but also on its internal states, and no concepts had been developed to-date allowing structural methods to deal with large sets of states. An important goal of this research was therefore to develop structural, non-canonical forms of representing the reachable states of a finite state machine and to develop methods for reachability analysis based on such representations. In order to reach this goal, two steps were taken. Firstly, a framework for manipulating Boolean functions represented as gate netlists has been established. Secondly, using this framework, a structural method for FSM traversal was developed serving as the basis for an equivalence checking algorithm for sequential circuits. The framework for manipulating Boolean functions represented as multi-level combinational networks is based on a new concept of an implicant in a multi-level network and on an AND/ORtype enumeration technique which allows us to derive such implicants. This concept extends the classical notion of an implicant in two-level circuits to the multi-level case. Using this notion, arbitrary transformations in multi-level combinational networks can be performed. The multi-level network implicants can be determined from AND/OR reasoning graphs, which are associated with an AND/OR reasoning technique operating directly on the gate netlist description of a multi-level circuit. This reasoning technique has the important property that it is complete, i.e. the associated AND/OR trees contain all prime implicants of a Boolean function at an arbitrary node in a combinational circuit. In other words, AND/OR graphs constructed for a network function serve as a representation of this function. A great advantage over BDDs is that AND/OR graphs, besides representing the logic function, also represent some structural properties of the analyzed circuitry. This permits to develop heuristics that are specially tailored for certain applications such as logic optimization or verification. Another advantage which is especially useful for logic optimization is the fact that the proposed AND/OR enumeration scheme is not restricted to the use of a specific logic alphabet such as B3 = {0, 1, X}. By using Roth’s D-calculus based on B5 = {0, 1, D, D-Komplement} permissible implicants can be determined. Transformations based on permissible implicants exploit observability don’t-care conditions in logic synthesis by creating permissible functions at internal network nodes. In order to evaluate the new structural framework for manipulating Boolean functions represented as gate netlists, several experiments with implicant-based optimization of multi-level circuits were performed. The results show that implicant-based circuit transformations lead to significantly better optimization results than traditional synthesis techniques. Next, based on the proposed structural methods for Boolean function manipulation, techniques for representing and manipulating the set of states of a sequential circuit have been developed. The concept of a “stub circuit” was introduced which implicitly represents a set of state vectors as the range of a multi-output function given as a gate netlist. The stub circuit is the result of an existential quantification operation which is obtained by functional decomposition using implicant-based netlist transformations and a network cutting procedure. Using this existential quantification operation, a new structural FSM traversal algorithm was formulated which performs a fixed point iteration on the set of reachable states represented by the stub circuit. The proposed approach performs a reachability analysis of the states of a sequential circuit. It operates on gate netlists and naturally allows to incorporate structural properties of a design under consideration into the reasoning. Therefore, structural FSM traversal is an interesting alternative to traditional symbolic FSM traversal, especially in those applications of formal verification, where structural properties can be exploited. Structural FSM traversal was applied to the problem of sequential equivalence checking. Here, structural similarities between the designs to be compared can effectively reduce the complexity of the verification task. The FSM to be traversed is a special product machine called sequential miter. The special structural properties of this product machine have made it possible to formulate an approximate algorithm for structural FSM traversal, called record and play(). This algorithm uses an approximation on the reachable state set represented by the stub circuit which is very beneficial for performance. Instead of calculating the stub circuit using the exact algorithm, implicant-based transformations directly using structural design similarities are performed. These transformations, together with existential quantification implemented by the cutting procedure, lead to an over-approximation of the reachable state set. By this overapproximation, only such unreachable product states are added to the set of states represented by the stub circuit which are unreachable at the current point in time but which are nevertheless equivalent. Therefore, more product states are added to the set of reachable states sometimes leading to drastic acceleration of the traversal, i.e. the fixed point is reached in much fewer steps. The algorithm record and play() was applied to the problem of checking the equivalence of a circuit with its optimized and retimed version. Retiming is a form of sequential circuit optimization which can radically alter the state encoding of a circuit. Traditional FSM traversal techniques often fail because the BDDs needed to represent the reachable state set and the transition relation of the product machine become too large. Experiments were conducted to evaluate the performance of record and play() on a standard set of sequential benchmark circuits. The algorithm was capable of proving the equivalence of optimized and retimed circuits with their original versions, some of which (to our knowledge) have never before been verified using traditional techniques like symbolic FSM traversal. The experimental results are very promising. Future research will therefore explore how structural FSM traversal can be applied to model checking.