Distributed binary decision diagrams
Date
2010-12
Authors
Fasan, Mary Oluwasola
Journal Title
Journal ISSN
Volume Title
Publisher
Stellenbosch : University of Stellenbosch
Abstract
ENGLISH ABSTRACT: Binary Decision Diagrams (BDDs) are data structures that have been used to solve various
problems in different aspects of computer aided design and formal verification. The large
memory and time requirements of BDD applications are the major constraints that usually
prevent the use of BDDs since there is a limited amount of memory available on a machine.
One way of overcoming this resource limitation problem is to utilize the memory available
on a network of workstations (NOW). This requires the distribution of the computation and
memory requirements involved in the manipulation of BDDs over a NOW.
In this thesis, an algorithm for manipulating BDDs on a NOW is presented. The algorithm
makes use of the breadth-first technique to manipulate BDDs so that various BDD operations
can be started concurrently on the different workstations on the NOW. The design and implementation
details of the distributed BDD package are described. The various approaches
considered in order to optimize the performance of the algorithm are also discussed. Experimental
results demonstrating the performance and capabilities of the distributed package and
the benefits of the different optimization approaches are given.
AFRIKAANSE OPSOMMING: Binêre besluitnemingsbome (BBBs) is data strukture wat gebruik word om probleme in verskillende areas van Rekenaarwetenskap, soos by voorbeeld rekenaargesteunde ontwerp en formele verifikasie, op te los. Die tyd- en spasiekoste van BBB-gebaseerde toepassings is die hoofrede waarom BBBs nie altyd gebruik kan word nie; die geheue van ’n enkele is ongelukkig te beperkend. Een manier om hierdie hulpbronprobleem te omseil, is om die gedeelde geheue van die werkstasies in ’n netwerk van werkstasies (Engels: “network of workstations”, oftewel, ’n NOW) te benut. Dit is dus nodig om die berekening en geheuevoorvereistes van die BBB bewerking oor die NOW te versprei. Hierdie tesis bied ’n algoritme aan om BBBs op ’n NOW te hanteer. Die algoritme gebruik die breedte-eerste soektegniek, sodat BBB operasies gelyklopend kan uitvoer. Die details van die ontwerp en implementasie van die verspreide BBB bilbioteek word beskryf. Verskeie benaderings om die gedrag van die biblioteek te optimeer word ook aangespreek. Empiriese resultate wat die werkverrigting en kapasiteit van die biblioteek meet, en wat die uitwerking van die onderskeie optimerings aantoon, word verskaf.
AFRIKAANSE OPSOMMING: Binêre besluitnemingsbome (BBBs) is data strukture wat gebruik word om probleme in verskillende areas van Rekenaarwetenskap, soos by voorbeeld rekenaargesteunde ontwerp en formele verifikasie, op te los. Die tyd- en spasiekoste van BBB-gebaseerde toepassings is die hoofrede waarom BBBs nie altyd gebruik kan word nie; die geheue van ’n enkele is ongelukkig te beperkend. Een manier om hierdie hulpbronprobleem te omseil, is om die gedeelde geheue van die werkstasies in ’n netwerk van werkstasies (Engels: “network of workstations”, oftewel, ’n NOW) te benut. Dit is dus nodig om die berekening en geheuevoorvereistes van die BBB bewerking oor die NOW te versprei. Hierdie tesis bied ’n algoritme aan om BBBs op ’n NOW te hanteer. Die algoritme gebruik die breedte-eerste soektegniek, sodat BBB operasies gelyklopend kan uitvoer. Die details van die ontwerp en implementasie van die verspreide BBB bilbioteek word beskryf. Verskeie benaderings om die gedrag van die biblioteek te optimeer word ook aangespreek. Empiriese resultate wat die werkverrigting en kapasiteit van die biblioteek meet, en wat die uitwerking van die onderskeie optimerings aantoon, word verskaf.
Description
Thesis (MSc (Mathematical Sciences)--University of Stellenbosch, 2010.
Keywords
Program verification, Data structures, Binary decision diagrams, Distributed computing, Dissertations -- Computer science, Theses -- Computer science, Dissertations -- Mathematical sciences, Theses -- Mathematical sciences