Filtern
Erscheinungsjahr
- 2002 (3) (entfernen)
Sprache
- Englisch (3) (entfernen)
Schlagworte
- OBDD (2)
- OBDDs (2)
- Algorithmus (1)
- Datenstruktur (1)
- Distributed Systems (1)
- Erweiterung (1)
- Formal Verification (1)
- Integrated Circuits (1)
- Logischer Entwurf (1)
- Middleware (1)
- Mobile Networks (1)
- Mobile Telekommunikation (1)
- Ordered Binary Decision Diagrams (1)
- Transitionssystem (1)
- Verifikation (1)
- Verteiltes System (1)
- XOR Parity (1)
- formal verification (1)
- partitioning (1)
- reordering (1)
Institut
- Informatik (3) (entfernen)
Today, usage of complex circuit designs in computers, in multimedia applications and communication devices is widespread and still increasing. At the same time, due to Moore's Law we do not expect to see an end in the growth of the complexity of digital circuits. The decreasing ability of common validation techniques -- like simulation -- to assure correctness of a circuit design enlarges the need for formal verification techniques. Formal verification delivers a mathematical proof that a given implementation of a design fulfills its specification. One of the basic and during the last years widely used data structure in formal verification are the so called Ordered Binary Decision Diagrams (OBDDs) introduced by R. Bryant in 1986. The topic of this thesis is integration of structural high-level information in the OBDD-based formal verification of sequential systems. This work consist of three major parts, covering different layers of formal verification applications: At the application layer, an assertion checking methodology, integrated in the verification flow of the high-level design and verification tool Protocol Compiler is presented. At the algorithmic layer, new approaches for partitioning of transition relations of complex finite state machines, that significantly improve the performance of OBDD-based sequential verification are introduced. Finally, at the data structure level, dynamic variable reordering techniques that drastically reduce the time required for reordering without a trade-off in OBDD-size are described. Overall, this work demonstrates how a tighter integration of applications by using structural information can significantly improve the efficiency of formal verification applications in an industrial setting.
Hardware bugs can be extremely expensive, financially. Because microprocessors and integrated circuits have become omnipresent in our daily live and also because of their continously growing complexity, research is driven towards methods and tools that are supposed to provide higher reliability of hardware designs and their implementations. Over the last decade Ordered Binary Decision Diagrams (OBDDs) have been well proven to serve as a data structure for the representation of combinatorial or sequential circuits. Their conciseness and their efficient algorithmic properties are responsible for their huge success in formal verification. But, due to Shannon's counting argument, OBDDs can not always guarantee the concise representation of a given design. In this thesis, Parity Ordered Binary Decision Diagrams are presented, which are a true extension of OBDDs. In addition to the regular branching nodes of an OBDD, functional nodes representing a parity operation are integrated into the data structure, thus resulting in Parity-OBDDs. Parity-OBDDs are more powerful than OBDDs are, but, they are no longer a canonical representation. Besides theoretical aspects of Parity-OBDDs, algorithms for their efficient manipulation are the main focus of this thesis. Furthermore, an analysis on the factors that influence the Parity-OBDD representation size gives way for the development of heuristic algorithms for their minimization. The results of these analyses as well as the efficiency of the data structure are also supported by experiments. Finally, the algorithmic concept of Parity-OBDDs is extended to Mod-p-Decision Diagrams (Mod-p-DDs) for the representation of functions that are defined over an arbitrary finite domain.
Mobile computing poses different requirements on middleware than more traditional desktop systems interconnected by fixed networks. Not only the characteristics of mobile network technologies as for example lower bandwidth and unreliability demand for customized support. Moreover, the devices employed in mobile settings usually are less powerful than their desktop counterparts. Slow processors, a fairly limited amount of memory, and smaller displays are typical properties of mobile equipment, again requiring special treatment. Furthermore, user mobility results in additional requirements on appropriate middleware support. As opposed to the quite static environments dominating the world of desktop computing, dynamic aspects gain more importance. Suitable strategies and techniques for exploring the environment e.g. in order to discover services available locally are only one example. Managing resources in a fault-tolerant manner, reducing the impact ill-behaved clients have on system stability define yet another exemplary prerequisite. Most state of the art middleware has been designed for use in the realm of static, resource rich environments and hence is not immediately applicable in mobile settings as set forth above. The work described throughout this thesis aims at investigating the suitability of different middleware technologies with regard to application design, development, and deployment in the context of mobile networks. Mostly based upon prototypes, shortcomings of those technologies are identified and possible solutions are proposed and evaluated where appropriate. Besides tailoring middleware to specific communication and device characteristics, the cellular structure of current mobile networks may and shall be exploited in favor of more scalable and robust systems. Hence, an additional topic considered within this thesis is to point out and investigate suitable approaches permitting to benefit from such cellular infrastructures. In particular, a system architecture for the development of applications in the context of mobile networks will be proposed. An evaluation of this architecture employing mobile agents as flexible, network-side representatives for mobile terminals is performed, again based upon a prototype application. In summary, this thesis aims at providing several complementary approaches regarding middleware support tailored for mobile, cellular networks, a field considered to be of rising importance in a world where mobile communication and particularly data services emerge rapidly, augmenting the globally interconnecting, wired Internet.