| Summary: | Thesis (MSc (Mathematical Sciences)--University of Stellenbosch, 2010. === 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.
|
|---|
