Parallel Algorithms for Construction and Manipulation of Binary Decision Diagrams

Binarni dijagrami odlučivanja (BDD) dijagrami omogućavaju učinkovit prikaz i formalnu verifikaciju digitalnih sustava. Postoje razne heuristike za optimizaciju formalne verifikacije BDD dijagramima. Jedan od načina za poboljšanje efikasnosti formalne verifikacije temeljene na BDD dijagramima je raspodijeljena izgradnja i manipulacija BDD dijagramima. Prednost raspodijeljene izgradnje BDD dijagrama leži u većoj procesorskoj snazi i većoj količini raspoloživog memorijskog prostora. Magistarski rad opisuje raspodijeljeni algoritam izgradnje i manipulacije BDD dijagramima namijenjen sustavu umreženih računala zasnovan na kombiniranom pristupu izgradnje BDD dijagrama. U radu je prikazana arhitektura i neki od detalja implementacije programskog ostvarenja tog algoritma. Mjerenja učinkovitosti algoritma provedena su izgradnjom BDD prikaza digitalnog množila i zbrajala zbog njihovog karakterističnog BDD prikaza. Mjerenja su izvedena na grozdu računala i dvoprocesorskom sustavu. U radu je dodatno analiziran utjecaj ostvarene priručne memorije na učinkovitost raspodijeljene izgradnje BDD dijagrama.Binary decision diagrams (BDDs) are data structures that enable efficient representation and formal verification of digital systems. There are different heuristics that can be employed in order to optimize BDD based formal verification process. In particular, distributed BDD construction and manipulation can be used to make formal verification of digital systems more efficient. The distribution benefits from additional CPU power and larger memory address space. The thesis describes distributed algorithm for BDD manipulation based on combined breadth-first and depth-first BDD construction techniques. The algorithm is targeted for execution on network of workstations. The implementation of algorithm is also given paying great attention to details. The measurement of the distributed BDD creation performance is accomplished by building BDD representation of digital adder and digital multiplier. These circuits are used because of the specific characteristics of their BDD representations. Performance of distributed algorithm is measured using two processor system and a computer cluster. Special analysis on performance impact of distributed computed cache is also given