Kaiserslautern - Fachbereich Elektrotechnik und Informationstechnik
Refine
Document Type
- Doctoral Thesis (5)
- Article (2)
Has Fulltext
- yes (7)
Keywords
Faculty / Organisational entity
In current practices of system-on-chip (SoC) design a trend can be observed to integrate more and more low-level software components into the system hardware at different levels of granularity. The implementation of important control functions and communication structures is frequently shifted from the SoC’s hardware into its firmware. As a result, the tight coupling of hardware and software at a low level of granularity raises substantial verification challenges since the conventional practice of verifying hardware and software independently is no longer sufficient. This calls for new methods for verification based on a joint analysis of hardware and software.
This thesis proposes hardware-dependent models of low-level software for performing formal verification. The proposed models are conceived to represent the software integrated with its hardware environment according to the current SoC design practices. Two hardware/software integration scenarios are addressed in this thesis, namely, speed-independent communication of the processor with its hardware periphery and cycle-accurate integration of firmware into an SoC module. For speed-independent hardware/software integration an approach for equivalence checking of hardware-dependent software is proposed and an evaluated. For the case of cycle-accurate hardware/software integration, a model for hardware/software co-verification has been developed and experimentally evaluated by applying it to property checking.
In recent years, formal property checking has become adopted successfully in industry and is used increasingly to solve the industrial verification tasks. This success results from property checking formulations that are well adapted to specific methodologies. In particular, assertion checking and property checking methodologies based on Bounded Model Checking or related techniques have matured tremendously during the last decade and are well supported by industrial methodologies. This is particularly true for formal property checking of computational System-on-Chip (SoC) modules. This work is based on a SAT-based formulation of property checking called Interval Property Checking (IPC). IPC originates in the Siemens company and is in industrial use since the mid 1990s. IPC handles a special type of safety properties, which specify operations in intervals between abstract starting and ending states. This paves the way for extremely efficient proving procedures. However, there are still two problems in the IPC-based verification methodology flow that reduce the productivity of the methodology and sometimes hamper adoption of IPC. First, IPC may return false counterexamples since its computational bounded circuit model only captures local reachability information, i.e., long-term dependencies may be missed. If this happens, the properties need to be strengthened with reachability invariants in order to rule out the spurious counterexamples. Identifying strong enough invariants is a laborious manual task. Second, a set of properties needs to be formulated manually for each individual design to be verified. This set, however, isn’t re-usable for different designs. This work exploits special features of communication modules in SoCs to solve these problems and to improve the productivity of the IPC methodology flow. First, the work proposes a decomposition-based reachability analysis to solve the problem of identifying reachability information automatically. Second, this work develops a generic, reusable set of properties for protocol compliance verification.
Die Architekturen vieler technischer Systeme sind derzeit im Umbruch. Der fortschreitende Einsatz von Netzwerken aus intelligenten rechnenden Knoten führt zu neuen Anforderungen an den Entwurf und die Analyse der resultierenden Systeme. Dabei spielt die Analyse des Zeitverhaltens mit seinen Bezügen zu Sicherheit und Performanz eine zentrale Rolle. Netzbasierte Automatisierungssysteme (NAS) unterscheiden sich hierbei von anderen verteilten Echtzeitsystemen durch ihr zyklisches Komponentenverhalten. Das aus der asynchronen Verknüpfung entstehende Gesamtverhalten ist mit klassischen Methoden kaum analysierbar. Zur Analyse von NAS wird deshalb der Einsatz der wahrscheinlichkeitsbasierten Modellverifikation (PMC) vorgeschlagen. PMC erlaubt detaillierte, quantitative Aussagen über das Systemverhalten. Für die dazu notwendige Modellierung des Systems auf Basis wahrscheinlichkeitsbasierter, zeitbewerteter Automaten wird die Beschreibungssprache DesLaNAS eingeführt. Exemplarisch werden der Einfluss verschiedener Komponenten und Verhaltensmodi auf die Antwortzeit eines NAS untersucht und die Ergebnisse mittels Labormessungen validiert.
Die fortschreitende Verbreitung von Ethernet-basierten Strukturen mit dezentralen und verteilten Anwendungen in der Automatisierung führt zu den so genannten netzbasier-ten Automatisierungssystemen (NAS). Diese sind zwar in Anschaffung und Betrieb kostengünstiger, moderner und flexibler als herkömmliche Strukturen, weisen jedoch nicht-deterministische Verzögerungen auf. Die genaue Analyse der resultierenden Antwortzeiten ist somit nicht nur Voraussetzung für den verantwortungsbewussten Einsatz dieser Technologie sondern ermöglicht es auch, bereits im Vorfeld von Umstrukturierungen oder Erweiterungen, Fragen der Verlässlichkeit zu klären. In diesem ersten von zwei Beiträgen wird hierfür zunächst die für die speziellen Bedürfnisse der Strukturbeschreibung von netzbasierten Automatisierungssystemen entwickelte Modellierungssprache DesLaNAS vorgestellt und auf ein einführendes Beispiel angewendet. Im zweiten Beitrag wird darauf aufbauend gezeigt, welchen Einfluss die einzelnen System-komponenten (SPS, Netzwerk, I/O-Karten) sowie netzbedingte Verhaltensmodi wie Synchronisation und die gemeinsame Nutzung von Ressourcen auf die Antwortzeiten des Gesamtsystems haben. Zur Analyse selbst wird die wahrscheinlichkeitsbasierte Modellverifikation (PMC) angewendet.
Netzbasierte Automatisierungssysteme (NAS) sind das Ergebnis der zunehmenden Dezentralisierung von Automatisierungssystemen mittels neuerer Netzwerkstrukturen. Eine ganze Fülle von Einflussfaktoren führt jedoch zu einem Spektrum von nicht-deterministischen Verzögerungen, die direkten Einfluss auf Qualität, Sicherheit und Zuverlässigkeit der Automatisierungsanlagen haben. Eine genaue Analyse dieser Einflussfaktoren ist somit nicht nur Voraussetzung für den verantwortungsbewussten Einsatz dieser Technologie sondern ermöglicht es auch, bereits im Vorfeld von Umstrukturierungen oder Erweiterungen Fragen der Verlässlichkeit zu klären. In diesem Beitrag wird gezeigt, welchen Einfluss einzelne Komponenten sowie netzbedingte Verhaltensmodi wie Synchronisation und die gemeinsame Nutzung von Ressourcen auf die Antwortzeiten des Gesamtsystems haben. Zur Analyse wird die wahrscheinlichkeitsbasierte Modellverifikation (PMC) verwendet. Umfangreiche Messungen wurden zur Validierung der Ergebnisse durchgeführt.
Mit zunehmender Integration von immermehr Funktionalität in zukünftigen SoC-Designs erhöht sich die Bedeutung der funktionalen Verifikation auf der Blockebene. Nur Blockentwürfe mit extrem niedriger Fehlerrate erlauben eine schnelle Integration in einen SoC-Entwurf. Diese hohen Qualitätsansprüche können durch simulationsbasierte Verifikation nicht erreicht werden. Aus diesem Grund rücken Methoden zur formalen Entwurfsverifikation in den Fokus. Auf der Blockebene hat sich die Eigenschaftsprüfung basierend auf dem iterativen Schaltungsmodell als erfolgreiche Technologie herausgestellt. Trotzdem gibt es immer noch einige Design-Klassen, die für BIMC schwer zu handhaben sind. Hierzu gehören Schaltungen mit hoher sequentieller Tiefe sowie arithmetische Blöcke. Die fortlaufende Verbesserung der verwendeten Beweismethoden, z.B. der verwendeten SAT-Solver, wird der zunehmenden Komplexität immer größer werdender Blöcke alleine nicht gewachsen sein. Aus diesem Grund zeigt diese Arbeit auf, wie bereits in der Problemaufbereitung des Front-Ends eines Werkzeugs zur formalen Verifikation Maßnahmen zur Vereinfachung der entstehenden Beweisprobleme ergriffen werden können. In den beiden angesprochenen Problemfeldern werden dazu exemplarisch geeignete Freiheitsgrade bei der Modellgenerierung im Front-End identifiziert und zur Vereinfachung der Beweisaufgaben für das Back-End ausgenutzt.
As the sustained trend towards integrating more and more functionality into systems on a chip can be observed in all fields, their economic realization is a challenge for the chip making industry. This is, however, barely possible today, as the ability to design and verify such complex systems could not keep up with the rapid technological development. Owing to this productivity gap, a design methodology, mainly using pre designed and pre verifying blocks, is mandatory. The availability of such blocks, meeting the highest possible quality standards, is decisive for its success. Cost-effective, this can only be achieved by formal verification on the block-level, namely by checking properties, ranging over finite intervals of time. As this verification approach is based on constructing and solving Boolean equivalence problems, it allows for using backtrack search procedures, such as SAT. Recent improvements of the latter are responsible for its high capacity. Still, the verification of some classes of hardware designs, enjoying regular substructures or complex arithmetic data paths, is difficult and often intractable. For regular designs, this is mainly due to individual treatment of symmetrical parts of the search space by backtrack search procedures used. One approach to tackle these deficiencies, is to exploit the regular structure for problem reduction on the register transfer level (RTL). This work describes a new approach for property checking on the RTL, preserving the problem inherent structure for subsequent reduction. The reduction is based on eliminating symmetrical parts from bitvector functions, and hence, from the search space. Several approaches for symmetry reduction in search problems, based on invariance of a function under permutation of variables, have been previously proposed. Unfortunately, our investigations did not reveal this kind of symmetry in relevant cases. Instead, we propose a reduction based on symmetrical values, as we encounter them much more frequently in our industrial examples. Let \(f\) be a Boolean function. The values \(0\) and \(1\) are symmetrical values for a variable \(x\) in \(f\) iff there is a variable permutation \(\pi\) of the variables of \(f\), fixing \(x\), such that \(f|_{x=0} = \pi(f|_{x=1})\). Then the question whether \(f=1\) holds is independent from this variable, and it can be removed. By iterative application of this approach to all variables of \(f\), they are either all removed, leaving \(f=1\) or \(f=0\) trivially, or there is a variable \(x'\) with no such \(\pi\). The latter leads to the conclusion that \(f=1\) does not hold, as we found a counter-example either with \(x'=0\), or \(x'=1\). Extending this basic idea to vectors of variables, allows to elevate it to the RTL. There, self similarities in the function representation, resulting from the regular structure preserved, can be exploited, and as a consequence, symmetrical bitvector values can be found syntactically. In particular, bitvector term-rewriting techniques, isomorphism procedures for specially manipulated term graphs, and combinations thereof, are proposed. This approach dramatically reduces the computational effort needed for functional verification on the block-level and, in particular, for the important problem class of regular designs. It allows the verification of industrial designs previously intractable. The main contributions of this work are in providing a framework for dealing with bitvector functions algebraically, a concise description of bounded model checking on the register transfer level, as well as new reduction techniques and new approaches for finding and exploiting symmetrical values in bitvector functions.